diff --git a/Complexity.lean b/Complexity.lean
index d8bc086f06..6ab6d0cbd2 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1071,6 +1071,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Am
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.BPP
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.TimeLayer
 public import Complexity.Computability.Complexity.Classes.LogSpace.Savitch
 public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON
 public import Complexity.Computability.Complexity.Classes.MIP
@@ -2724,6 +2725,7 @@ public import Complexity.Foundations.LinearAlgebra.Matrix.Rank
 public import Complexity.Foundations.LinearAlgebra.Matrix.RectPermanent
 public import Complexity.Foundations.LinearAlgebra.Matrix.SchurComplement
 public import Complexity.Foundations.LinearAlgebra.Matrix.SubmatrixRobust
+public import Complexity.Foundations.LinearAlgebra.Matrix.TimeLayer
 public import Complexity.Foundations.LinearAlgebra.Matrix.Toeplitz
 public import Complexity.Foundations.LinearAlgebra.PivotSpace
 public import Complexity.Foundations.LinearAlgebra.Rank
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/TimeLayer.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/TimeLayer.lean
new file mode 100644
index 0000000000..536fa5978a
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/TimeLayer.lean
@@ -0,0 +1,237 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
+public import Complexity.Foundations.LinearAlgebra.Matrix.TimeLayer
+import Mathlib.Tactic.Positivity
+
+/-!
+# Clocked fair-coin configuration matrices
+
+The ordinary configuration matrix keeps halted views absorbing and counts both coins, including
+coincident successors. Halving it gives a nonnegative matrix with row mass exactly one on any
+closed finite set of views. Clocking this actual matrix and paying the accepting-view indicator
+only at the final time gives the strictly forward system of [OpenAI2026LogSpace, Lemma 2.1].
+Its explicitly constructed potential lies in `[0,1]` at every clocked view. At clock zero it is
+the actual finite-time acceptance probability, and also the existing finite sum of live-matrix
+acceptance terms. No halting-time hypothesis is needed for these finite-horizon identities.
+
+The clocked matrix entry is also identified with the native compact-ID coin count, supplied
+with its one scanned input symbol. This preserves the distinction between an absorbing halted
+view before the horizon and a terminal clock layer with zero outgoing weight.
+
+This file proves mathematical structure and acceptance semantics. It does not implement bounded
+vertex enumeration, compose the symbol query with the original input, or construct incoming
+paired ports or the recursive estimator. In particular it is not a proof of `BPL ⊆ L`.
+
+## Main results
+
+* `Turing.MultiTapePTM.half_configMatrix_mulVec_one`: actual fair-coin row mass.
+* `Turing.MultiTapePTM.timeLayer_configMatrix_potential_mem_Icc`: bounded potential at every view.
+* `Turing.MultiTapePTM.timeLayer_configMatrix_acceptance`: the clock-zero acceptance identity.
+* `Turing.MultiTapePTM.ConfigurationGraph.timeLayer_configMatrix_eq_coinCountWithSymbol`:
+  the actual local reader gives each nonzero clocked entry.
+* `Cslib.Complexity.exists_timeLayer_configMatrix_of_mem_BPL`: polynomial-size strict-forward
+  systems with the actual `2/3` versus `1/3` acceptance gap.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 2, Lemma 2.1, `model.tex`, terminal-time configuration reduction
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+/-- The accepting halted-view indicator lies in `[0,1]` at every view. -/
+theorem Turing.FiniteCfg.acceptVec_mem_Icc {k : ℕ} {State : Type} {R : Type*}
+    [Field R] [LinearOrder R] [IsStrictOrderedRing R]
+    {V : Finset (Turing.FiniteCfg k Bool State)} :
+    Turing.FiniteCfg.acceptVec R V ∈ Set.Icc 0 1 := by
+  classical
+  constructor <;> intro x <;> unfold Turing.FiniteCfg.acceptVec <;> split_ifs <;> simp
+
+namespace Turing.MultiTapePTM
+
+open Matrix
+
+variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State)
+  {R : Type*} [Field R] {V : Finset (FiniteCfg k Bool State)}
+
+section Ordered
+
+variable [LinearOrder R] [IsStrictOrderedRing R]
+
+/-- The normalized ordinary coin matrix is entrywise nonnegative, including absorbing rows. -/
+theorem half_configMatrix_nonneg :
+    ∀ x y : V, 0 ≤ ((2 : R)⁻¹ • machine.configMatrix R V) x y := by
+  classical
+  intro x y
+  change 0 ≤ (2 : R)⁻¹ * ∑ b : Bool, if machine.viewCoinStep x b = y then 1 else 0
+  positivity
+
+/-- Closedness of the actual view set makes every normalized ordinary coin row sum to one. -/
+theorem half_configMatrix_mulVec_one
+    (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) :
+    ((2 : R)⁻¹ • machine.configMatrix R V) *ᵥ 1 = 1 := by
+  classical
+  ext x
+  rw [Matrix.smul_mulVec, Pi.smul_apply, configMatrix, Matrix.coinStepMatrix_mulVec hV]
+  simp [smul_eq_mul]
+
+open scoped Classical in
+/-- The actual clocked configuration potential is bounded on every state, including views
+unreachable from the designated start. Closedness is the only graph hypothesis. -/
+theorem timeLayer_configMatrix_potential_mem_Icc
+    (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) (T : ℕ) :
+    Matrix.timeLayerPotential T ((2 : R)⁻¹ • machine.configMatrix R V)
+      (FiniteCfg.acceptVec R V) ∈ Set.Icc 0 1 := by
+  classical
+  exact Matrix.timeLayerPotential_mem_Icc (half_configMatrix_nonneg machine)
+    (half_configMatrix_mulVec_one machine hV).le (FiniteCfg.acceptVec_mem_Icc (R := R)) T
+
+end Ordered
+
+open scoped Classical in
+/-- At the initial clocked view, the explicit potential is the machine's finite-time
+acceptance probability. The horizon may be zero and the machine need not yet have halted. -/
+theorem timeLayer_configMatrix_acceptance {input : List Bool}
+    (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V)
+    (hinit : machine.toNTM.initView input ∈ V) (T : ℕ) :
+    Matrix.timeLayerPotential T ((2 : R)⁻¹ • machine.configMatrix R V)
+      (FiniteCfg.acceptVec R V) (toLex (0, ⟨_, hinit⟩)) =
+        (machine.acceptCoins input T : R) / 2 ^ T := by
+  classical
+  rw [Matrix.timeLayerPotential_zero]
+  exact (acceptCoins_div_eq_configMatrix_pow_mulVec R hV hinit T).symm
+
+open scoped Classical in
+/-- The terminal-reward convention agrees exactly with the existing first-stop sum of live
+acceptance terms; these are two proved expressions for the same actual probability. -/
+theorem timeLayer_configMatrix_eq_sum_live [CharZero R] {input : List Bool}
+    (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V)
+    (hinit : machine.toNTM.initView input ∈ V) (T : ℕ) :
+    Matrix.timeLayerPotential T ((2 : R)⁻¹ • machine.configMatrix R V)
+      (FiniteCfg.acceptVec R V) (toLex (0, ⟨_, hinit⟩)) =
+        ∑ t ∈ Finset.range (T + 1),
+          (((2 : R)⁻¹ • machine.liveConfigMatrix R V) ^ t *ᵥ FiniteCfg.acceptVec R V)
+            ⟨_, hinit⟩ := by
+  classical
+  rw [timeLayer_configMatrix_acceptance machine hV hinit]
+  exact acceptCoins_div_eq_sum_liveConfigMatrix R hV hinit T
+
+namespace ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph
+
+variable [Fintype State]
+
+/-- A clocked ordinary entry is half the certified local coin count exactly when the target
+clock is the next one, and zero otherwise. Representation hypotheses concern only the two
+actual views, and the original input is used at its explicit `queryIndex`. -/
+theorem timeLayer_configMatrix_eq_coinCountWithSymbol {B T : ℕ} (i j : Fin (T + 1))
+    (x y : V) (hinput : x.val.input = y.val.input)
+    (hx : MultiTapeNTM.outputClass x.val.output = x.val.output)
+    (hy : MultiTapeNTM.outputClass y.val.output = y.val.output)
+    (hfitX : Fits B (registers x.val)) (hfitY : Fits B (registers y.val)) :
+    Matrix.timeLayer T ((2 : R)⁻¹ • machine.configMatrix R V)
+      (toLex (i, x)) (toLex (j, y)) =
+        if i.val + 1 = j.val then
+          (coinCountWithSymbol machine B x.val.input.length (vertexID B x.val) (vertexID B y.val)
+            x.val.input[queryIndex (k := k) B (vertexID B x.val)]? : R) / 2 else 0 := by
+  change (if i.val + 1 = j.val then (2 : R)⁻¹ * machine.configMatrix R V x y else 0) = _
+  rw [← coinCountWithSymbol_eq_configMatrix machine x y hinput hx hy hfitX hfitY]
+  simp only [div_eq_inv_mul]
+
+/-- Actual reachability and logarithmic space discharge the representation conditions for
+the clocked entry reader at the standard polynomial radix. -/
+theorem timeLayer_configMatrix_eq_coinCountWithSymbol_of_reachable (c : ℕ) {input : List Bool}
+    (hs : machine.toNTM.RunsInSpace input (c * (Nat.log2 input.length + 1)))
+    (hV : ∀ v ∈ V, Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v)
+    {T : ℕ} (i j : Fin (T + 1)) (x y : V) :
+    let B := radix (radixExponent State c) input.length
+    Matrix.timeLayer T ((2 : R)⁻¹ • machine.configMatrix R V)
+      (toLex (i, x)) (toLex (j, y)) =
+        if i.val + 1 = j.val then
+          (coinCountWithSymbol machine B input.length (vertexID B x.val) (vertexID B y.val)
+            input[queryIndex (k := k) B (vertexID B x.val)]? : R) / 2 else 0 := by
+  change (if i.val + 1 = j.val then (2 : R)⁻¹ * machine.configMatrix R V x y else 0) = _
+  rw [← coinCountWithSymbol_eq_configMatrix_of_reachable (R := R) machine c hs hV x y]
+  simp only [div_eq_inv_mul]
+
+end ConfigurationGraph
+
+end Turing.MultiTapePTM
+
+namespace Cslib.Complexity
+
+open _root_.Turing Matrix
+
+variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
+
+/-- **A concrete strict-forward matrix system for `BPL`.** Clock the actual ordinary
+configuration matrix up to the existing polynomial halting bound `T`. There are at most
+`(T + 1) * T` clocked views, the terminal reward is zero or one, and the explicitly defined
+potential solves the system, lies in `[0,1]`, and retains the `2/3` versus `1/3` gap.
+
+The order within a layer is chosen by a finite equivalence; it makes no algorithmic enumeration
+claim. The clocked entries separately have the compact-reader interpretation above. Bounded-ID
+enumeration, whole-input access, paired ports, and a native estimator remain separate. -/
+theorem exists_timeLayer_configMatrix_of_mem_BPL (h : A ∈ BPL enc) :
+    ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : MultiTapePTM k Bool State) (d : ℕ),
+      ∀ a,
+        let T := 2 * (2 * ((enc a).length + 1)) ^ d
+        ∃ (V : Finset (FiniteCfg k Bool State)) (hinit : M.toNTM.initView (enc a) ∈ V)
+          (order : LinearOrder V),
+          letI := order
+          let P := (2 : ℚ)⁻¹ • M.configMatrix ℚ V
+          let C := timeLayer T P
+          let e := timeLayerReward T (FiniteCfg.acceptVec ℚ V)
+          let p := timeLayerPotential T P (FiniteCfg.acceptVec ℚ V)
+          Fintype.card (Lex (Fin (T + 1) × V)) ≤ (T + 1) * T ∧
+          C.IsStrictUpperTriangular ∧ (∀ x y, 0 ≤ C x y) ∧ C *ᵥ 1 ≤ 1 ∧
+          (∀ x, e x = 0 ∨ e x = 1) ∧ (1 - C) *ᵥ p = e ∧ (1 - C)⁻¹ *ᵥ e = p ∧
+          p ∈ Set.Icc 0 1 ∧
+          (a ∈ A → 2 / 3 ≤ p (toLex (0, ⟨_, hinit⟩))) ∧
+          (a ∉ A → p (toLex (0, ⟨_, hinit⟩)) ≤ 1 / 3) := by
+  classical
+  obtain ⟨k, State, hfin, M, d, hM⟩ := exists_configMatrix_of_mem_BPL h
+  refine ⟨k, State, hfin, M, d, fun a => ?_⟩
+  obtain ⟨V, hinit, hcard, hclosed, hreach, htime, _, hmem, hnot⟩ := hM a
+  -- Keep the existing equality decision so the chosen order uses the same matrix powers.
+  let decV : DecidableEq V := inferInstance
+  let baseOrder : LinearOrder V := LinearOrder.lift' V.equivFin V.equivFin.injective
+  let order : LinearOrder V :=
+    { baseOrder with
+      toDecidableEq := decV
+      compare := fun a b =>
+        @compareOfLessAndEq V a b baseOrder.toLT (baseOrder.toDecidableLT a b) decV
+      compare_eq_compareOfLessAndEq := fun _ _ => rfl }
+  refine ⟨V, hinit, order, ?_⟩
+  have hP0 := M.half_configMatrix_nonneg (R := ℚ) (V := V)
+  have hP1 := (M.half_configMatrix_mulVec_one (R := ℚ) hclosed).le
+  refine ⟨?_, timeLayer_isStrictUpperTriangular _ _, timeLayer_nonneg hP0 _,
+    timeLayer_mulVec_one_le hP1 _, ?_, one_sub_timeLayer_mulVec _ _ _,
+    inv_one_sub_timeLayer_mulVec _ _ _, M.timeLayer_configMatrix_potential_mem_Icc hclosed _,
+    ?_, ?_⟩
+  · rw [card_timeLayer, Fintype.card_coe]
+    exact Nat.mul_le_mul_left _ hcard
+  · intro x
+    unfold timeLayerReward FiniteCfg.acceptVec
+    split_ifs <;> simp
+  · intro ha
+    rw [M.timeLayer_configMatrix_acceptance hclosed hinit,
+      M.acceptCoins_div_eq_inv_mulVec ℚ htime hclosed hreach hinit]
+    exact hmem ha
+  · intro ha
+    rw [M.timeLayer_configMatrix_acceptance hclosed hinit,
+      M.acceptCoins_div_eq_inv_mulVec ℚ htime hclosed hreach hinit]
+    exact hnot ha
+
+end Cslib.Complexity
diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer.lean b/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer.lean
new file mode 100644
index 0000000000..63147d80d4
--- /dev/null
+++ b/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer.lean
@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy
+import Mathlib.Data.Fintype.Prod
+
+/-!
+# Time layers and terminal rewards
+
+`Matrix.timeLayer T P` places a copy of `P` between each pair of consecutive clock layers
+`0, …, T`. All other entries vanish, including the final rows. The lexicographic order makes
+this matrix strictly upper triangular, even when `P` itself has cycles or absorbing states.
+The reward `e` is paid only at time `T`. Its potential at `(i,x)` is exactly
+`(P ^ (T - i) *ᵥ e) x`, which solves the actual clocked linear system. Nonnegative
+substochastic `P` and rewards in `[0,1]` give a potential in `[0,1]` at every clocked state.
+
+This is the matrix construction in [OpenAI2026LogSpace, Lemma 2.1], using the terminal-reward
+convention of its proof. It does not enumerate configurations or assert a resource bound for
+accessing the matrix. The machine and local-count specialization is in
+`Classes.LogSpace.Randomized.TimeLayer`.
+
+## Main definitions
+
+* `Matrix.timeLayer`: transitions only to the next clock layer.
+* `Matrix.timeLayerReward`: a reward supported on the last layer.
+* `Matrix.timeLayerPotential`: the actual remaining-time matrix power.
+
+## Main results
+
+* `Matrix.timeLayer_isStrictUpperTriangular`, `Matrix.timeLayer_mulVec_one_le`:
+  forwardness and the inherited row bound.
+* `Matrix.one_sub_timeLayer_mulVec`: the potential solves the clocked system.
+* `Matrix.inv_one_sub_timeLayer_mulVec`: its inverse-matrix expression.
+* `Matrix.timeLayerPotential_mem_Icc`: the potential is bounded at every clocked state.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 2, Lemma 2.1, `model.tex`, terminal-time construction
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Matrix
+
+open Finset
+
+variable {V R : Type*}
+
+/-- Place `P` between consecutive clock layers, with no outgoing edge from the last layer. -/
+@[expose] def timeLayer [Zero R] (T : ℕ) (P : Matrix V V R) :
+    Matrix (Lex (Fin (T + 1) × V)) (Lex (Fin (T + 1) × V)) R :=
+  fun a b => if (ofLex a).1.val + 1 = (ofLex b).1.val then P (ofLex a).2 (ofLex b).2 else 0
+
+/-- Pay the original reward only at the final clock layer. -/
+@[expose] def timeLayerReward [Zero R] (T : ℕ) (e : V → R) : Lex (Fin (T + 1) × V) → R :=
+  fun a => if (ofLex a).1.val = T then e (ofLex a).2 else 0
+
+/-- The value at a clocked state after its actual remaining number of transitions. -/
+@[expose] def timeLayerPotential [Fintype V] [DecidableEq V] [Semiring R]
+    (T : ℕ) (P : Matrix V V R) (e : V → R) : Lex (Fin (T + 1) × V) → R :=
+  fun a => (P ^ (T - (ofLex a).1.val) *ᵥ e) (ofLex a).2
+
+/-- Clocking multiplies the number of states by exactly `T + 1`. -/
+theorem card_timeLayer [Fintype V] (T : ℕ) :
+    Fintype.card (Lex (Fin (T + 1) × V)) = (T + 1) * Fintype.card V := by
+  rw [Fintype.card_congr (ofLex : Lex (Fin (T + 1) × V) ≃ Fin (T + 1) × V)]
+  simp only [Fintype.card_prod, Fintype.card_fin]
+
+/-- The clock alone supplies strict forwardness; no acyclicity of `P` is needed. -/
+theorem timeLayer_isStrictUpperTriangular [LT V] [Zero R] (T : ℕ) (P : Matrix V V R) :
+    (timeLayer T P).IsStrictUpperTriangular := by
+  intro a b hab
+  apply ite_eq_right
+  intro hclock
+  exact hab (Prod.Lex.lt_iff.mpr (Or.inl (show (ofLex a).1 < (ofLex b).1 by
+    change (ofLex a).1.val < (ofLex b).1.val
+    omega)))
+
+/-- Every terminal row is zero, including when the horizon is zero. -/
+theorem timeLayer_last [Zero R] (T : ℕ) (P : Matrix V V R) (x : V)
+    (b : Lex (Fin (T + 1) × V)) : timeLayer T P (toLex (Fin.last T, x)) b = 0 := by
+  apply ite_eq_right
+  have hb := (ofLex b).1.isLt
+  change ¬ T + 1 = (ofLex b).1.val
+  omega
+
+/-- A clocked row applies `P` to the next slice; at the horizon it vanishes. -/
+theorem timeLayer_mulVec [Fintype V] [Semiring R] (T : ℕ) (P : Matrix V V R)
+    (v : Lex (Fin (T + 1) × V) → R) (i : Fin (T + 1)) (x : V) :
+    (timeLayer T P *ᵥ v) (toLex (i, x)) =
+      if h : i.val < T then
+        (P *ᵥ fun y => v (toLex (⟨i.val + 1, Nat.succ_lt_succ h⟩, y))) x else 0 := by
+  classical
+  unfold mulVec dotProduct
+  rw [← (toLex : Fin (T + 1) × V ≃ Lex (Fin (T + 1) × V)).sum_comp]
+  rw [Fintype.sum_prod_type]
+  by_cases hi : i.val < T
+  · rw [dite_eq_left hi]
+    rw [sum_eq_single (⟨i.val + 1, Nat.succ_lt_succ hi⟩ : Fin (T + 1))]
+    · simp [timeLayer]
+    · intro j _ hj
+      have hne : i.val + 1 ≠ j.val := fun h => hj (Fin.ext h.symm)
+      simp [timeLayer, hne]
+    · simp
+  · rw [dite_eq_right hi]
+    refine sum_eq_zero fun j _ => ?_
+    have hne : i.val + 1 ≠ j.val := by omega
+    simp [timeLayer, hne]
+
+/-- Nonnegative entries remain nonnegative after clocking. -/
+theorem timeLayer_nonneg [Zero R] [Preorder R] {P : Matrix V V R}
+    (hP : ∀ x y, 0 ≤ P x y) (T : ℕ) : ∀ a b, 0 ≤ timeLayer T P a b := by
+  intro a b
+  unfold timeLayer
+  split_ifs
+  · exact hP _ _
+  · exact le_rfl
+
+/-- Clocking preserves the substochastic row bound, with zero terminal rows. -/
+theorem timeLayer_mulVec_one_le [Fintype V] [Semiring R] [PartialOrder R] [IsOrderedRing R]
+    {P : Matrix V V R} (hP : P *ᵥ 1 ≤ 1) (T : ℕ) : timeLayer T P *ᵥ 1 ≤ 1 := by
+  intro a
+  let i := (ofLex a).1
+  let x := (ofLex a).2
+  change (timeLayer T P *ᵥ 1) (toLex (i, x)) ≤ (1 : R)
+  rw [timeLayer_mulVec]
+  split_ifs
+  · exact hP x
+  · exact zero_le_one
+
+/-- A substochastic matrix preserves `[0,1]` under every finite power. -/
+theorem pow_mulVec_mem_Icc [Fintype V] [DecidableEq V]
+    [Semiring R] [PartialOrder R] [IsOrderedRing R] {P : Matrix V V R} {e : V → R}
+    (hP0 : ∀ x y, 0 ≤ P x y) (hP1 : P *ᵥ 1 ≤ 1) (he : e ∈ Set.Icc 0 1) (t : ℕ) :
+    P ^ t *ᵥ e ∈ Set.Icc 0 1 := by
+  induction t with
+  | zero => simpa using he
+  | succ t ih =>
+    rw [pow_succ', ← mulVec_mulVec]
+    exact ⟨mulVec_nonneg hP0 ih.1, mulVec_le_one hP0 hP1 ih.2⟩
+
+/-- The actual remaining-time potential lies in `[0,1]` at every clocked state. -/
+theorem timeLayerPotential_mem_Icc [Fintype V] [DecidableEq V]
+    [Semiring R] [PartialOrder R] [IsOrderedRing R] {P : Matrix V V R} {e : V → R}
+    (hP0 : ∀ x y, 0 ≤ P x y) (hP1 : P *ᵥ 1 ≤ 1) (he : e ∈ Set.Icc 0 1) (T : ℕ) :
+    timeLayerPotential T P e ∈ Set.Icc 0 1 := by
+  constructor <;> intro a
+  · exact (pow_mulVec_mem_Icc hP0 hP1 he _).1 _
+  · exact (pow_mulVec_mem_Icc hP0 hP1 he _).2 _
+
+/-- At clock zero, the potential is the original `T`-step terminal expectation. -/
+theorem timeLayerPotential_zero [Fintype V] [DecidableEq V] [Semiring R]
+    (T : ℕ) (P : Matrix V V R) (e : V → R) (x : V) :
+    timeLayerPotential T P e (toLex (0, x)) = (P ^ T *ᵥ e) x := by
+  simp [timeLayerPotential]
+
+/-- The clocked potential solves the actual linear system, with reward only at final time. -/
+theorem one_sub_timeLayer_mulVec [Fintype V] [DecidableEq V] [Ring R]
+    (T : ℕ) (P : Matrix V V R) (e : V → R) :
+    (1 - timeLayer T P) *ᵥ timeLayerPotential T P e = timeLayerReward T e := by
+  rw [sub_mulVec, one_mulVec]
+  ext a
+  let i := (ofLex a).1
+  let x := (ofLex a).2
+  change timeLayerPotential T P e (toLex (i, x)) -
+    (timeLayer T P *ᵥ timeLayerPotential T P e) (toLex (i, x)) =
+      timeLayerReward T e (toLex (i, x))
+  rw [timeLayer_mulVec]
+  by_cases hi : i.val < T
+  · rw [dite_eq_left hi]
+    have hne : i.val ≠ T := by omega
+    have hremaining : T - i.val = T - (i.val + 1) + 1 := by omega
+    change (P ^ (T - i.val) *ᵥ e) x -
+      (P *ᵥ (P ^ (T - (i.val + 1)) *ᵥ e)) x = if i.val = T then e x else 0
+    rw [ite_eq_right hne, mulVec_mulVec, ← pow_succ', ← hremaining, sub_self]
+  · rw [dite_eq_right hi]
+    have hiT : i.val = T := by omega
+    simp [timeLayerPotential, timeLayerReward, hiT]
+
+/-- The clocked linear system has determinant one over any commutative ring. -/
+theorem det_one_sub_timeLayer [Fintype V] [LinearOrder V] [CommRing R]
+    (T : ℕ) (P : Matrix V V R) : (1 - timeLayer T P).det = 1 := by
+  rw [sub_eq_add_neg]
+  exact (timeLayer_isStrictUpperTriangular T P).neg.det_one_add
+
+/-- The inverse expression equals the explicitly constructed remaining-time potential. -/
+theorem inv_one_sub_timeLayer_mulVec [Fintype V] [LinearOrder V] [CommRing R]
+    (T : ℕ) (P : Matrix V V R) (e : V → R) :
+    (1 - timeLayer T P)⁻¹ *ᵥ timeLayerReward T e = timeLayerPotential T P e := by
+  have hu : IsUnit (1 - timeLayer T P).det := by rw [det_one_sub_timeLayer]; exact isUnit_one
+  rw [← one_sub_timeLayer_mulVec T P e, mulVec_mulVec, nonsing_inv_mul _ hu, one_mulVec]
+
+end Matrix
diff --git a/ComplexityTests/TimeLayer.lean b/ComplexityTests/TimeLayer.lean
new file mode 100644
index 0000000000..861671546f
--- /dev/null
+++ b/ComplexityTests/TimeLayer.lean
@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.TimeLayer
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Clocked matrix and machine examples
+
+An absorbing two-state matrix has a self-loop at its running state and acceptance probability
+`3/4` after two steps. Clocking removes every cycle and pays the reward only at final time.
+The same example is realized by a concrete zero-work-tape fair-coin machine: false continues,
+true outputs true and halts. Thus the finite-horizon theorem also applies when no uniform
+halting bound exists. Zero horizons and the actual compact-count reader are checked too.
+-/
+
+namespace ComplexityTests.TimeLayer
+
+open Matrix Finset
+
+private def P : Matrix (Fin 2) (Fin 2) ℚ := ![![1 / 2, 1 / 2], ![0, 1]]
+private def e : Fin 2 → ℚ := ![0, 1]
+
+private theorem P_nonneg (x y : Fin 2) : 0 ≤ P x y := by
+  fin_cases x <;> fin_cases y <;> norm_num [P]
+
+private theorem P_row : P *ᵥ 1 ≤ 1 := by
+  intro x
+  fin_cases x <;> norm_num [P, mulVec, dotProduct, Fin.sum_univ_two]
+
+private theorem e_bounds : e ∈ Set.Icc 0 1 := by
+  constructor <;> intro x <;> fin_cases x <;> norm_num [e]
+
+example : ¬ P.IsStrictUpperTriangular ∧ (timeLayer 2 P).IsStrictUpperTriangular := by
+  refine ⟨fun h => ?_, timeLayer_isStrictUpperTriangular _ _⟩
+  have h00 := h (i := 0) (j := 0) (by decide)
+  norm_num [P] at h00
+
+example : timeLayerPotential 2 P e (toLex (0, 0)) = 3 / 4 ∧
+    timeLayerPotential 2 P e (toLex (1, 0)) = 1 / 2 ∧
+    timeLayerPotential 2 P e (toLex (2, 0)) = 0 := by
+  change (P ^ 2 *ᵥ e) 0 = 3 / 4 ∧ (P ^ 1 *ᵥ e) 0 = 1 / 2 ∧ (P ^ 0 *ᵥ e) 0 = 0
+  rw [pow_two, ← mulVec_mulVec, pow_one, pow_zero]
+  norm_num [P, e, mulVec, dotProduct, Fin.sum_univ_two]
+
+-- An absorbing state still advances its clock; the reward is withheld until the last layer.
+example : timeLayer 2 P (toLex (1, 1)) (toLex (2, 1)) = 1 ∧
+    timeLayerReward 2 e (toLex (1, 1)) = 0 ∧ timeLayerReward 2 e (toLex (2, 1)) = 1 := by
+  norm_num [timeLayer, timeLayerReward, P, e]
+
+example : timeLayerPotential 2 P e ∈ Set.Icc 0 1 :=
+  timeLayerPotential_mem_Icc P_nonneg P_row e_bounds 2
+
+example : (1 - timeLayer 2 P) *ᵥ timeLayerPotential 2 P e = timeLayerReward 2 e ∧
+    (1 - timeLayer 2 P)⁻¹ *ᵥ timeLayerReward 2 e = timeLayerPotential 2 P e :=
+  ⟨one_sub_timeLayer_mulVec _ _ _, inv_one_sub_timeLayer_mulVec _ _ _⟩
+
+example (x : Fin 2) (b : Lex (Fin 1 × Fin 2)) :
+    timeLayer 0 P (toLex (0, x)) b = 0 := timeLayer_last 0 P x b
+
+example (x : Fin 2) : timeLayerPotential 0 P e (toLex (0, x)) = e x := by
+  rw [timeLayerPotential_zero, pow_zero, one_mulVec]
+
+example : Fintype.card (Lex (Fin 3 × Fin 2)) = 6 := card_timeLayer (V := Fin 2) 2
+
+open Cslib.Turing Turing MultiTapeTM
+
+/-- False repeats the current running view; true accepts immediately. -/
+private def machine : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ _ _ _ bit :=
+    .step
+      { inputTape := 0
+        workTapes := Fin.elim0
+        output := if bit then some true else none
+        state := if bit then none else some () }
+      Empty.elim Empty.elim
+
+private def view (done : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨[], if done then none else some (), 1, Fin.elim0, if done then [true] else []⟩
+
+private theorem start_eq : machine.toNTM.initView [] = view false := by
+  simp [MultiTapeNTM.initView, MultiTapePTM.toNTM, MultiTapePTM.branches,
+    MultiTapeMachine.toNTM, FiniteCfg.init, machine, view, funext_iff]
+
+private theorem step_view (done bit : Bool) :
+    machine.viewCoinStep (view done) bit = view (done || bit) := by
+  cases done <;> cases bit <;>
+    simp [MultiTapePTM.viewCoinStep, machine, view, MultiTapePTM.withCoin,
+      MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv, FiniteCfg.step,
+      FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, funext_iff]
+
+private theorem view_injective : Function.Injective view := by
+  intro a b h
+  cases a <;> cases b <;> simp_all [view]
+
+open scoped Classical in
+private noncomputable def views : Finset (FiniteCfg 0 Bool Unit) := univ.image view
+
+open scoped Classical in
+private noncomputable def vertex (done : Bool) : views :=
+  ⟨view done, mem_image.mpr ⟨done, mem_univ _, rfl⟩⟩
+
+private theorem closed : ∀ x ∈ views, ∀ bit, machine.viewCoinStep x bit ∈ views := by
+  classical
+  intro x hx bit
+  obtain ⟨done, _, rfl⟩ := mem_image.mp hx
+  rw [step_view]
+  exact mem_image.mpr ⟨done || bit, mem_univ _, rfl⟩
+
+private noncomputable def loopMatrix : Matrix views views ℚ :=
+  (2 : ℚ)⁻¹ • machine.configMatrix ℚ views
+
+private theorem loop_mulVec (g : views → ℚ) (done : Bool) :
+    (loopMatrix *ᵥ g) (vertex done) = (g (vertex done) + g (vertex true)) / 2 := by
+  classical
+  have hcoin (bit : Bool) :
+      (⟨machine.viewCoinStep (vertex done) bit, closed _ (vertex done).property bit⟩ : views) =
+        vertex (done || bit) := Subtype.ext (step_view done bit)
+  rw [loopMatrix, Matrix.smul_mulVec, Pi.smul_apply, MultiTapePTM.configMatrix,
+    Matrix.coinStepMatrix_mulVec closed]
+  simp only [hcoin, Fintype.sum_bool, Bool.or_false, Bool.or_true, smul_eq_mul]
+  ring
+
+open scoped Classical in
+private theorem loop_probability :
+    timeLayerPotential 2 loopMatrix (FiniteCfg.acceptVec ℚ views) (toLex (0, vertex false)) =
+      3 / 4 := by
+  classical
+  rw [timeLayerPotential_zero, pow_two, ← mulVec_mulVec, loop_mulVec, loop_mulVec, loop_mulVec]
+  norm_num [FiniteCfg.acceptVec, vertex, view]
+
+-- This is the native machine's actual accepting-coin frequency, derived through the new bridge.
+example : (machine.acceptCoins [] 2 : ℚ) / 2 ^ 2 = 3 / 4 := by
+  classical
+  have hinit : machine.toNTM.initView [] ∈ views := start_eq ▸ (vertex false).property
+  have hstart : (⟨machine.toNTM.initView [], hinit⟩ : views) = vertex false :=
+    Subtype.ext start_eq
+  have h := machine.timeLayer_configMatrix_acceptance (R := ℚ) closed hinit 2
+  rw [hstart] at h
+  exact h.symm.trans loop_probability
+
+-- The machine potential bound has all graph assumptions discharged on these actual two views.
+open scoped Classical in
+example : timeLayerPotential 2 loopMatrix (FiniteCfg.acceptVec ℚ views) ∈ Set.Icc 0 1 :=
+  machine.timeLayer_configMatrix_potential_mem_Icc closed 2
+
+private theorem reachable (v : FiniteCfg 0 Bool Unit) (hv : v ∈ views) :
+    Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView []) v := by
+  classical
+  obtain ⟨done, _, rfl⟩ := mem_image.mp hv
+  cases done
+  · rw [start_eq]
+  · refine Relation.ReflTransGen.tail .refl (MultiTapePTM.viewStep_toNTM_iff.mpr ⟨true, ?_⟩)
+    rw [start_eq, step_view]
+    rfl
+
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+-- The same nonzero edge is read from actual compact IDs using the machine's zero-space bound.
+example :
+    let B := radix (radixExponent Unit 0) 0
+    (coinCountWithSymbol machine B 0 (vertexID B (view false)) (vertexID B (view true))
+      ([] : List Bool)[queryIndex (k := 0) B (vertexID B (view false))]? : ℚ) / 2 = 1 / 2 := by
+  classical
+  have hs : machine.toNTM.RunsInSpace [] (0 * (Nat.log2 ([] : List Bool).length + 1)) := by
+    rw [Nat.zero_mul]
+    exact MultiTapeNTM.runsInSpace_zero_tapes _ _ _
+  have hentry : timeLayer 2 loopMatrix (toLex (0, vertex false)) (toLex (1, vertex true)) =
+      1 / 2 := by
+    norm_num [timeLayer, loopMatrix, MultiTapePTM.configMatrix, Matrix.coinStepMatrix,
+      Fintype.sum_bool, vertex, step_view, view_injective.eq_iff]
+  have h := timeLayer_configMatrix_eq_coinCountWithSymbol_of_reachable (R := ℚ)
+    machine 0 hs reachable (T := 2) 0 1 (vertex false) (vertex true)
+  change timeLayer 2 loopMatrix (toLex (0, vertex false)) (toLex (1, vertex true)) = _ at h
+  rw [hentry] at h
+  exact h.symm
+
+end ComplexityTests.TimeLayer