diff --git a/Complexity.lean b/Complexity.lean
index fdd3b220c6..821e5b8a69 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1092,6 +1092,8 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.BPP
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.CompactMatrix
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.CompactTimeLayer
 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.PolyTime
@@ -1571,6 +1573,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Deterministic
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ReadInput
@@ -2795,6 +2798,7 @@ public import Complexity.Foundations.LinearAlgebra.ExchangeReplacement
 public import Complexity.Foundations.LinearAlgebra.ImageSparsification
 public import Complexity.Foundations.LinearAlgebra.Interpolation
 public import Complexity.Foundations.LinearAlgebra.KernelVector
+public import Complexity.Foundations.LinearAlgebra.Matrix.ClosedSubmatrix
 public import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep
 public import Complexity.Foundations.LinearAlgebra.Matrix.CopyStage
 public import Complexity.Foundations.LinearAlgebra.Matrix.CorrectionHierarchy
@@ -2810,6 +2814,7 @@ 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.TimeLayer.Fin
 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/CompactMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean
new file mode 100644
index 0000000000..5f7ba706cf
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean
@@ -0,0 +1,203 @@
+/-
+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.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.Table
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Deterministic
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Injective
+import Complexity.Foundations.LinearAlgebra.Matrix.ClosedSubmatrix
+
+/-!
+# Fair-coin matrices on the entire compact configuration box
+
+The matrix is indexed by every bounded compact ID, as enumerated by the initialized native
+`coinTable` writer. Invalid IDs have zero rows, and transitions leaving the box are omitted.
+Fixed-coin determinism makes every row substochastic, without a reachable-view premise.
+For a logarithmic-space run the box contains every reachable view; restriction to that closed
+image therefore proves exact finite-time acceptance for the ambient matrix.
+
+This supplies the enumerated base matrix of [OpenAI2026LogSpace, Lemma 2.1]. Clocking and the
+terminal reward are treated separately. Native clocked serialization, paired ports and the
+recursive estimator are not asserted here.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.ConfigurationGraph.compactCoinMatrix`: half the actual compact coin count.
+* `Turing.MultiTapePTM.ConfigurationGraph.compactAcceptVec`: the accepting-halt indicator.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.compactCoinMatrix_eq_coinTable`: exact native table
+  interpretation.
+* `Turing.MultiTapePTM.ConfigurationGraph.compactCoinMatrix_mulVec_one_le`: the entire matrix is
+  substochastic, including unreachable and invalid IDs.
+* `Turing.MultiTapePTM.ConfigurationGraph.compactCoinMatrix_pow_accept`: exact finite-time
+  acceptance on the ambient box, from the original logarithmic-space witness.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 2, Lemma 2.1, `model.tex` (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph Matrix
+
+variable {k : ℕ} {State : Type} [Fintype State] (machine : MultiTapePTM k Bool State)
+  (R : Type*) [Field R]
+
+/-- The actual fair-coin transition probabilities on every ID in the radix box. Invalid IDs
+and overflowing transitions have zero entries; coincident coin successors have weight one. -/
+@[expose] noncomputable def compactCoinMatrix (B : ℕ) (w : List Bool) :
+    Matrix (Fin (vertexBound (k := k) B)) (Fin (vertexBound (k := k) B)) R :=
+  fun u v => (coinCountWithSymbol machine B w.length u v
+    w[queryIndex (k := k) B u]? : R) / 2
+
+variable {machine}
+
+/-- The accepting-halt indicator on the entire box, with invalid IDs assigned zero. -/
+@[expose] noncomputable def compactAcceptVec (B n : ℕ) :
+    Fin (vertexBound (k := k) B) → R :=
+  fun u => if bad (k := k) (State := State) B n u then 1 else 0
+
+variable {R}
+
+/-- The two bits written by the initialized native table give this matrix entry exactly. -/
+theorem compactCoinMatrix_eq_coinTable (D : ℕ) (w : List Bool)
+    (u v : Fin (vertexBound (k := k) (radix D w.length))) :
+    compactCoinMatrix machine R (radix D w.length) w u v =
+      (((coinTable machine D w).getD
+          (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val)) false).toNat +
+        ((coinTable machine D w).getD
+          (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + 1)
+          false).toNat : ℕ) / 2 := by
+  rw [coinTable_count]
+  rfl
+
+section Ordered
+
+variable [LinearOrder R] [IsStrictOrderedRing R]
+
+/-- Every ambient entry is nonnegative. -/
+theorem compactCoinMatrix_nonneg (B : ℕ) (w : List Bool) :
+    ∀ u v, 0 ≤ compactCoinMatrix machine R B w u v := by
+  intro u v
+  unfold compactCoinMatrix
+  positivity
+
+/-- The ambient row sum is at most one. This includes malformed and unreachable sources and
+sources whose successor would overflow the radix. -/
+theorem compactCoinMatrix_mulVec_one_le (B : ℕ) (w : List Bool) :
+    compactCoinMatrix machine R B w *ᵥ 1 ≤ 1 := by
+  intro u
+  have hfalse := sum_edgeWithSymbol_le_one (machine.withCoin false).toTM B w.length u
+    w[queryIndex (k := k) B u]?
+  have htrue := sum_edgeWithSymbol_le_one (machine.withCoin true).toTM B w.length u
+    w[queryIndex (k := k) B u]?
+  have hcount : ∑ v : Fin (vertexBound (k := k) B),
+      coinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B u]? ≤ 2 := by
+    simp only [coinCountWithSymbol, Finset.sum_add_distrib]
+    omega
+  have hcast : (∑ v : Fin (vertexBound (k := k) B),
+      (coinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B u]? : R)) ≤ 2 := by
+    exact_mod_cast hcount
+  simpa only [mulVec, dotProduct, compactCoinMatrix, Pi.one_apply, mul_one,
+    ← Finset.sum_div] using (div_le_one (by norm_num : (0 : R) < 2)).mpr hcast
+
+/-- The accepting reward is bounded at every ambient ID. -/
+theorem compactAcceptVec_mem_Icc (B n : ℕ) :
+    compactAcceptVec (k := k) (State := State) R B n ∈ Set.Icc 0 1 := by
+  constructor <;> intro u <;> unfold compactAcceptVec <;> split_ifs <;> simp
+
+end Ordered
+
+variable (machine)
+
+/-- The actual initial compact ID at the standard logarithmic-space radix. The space witness
+derives the required bound internally; no separately supplied ID or fit premise is needed. -/
+@[expose] noncomputable def compactStart (c : ℕ) {w : List Bool}
+    (hs : machine.toNTM.RunsInSpace w (c * (Nat.log2 w.length + 1))) :
+    Fin (vertexBound (k := k) (radix (radixExponent State c) w.length)) :=
+  ⟨startID machine.toNTM (radix (radixExponent State c) w.length), by
+    rw [← vertexID_init machine.toNTM _ w]
+    exact vertexID_lt (fits_of_runsInSpace c hs .refl)⟩
+
+variable {machine}
+
+/-- The ambient compact matrix has exactly the machine's finite-time acceptance probability
+at its actual start. Only the original logarithmic-space witness is assumed; the finite reachable
+set, canonical representations, fit bounds and start-ID bound are all derived in the proof. -/
+theorem compactCoinMatrix_pow_accept (c : ℕ) {w : List Bool}
+    (hs : machine.toNTM.RunsInSpace w (c * (Nat.log2 w.length + 1))) (t : ℕ) :
+    let B := radix (radixExponent State c) w.length
+    (compactCoinMatrix machine R B w ^ t *ᵥ
+      compactAcceptVec (k := k) (State := State) R B w.length) (compactStart machine c hs) =
+        (machine.acceptCoins w t : R) / 2 ^ t := by
+  classical
+  let B := radix (radixExponent State c) w.length
+  obtain ⟨V, hreach, hclosedV, _⟩ := machine.exists_finset_reachable hs
+  have hinit : machine.toNTM.initView w ∈ V := (hreach _).mpr .refl
+  have hr (v : V) := (hreach v).mp v.property
+  have hinput (v : V) : v.val.input = w := input_of_reachable (hr v)
+  have hfit (v : V) : Fits B (registers v.val) := fits_of_runsInSpace c hs (hr v)
+  let e : V ↪ Fin (vertexBound (k := k) B) :=
+    ⟨fun v => ⟨vertexID B v.val, vertexID_lt (hfit v)⟩, by
+      intro v z hvz
+      apply Subtype.ext
+      exact vertexID_injective ((hinput v).trans (hinput z).symm)
+        (canonical_of_reachable machine (hr v)) (canonical_of_reachable machine (hr z))
+        (hfit v) (hfit z) (congrArg Fin.val hvz)⟩
+  have hclosed (v : V) (z : Fin (vertexBound (k := k) B)) (hz : z ∉ Set.range e) :
+      compactCoinMatrix machine R B w (e v) z = 0 := by
+    have hzero (bit : Bool) : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM
+        B w.length (vertexID B v.val) z w[queryIndex (k := k) B (vertexID B v.val)]? = false := by
+      apply Bool.eq_false_iff.mpr
+      intro hedge
+      have hedge' : Edge (machine.withCoin bit).toTM.toMultiTapeNTM B v.val.input
+          (vertexID B v.val) z := by
+        simpa only [Edge, hinput v] using hedge
+      obtain ⟨next, hstep, _, hid, _⟩ := edge_sound (hfit v) hedge'
+      have hnext := (viewStep_withCoin_iff machine bit).mp hstep
+      have hn : next ∈ V := (hreach next).mpr
+        ((hr v).tail (machine.viewStep_toNTM_iff.mpr ⟨bit, hnext⟩))
+      exact hz ⟨⟨next, hn⟩, Fin.ext hid.symm⟩
+    change (coinCountWithSymbol machine B w.length (vertexID B v.val) z
+      w[queryIndex (k := k) B (vertexID B v.val)]? : R) / 2 = 0
+    simp [coinCountWithSymbol, hzero]
+  have hmatrix : (compactCoinMatrix machine R B w).submatrix e e =
+      (2 : R)⁻¹ • machine.configMatrix R V := by
+    ext v z
+    change (coinCountWithSymbol machine B w.length (vertexID B v.val) (vertexID B z.val)
+      w[queryIndex (k := k) B (vertexID B v.val)]? : R) / 2 =
+        (2 : R)⁻¹ * machine.configMatrix R V v z
+    rw [coinCountWithSymbol_eq_configMatrix_of_reachable machine c hs
+      (fun v hv => (hreach v).mp hv) v z, div_eq_inv_mul]
+  have hreward : compactAcceptVec (k := k) (State := State) R B w.length ∘ e =
+      FiniteCfg.acceptVec R V := by
+    funext v
+    have hb := bad_vertexID (hfit v)
+    rw [hinput v] at hb
+    change (if bad (k := k) (State := State) B w.length (vertexID B v.val)
+      then (1 : R) else 0) = FiniteCfg.acceptVec R V v
+    simp only [hb, FiniteCfg.acceptVec]
+  have he : e ⟨machine.toNTM.initView w, hinit⟩ = compactStart machine c hs := by
+    apply Fin.ext
+    exact vertexID_init machine.toNTM B w
+  have hp := Matrix.submatrix_pow_mulVec_of_closed (compactCoinMatrix machine R B w) e
+    hclosed (compactAcceptVec (k := k) (State := State) R B w.length) t
+  rw [hmatrix, hreward] at hp
+  have hv := congrFun hp ⟨machine.toNTM.initView w, hinit⟩
+  rw [Function.comp_apply, he] at hv
+  exact hv.symm.trans
+    (machine.acceptCoins_div_eq_configMatrix_pow_mulVec R hclosedV hinit t).symm
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean
new file mode 100644
index 0000000000..3c2cd9c082
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean
@@ -0,0 +1,143 @@
+/-
+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.CompactMatrix
+public import Complexity.Foundations.LinearAlgebra.Matrix.TimeLayer.Fin
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds
+
+/-!
+# The clocked BPL matrix on consecutive compact identifiers
+
+The entire compact configuration box is clocked and indexed by the explicit integer
+`clock * vertexBound + baseID`. Its real-valued matrix is nonnegative, substochastic and strictly
+forward in that numeric order. Terminal rewards and the remaining-time potential satisfy the
+linear and inverse equations, with potential in `[0,1]` at every ID, and retain the actual BPL
+acceptance gap at the encoded initial configuration.
+
+The endpoint preserves the original logarithmic-space constant and derives the fitting radix
+from it. It does not choose an arbitrary ordering of reachable views. The ordinary entries are
+the counts written by the native initialized table, via `compactCoinMatrix_eq_coinTable`.
+Native clocked serialization, paired ports and the native recursive estimator remain open.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.finTimeLayer_compactCoinMatrix_acceptance`: clock-zero
+  acceptance for the explicit finite indexing and any horizon.
+* `Cslib.Complexity.exists_compactTimeLayer_of_mem_BPL`: the canonical polynomial-size
+  strict-forward real matrix with the actual `2/3` versus `1/3` BPL gap.
+
+## 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 Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph Matrix
+
+variable {k : ℕ} {State : Type} [Fintype State] {machine : MultiTapePTM k Bool State}
+  {R : Type*} [Field R]
+
+/-- Clocking the ambient compact matrix preserves the machine's actual finite-time acceptance
+probability at the explicit clock-zero start ID. -/
+theorem finTimeLayer_compactCoinMatrix_acceptance (c : ℕ) {w : List Bool}
+    (hs : machine.toNTM.RunsInSpace w (c * (Nat.log2 w.length + 1))) (T : ℕ) :
+    let B := radix (radixExponent State c) w.length
+    let N := vertexBound (k := k) B
+    finTimeLayerPotential T (compactCoinMatrix machine R B w)
+      (compactAcceptVec (k := k) (State := State) R B w.length)
+      ((timeLayerEquiv T N).symm (toLex (0, compactStart machine c hs))) =
+        (machine.acceptCoins w T : R) / 2 ^ T := by
+  dsimp only
+  rw [finTimeLayerPotential_zero, compactCoinMatrix_pow_accept]
+
+end Turing.MultiTapePTM.ConfigurationGraph
+
+namespace Cslib.Complexity
+
+open _root_.Turing MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph Matrix
+
+variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
+
+/-- **The enumerated clocked BPL matrix.** An actual BPL witness supplies one fixed machine,
+space constant and polynomial horizon. On every encoded word the full compact box, with numeric
+clock/base IDs, gives a real strict-forward substochastic matrix and a terminal reward whose
+bounded inverse potential has the original acceptance gap. The dimension is explicitly polynomial.
+
+The space witness is produced by this theorem, and all radix, start and representation bounds
+are derived from it. This is a semantic bridge for the existing initialized ordinary table;
+it does not assert native clocked serialization or incoming paired-port computation. -/
+theorem exists_compactTimeLayer_of_mem_BPL (h : A ∈ BPL enc) :
+    ∃ (k : ℕ) (State : Type) (_ : Fintype State) (M : MultiTapePTM k Bool State) (c d : ℕ),
+      ∀ a, ∃ hs : M.toNTM.RunsInSpace (enc a) (c * (Nat.log2 (enc a).length + 1)),
+        let w := enc a
+        let D := radixExponent State c
+        let B := radix D w.length
+        let N := vertexBound (k := k) B
+        let T := 2 * (2 * (w.length + 1)) ^ d
+        let P := compactCoinMatrix M ℝ B w
+        let e₀ := compactAcceptVec (k := k) (State := State) ℝ B w.length
+        let S := finTimeLayer T P
+        let e := finTimeLayerReward T e₀
+        let p := finTimeLayerPotential T P e₀
+        let x₀ := (timeLayerEquiv T N).symm (toLex (0, compactStart M c hs))
+        M.toNTM.RunsInTime w T ∧
+        Fintype.card (Fin ((T + 1) * N)) ≤
+          (2 * (w.length + 1)) ^ (D * Fintype.card (Register k) + d + 2) ∧
+        S.IsStrictUpperTriangular ∧ (∀ x y, 0 ≤ S x y) ∧ S *ᵥ 1 ≤ 1 ∧
+        (∀ x, e x = 0 ∨ e x = 1) ∧ (1 - S) *ᵥ p = e ∧ (1 - S)⁻¹ *ᵥ e = p ∧
+        p ∈ Set.Icc 0 1 ∧
+        (a ∈ A → 2 / 3 ≤ p x₀) ∧ (a ∉ A → p x₀ ≤ 1 / 3) := by
+  classical
+  obtain ⟨k, State, _, M, c, hM⟩ := h
+  let : Fintype State := Fintype.ofFinite State
+  obtain ⟨d, hd⟩ := M.toNTM.exists_runsInTime_polynomial_of_runsInSpace_log c
+  refine ⟨k, State, inferInstance, M, c, d, fun a => ?_⟩
+  obtain ⟨hs, t, ht, hmem, hnot⟩ := hM a
+  refine ⟨hs, ?_⟩
+  dsimp only
+  have hT := hd hs ht
+  have hP0 := compactCoinMatrix_nonneg (machine := M) (R := ℝ)
+    (radix (radixExponent State c) (enc a).length) (enc a)
+  have hP1 := compactCoinMatrix_mulVec_one_le (machine := M) (R := ℝ)
+    (radix (radixExponent State c) (enc a).length) (enc a)
+  refine ⟨hT, ?_, finTimeLayer_isStrictUpperTriangular _ _, finTimeLayer_nonneg hP0 _,
+    finTimeLayer_mulVec_one_le hP1 _, ?_, one_sub_finTimeLayer_mulVec _ _ _,
+    inv_one_sub_finTimeLayer_mulVec _ _ _,
+    finTimeLayerPotential_mem_Icc hP0 hP1 (compactAcceptVec_mem_Icc _ _) _, ?_, ?_⟩
+  · rw [Fintype.card_fin]
+    exact (Nat.le_succ _).trans (clockedVertexBound_add_one_le_pow
+      (k := k) (radixExponent State c) d (enc a).length)
+  · intro x
+    unfold finTimeLayerReward timeLayerReward compactAcceptVec
+    dsimp only [Function.comp_apply]
+    split_ifs <;> simp
+  · intro ha
+    rw [finTimeLayer_compactCoinMatrix_acceptance]
+    have hn := (M.two_pow_mul_le_iff ht hT 2 3).mp (hmem ha)
+    have hc : (2 : ℝ) * 2 ^ (2 * (2 * ((enc a).length + 1)) ^ d) ≤
+        3 * (M.acceptCoins (enc a) (2 * (2 * ((enc a).length + 1)) ^ d) : ℝ) := by
+      exact_mod_cast hn
+    rw [le_div_iff₀ (by positivity)]
+    linarith
+  · intro ha
+    rw [finTimeLayer_compactCoinMatrix_acceptance]
+    have hn := (M.mul_le_two_pow_iff ht hT 1 3).mp (by simpa only [one_mul] using hnot ha)
+    simp only [one_mul] at hn
+    have hc : (3 : ℝ) * (M.acceptCoins (enc a) (2 * (2 * ((enc a).length + 1)) ^ d) : ℝ) ≤
+        2 ^ (2 * (2 * ((enc a).length + 1)) ^ d) := by
+      exact_mod_cast hn
+    rw [div_le_iff₀ (by positivity)]
+    linarith
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean
index 9ba13cdb2e..5b166e91a6 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean
@@ -146,7 +146,8 @@ theorem liveCoinCountWithSymbol_eq_liveConfigMatrix {B : ℕ}
     exact coinCountWithSymbol_eq_configMatrix (R := R) machine x y hinput hx hy hfitX hfitY
 
 omit [Fintype State] in
-private theorem canonical_of_reachable {input : List Bool} {v : FiniteCfg k Bool State}
+/-- Every view reachable from the initial view already has its canonical output summary. -/
+theorem canonical_of_reachable {input : List Bool} {v : FiniteCfg k Bool State}
     (hv : Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v) :
     outputClass v.output = v.output := by
   obtain ⟨p, hrep⟩ := exists_computationPath_of_viewStep hv
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean
index a018b8f44c..fe1455f737 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean
@@ -20,6 +20,8 @@ and ternary symbol/count scratch register in terms of the length of the framed i
 ## Main results
 
 * `Turing.MultiTapeNTM.ConfigurationGraph.configurationCounter_bounds`: the standard counter bound.
+* `Turing.MultiTapeNTM.ConfigurationGraph.clockedVertexBound_add_one_le_pow`: the clocked box
+  and its final counter value have a fixed polynomial bound.
 -/
 
 public section
@@ -48,4 +50,26 @@ theorem configurationCounter_bounds {k : ℕ} (D : ℕ) (w : List Bool) :
   rw [hB]
   exact ⟨by omega, by omega, by omega⟩
 
+/-- With the standard polynomial horizon, the full clocked compact box plus one is bounded by
+a fixed power of `2 * (n + 1)`, including at the empty input and zero exponents. -/
+theorem clockedVertexBound_add_one_le_pow {k : ℕ} (D d n : ℕ) :
+    (2 * (2 * (n + 1)) ^ d + 1) * vertexBound (k := k) (radix D n) + 1 ≤
+      (2 * (n + 1)) ^ (D * Fintype.card (Register k) + d + 2) := by
+  let F := 2 * (n + 1)
+  let E := D * Fintype.card (Register k)
+  have hF : 2 ≤ F := by dsimp [F]; omega
+  have hN : vertexBound (k := k) (radix D n) ≤ F ^ E := by
+    rw [vertexBound_eq_pow]
+    exact Nat.pow_le_pow_left (by dsimp [F]; omega) E
+  have hE : 1 ≤ F ^ E := Nat.one_le_pow _ _ (by omega)
+  have hd : 1 ≤ F ^ d := Nat.one_le_pow _ _ (by omega)
+  change (2 * F ^ d + 1) * vertexBound (k := k) (radix D n) + 1 ≤ F ^ (E + d + 2)
+  calc
+    _ ≤ (2 * F ^ d + 1) * F ^ E + 1 :=
+      Nat.add_le_add_right (Nat.mul_le_mul_left _ hN) 1
+    _ ≤ (F ^ E * F ^ d) * 4 := by nlinarith
+    _ ≤ (F ^ E * F ^ d) * F ^ 2 :=
+      Nat.mul_le_mul_left _ (by nlinarith [sq_nonneg (F - 2 : ℤ)])
+    _ = F ^ (E + d + 2) := by rw [pow_add, pow_add]
+
 end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Deterministic.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Deterministic.lean
new file mode 100644
index 0000000000..3da55e10c5
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Deterministic.lean
@@ -0,0 +1,94 @@
+/-
+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.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
+
+/-!
+# Deterministic edges throughout the compact configuration box
+
+The guarded compact graph of a deterministic machine has at most one successor at every ID,
+including invalid and unreachable IDs. This does not require a decoder or a represented-view
+hypothesis. It follows directly from the fixed transition table and injective observation codes.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.edgeWithSymbol_target_unique`: target uniqueness for
+  the compact graph of a deterministic machine.
+* `Turing.MultiTapeNTM.ConfigurationGraph.sum_edgeWithSymbol_le_one`: each indicator row has
+  total mass at most one, including rows truncated by the radix bound.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+private theorem matchesEntry_observations {n : ℕ} {r : Register k → ℕ}
+    {symbol : Option Bool} {a b : Instruction k State}
+    (ha : matchesEntry n r symbol a = true) (hb : matchesEntry n r symbol b = true) :
+    a.1 = b.1 ∧ a.2.1 = b.2.1 ∧ a.2.2.1 = b.2.2.1 := by
+  simp only [matchesEntry, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true,
+    List.mem_ofFn, id_eq] at ha hb
+  refine ⟨Option.some.inj (stateCode_injective (ha.1.1.symm.trans hb.1.1)),
+    ha.1.2.symm.trans hb.1.2, funext fun i => ?_⟩
+  exact symbolCode_injective
+    ((of_decide_eq_true (ha.2 _ ⟨i, rfl⟩)).symm.trans (of_decide_eq_true (hb.2 _ ⟨i, rfl⟩)))
+
+/-- The compact graph of a deterministic machine has at most one target for each source and
+supplied input symbol. The statement includes all IDs, with no validity or reachability premise. -/
+theorem edgeWithSymbol_target_unique (tm : MultiTapeTM k Bool State)
+    {B n u v z : ℕ} {symbol : Option Bool}
+    (hv : edgeWithSymbol tm.toMultiTapeNTM B n u v symbol = true)
+    (hz : edgeWithSymbol tm.toMultiTapeNTM B n u z symbol = true) : v = z := by
+  simp only [edgeWithSymbol, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
+    List.any_eq_true] at hv hz
+  rcases hv.2 with hv | ⟨a, ha, ⟨⟨hma, _⟩, hv⟩⟩
+  · rcases hz.2 with hz | ⟨b, _, ⟨⟨hmb, _⟩, _⟩⟩
+    · exact hv.2.trans hz.2.symm
+    · simp only [matchesEntry, Bool.and_eq_true, decide_eq_true_eq] at hmb
+      have h := stateCode_injective (hv.1.symm.trans hmb.1.1)
+      cases h
+  · rcases hz.2 with hz | ⟨b, hb, ⟨⟨hmb, _⟩, hz⟩⟩
+    · simp only [matchesEntry, Bool.and_eq_true, decide_eq_true_eq] at hma
+      have h := stateCode_injective (hz.1.symm.trans hma.1.1)
+      cases h
+    · obtain ⟨hq, hi, hw⟩ := matchesEntry_observations hma hmb
+      have hta := MultiTapeTM.tr_iff.mp ((mem_instructions tm.toMultiTapeNTM a).mp ha)
+      have htb := MultiTapeTM.tr_iff.mp ((mem_instructions tm.toMultiTapeNTM b).mp hb)
+      rw [hq, hi, hw] at hta
+      have haction := hta.symm.trans htb
+      rw [haction] at hv
+      exact hv.trans hz.symm
+
+/-- Summing a deterministic edge indicator over the entire compact box gives at most one.
+Invalid IDs and radix-overflowing transitions may give a row of zeros. -/
+theorem sum_edgeWithSymbol_le_one (tm : MultiTapeTM k Bool State)
+    (B n u : ℕ) (symbol : Option Bool) :
+    ∑ v : Fin (vertexBound (k := k) B),
+      (edgeWithSymbol tm.toMultiTapeNTM B n u v symbol).toNat ≤ 1 := by
+  classical
+  by_cases h : ∃ v : Fin (vertexBound (k := k) B),
+      edgeWithSymbol tm.toMultiTapeNTM B n u v symbol = true
+  · obtain ⟨v, hv⟩ := h
+    rw [Finset.sum_eq_single v]
+    · simp [hv]
+    · intro z _ hz
+      have he : edgeWithSymbol tm.toMultiTapeNTM B n u z symbol = false := by
+        apply Bool.eq_false_iff.mpr
+        intro he
+        exact hz (Fin.ext (edgeWithSymbol_target_unique tm he hv))
+      simp [he]
+    · simp
+  · have he (v : Fin (vertexBound (k := k) B)) :
+        edgeWithSymbol tm.toMultiTapeNTM B n u v symbol = false :=
+      Bool.eq_false_iff.mpr fun hv => h ⟨v, hv⟩
+    simp [he]
+
+end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/ClosedSubmatrix.lean b/Complexity/Foundations/LinearAlgebra/Matrix/ClosedSubmatrix.lean
new file mode 100644
index 0000000000..fa64fe2b2e
--- /dev/null
+++ b/Complexity/Foundations/LinearAlgebra/Matrix/ClosedSubmatrix.lean
@@ -0,0 +1,53 @@
+/-
+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.Init
+public import Mathlib.Data.Matrix.Mul
+
+/-!
+# Matrix powers on a closed set of indices
+
+An injectively indexed submatrix preserves matrix-vector products and their iterates when rows
+in the image have zero entries outside it. The ambient vector may take arbitrary values outside
+the image. This is the restriction principle used to compare reachable configuration matrices
+with an explicitly enumerated ambient box.
+
+## Main results
+
+* `Matrix.submatrix_mulVec_of_closed`: one multiplication commutes with restriction.
+* `Matrix.submatrix_pow_mulVec_of_closed`: so do all matrix powers.
+-/
+
+public section
+
+namespace Matrix
+
+variable {ι κ R : Type*} [Fintype ι] [Fintype κ] [Semiring R]
+
+/-- Restricting to an injectively indexed set of rows commutes with matrix-vector multiplication
+if those rows have no nonzero entries outside the indexed set. -/
+theorem submatrix_mulVec_of_closed (M : Matrix κ κ R) (e : ι ↪ κ)
+    (hclosed : ∀ i j, j ∉ Set.range e → M (e i) j = 0) (v : κ → R) :
+    M.submatrix e e *ᵥ (v ∘ e) = (M *ᵥ v) ∘ e := by
+  ext i
+  exact Fintype.sum_of_injective e e.injective
+    (fun j => M (e i) (e j) * v (e j)) (fun j => M (e i) j * v j)
+    (fun j hj => by rw [hclosed i j hj, zero_mul]) (fun _ => rfl)
+
+/-- Every power preserves restriction to a set with no outgoing nonzero matrix entries. -/
+theorem submatrix_pow_mulVec_of_closed [DecidableEq ι] [DecidableEq κ]
+    (M : Matrix κ κ R) (e : ι ↪ κ)
+    (hclosed : ∀ i j, j ∉ Set.range e → M (e i) j = 0) (v : κ → R) (t : ℕ) :
+    M.submatrix e e ^ t *ᵥ (v ∘ e) = (M ^ t *ᵥ v) ∘ e := by
+  induction t with
+  | zero => simp
+  | succ t ih =>
+    simp only [pow_succ', ← mulVec_mulVec, ih, submatrix_mulVec_of_closed M e hclosed]
+
+end Matrix
diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer/Fin.lean b/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer/Fin.lean
new file mode 100644
index 0000000000..512254f8b3
--- /dev/null
+++ b/Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer/Fin.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.LinearAlgebra.Matrix.TimeLayer
+
+/-!
+# Time layers with consecutive natural-number identifiers
+
+Reindex `Matrix.timeLayer` on `Fin ((T + 1) * n)` by the identifier `i * n + u` for clock `i`
+and base vertex `u`. Division and remainder recover the two components. The order, row bound,
+linear system and inverse formula are transported from the existing time-layer construction.
+
+## Main definitions
+
+* `Matrix.timeLayerEquiv`: the explicit clock/base equivalence.
+* `Matrix.finTimeLayer`, `Matrix.finTimeLayerReward`, `Matrix.finTimeLayerPotential`: the
+  existing time-layer construction on consecutive finite identifiers.
+
+## Main results
+
+* `Matrix.finTimeLayer_isStrictUpperTriangular`: numeric order is the forward clock order.
+* `Matrix.finTimeLayer_mulVec_one_le`, `Matrix.finTimeLayerPotential_mem_Icc`: global bounds.
+* `Matrix.one_sub_finTimeLayer_mulVec`, `Matrix.inv_one_sub_finTimeLayer_mulVec`: exact equations.
+-/
+
+public section
+
+namespace Matrix
+
+variable {n : ℕ} {R : Type*}
+
+/-- Split a consecutive identifier into its clock and base vertex. -/
+@[expose] def timeLayerEquiv (T n : ℕ) :
+    Fin ((T + 1) * n) ≃ Lex (Fin (T + 1) × Fin n) :=
+  finProdFinEquiv.symm.trans toLex
+
+/-- The clock is the quotient and the base vertex is the remainder. -/
+theorem timeLayerEquiv_apply (T n : ℕ) (a : Fin ((T + 1) * n)) :
+    timeLayerEquiv T n a = toLex (a.divNat, a.modNat) := rfl
+
+/-- The identifier has the usual row-major arithmetic value. -/
+theorem timeLayerEquiv_val (T n : ℕ) (a : Fin ((T + 1) * n)) :
+    a.val = (ofLex (timeLayerEquiv T n a)).2.val +
+      n * (ofLex (timeLayerEquiv T n a)).1.val := by
+  have h := finProdFinEquiv_apply_val (ofLex (timeLayerEquiv T n a))
+  simp only [timeLayerEquiv, Equiv.trans_apply, ofLex_toLex, Equiv.apply_symm_apply] at h
+  exact h
+
+/-- Numeric identifiers reflect the clock-then-base lexicographic order. -/
+theorem timeLayerEquiv_lt (T n : ℕ) {a b : Fin ((T + 1) * n)}
+    (h : timeLayerEquiv T n a < timeLayerEquiv T n b) : a < b := by
+  rw [Fin.lt_def, timeLayerEquiv_val T n a, timeLayerEquiv_val T n b]
+  rcases Prod.Lex.lt_iff.mp h with hclock | ⟨hclock, hbase⟩
+  · have hc : (ofLex (timeLayerEquiv T n a)).1.val + 1 ≤
+        (ofLex (timeLayerEquiv T n b)).1.val := hclock
+    have hb := (ofLex (timeLayerEquiv T n a)).2.isLt
+    nlinarith
+  · rw [hclock]
+    exact Nat.add_lt_add_right hbase _
+
+/-- The existing clocked matrix, indexed consecutively by clock then base vertex. -/
+@[expose] def finTimeLayer [Zero R] (T : ℕ) (P : Matrix (Fin n) (Fin n) R) :
+    Matrix (Fin ((T + 1) * n)) (Fin ((T + 1) * n)) R :=
+  (timeLayer T P).submatrix (timeLayerEquiv T n) (timeLayerEquiv T n)
+
+/-- The existing terminal reward on consecutive identifiers. -/
+@[expose] def finTimeLayerReward [Zero R] (T : ℕ) (e : Fin n → R) :
+    Fin ((T + 1) * n) → R := timeLayerReward T e ∘ timeLayerEquiv T n
+
+/-- The existing remaining-time potential on consecutive identifiers. -/
+@[expose] def finTimeLayerPotential [Semiring R] (T : ℕ)
+    (P : Matrix (Fin n) (Fin n) R) (e : Fin n → R) : Fin ((T + 1) * n) → R :=
+  timeLayerPotential T P e ∘ timeLayerEquiv T n
+
+/-- A finite-index entry tests the next clock and then uses the two base remainders. -/
+theorem finTimeLayer_apply [Zero R] (T : ℕ) (P : Matrix (Fin n) (Fin n) R)
+    (a b : Fin ((T + 1) * n)) : finTimeLayer T P a b =
+      if a.val / n + 1 = b.val / n then P a.modNat b.modNat else 0 := rfl
+
+/-- Numeric order gives strict forwardness for the reindexed matrix. -/
+theorem finTimeLayer_isStrictUpperTriangular [Zero R] (T : ℕ)
+    (P : Matrix (Fin n) (Fin n) R) : (finTimeLayer T P).IsStrictUpperTriangular := by
+  intro a b hab
+  exact timeLayer_isStrictUpperTriangular T P (fun h => hab (timeLayerEquiv_lt T n h))
+
+/-- Nonnegativity is preserved by the explicit reindexing. -/
+theorem finTimeLayer_nonneg [Zero R] [Preorder R] {P : Matrix (Fin n) (Fin n) R}
+    (hP : ∀ a b, 0 ≤ P a b) (T : ℕ) : ∀ a b, 0 ≤ finTimeLayer T P a b :=
+  fun a b => timeLayer_nonneg hP T (timeLayerEquiv T n a) (timeLayerEquiv T n b)
+
+/-- Clocking and explicit reindexing preserve the substochastic row bound. -/
+theorem finTimeLayer_mulVec_one_le [Semiring R] [PartialOrder R] [IsOrderedRing R]
+    {P : Matrix (Fin n) (Fin n) R} (hP : P *ᵥ 1 ≤ 1) (T : ℕ) :
+    finTimeLayer T P *ᵥ 1 ≤ 1 := by
+  intro a
+  rw [finTimeLayer, submatrix_mulVec_equiv]
+  exact timeLayer_mulVec_one_le hP T (timeLayerEquiv T n a)
+
+/-- The finite-index potential is bounded at every clock and base identifier. -/
+theorem finTimeLayerPotential_mem_Icc [Semiring R] [PartialOrder R] [IsOrderedRing R]
+    {P : Matrix (Fin n) (Fin n) R} {e : Fin n → R} (hP0 : ∀ a b, 0 ≤ P a b)
+    (hP1 : P *ᵥ 1 ≤ 1) (he : e ∈ Set.Icc 0 1) (T : ℕ) :
+    finTimeLayerPotential T P e ∈ Set.Icc 0 1 := by
+  have h := timeLayerPotential_mem_Icc hP0 hP1 he T
+  exact ⟨fun a => h.1 (timeLayerEquiv T n a), fun a => h.2 (timeLayerEquiv T n a)⟩
+
+/-- At clock zero, the potential is the original terminal expectation. -/
+theorem finTimeLayerPotential_zero [Semiring R] (T : ℕ) (P : Matrix (Fin n) (Fin n) R)
+    (e : Fin n → R) (x : Fin n) :
+    finTimeLayerPotential T P e ((timeLayerEquiv T n).symm (toLex (0, x))) =
+      (P ^ T *ᵥ e) x := by
+  rw [finTimeLayerPotential, Function.comp_apply, Equiv.apply_symm_apply,
+    timeLayerPotential_zero]
+
+private theorem one_sub_finTimeLayer [Ring R] (T : ℕ) (P : Matrix (Fin n) (Fin n) R) :
+    1 - finTimeLayer T P =
+      (1 - timeLayer T P).submatrix (timeLayerEquiv T n) (timeLayerEquiv T n) := by
+  simp only [submatrix_sub, Pi.sub_apply, submatrix_one_equiv, finTimeLayer]
+
+/-- The finite-index potential solves the same terminal-reward linear system. -/
+theorem one_sub_finTimeLayer_mulVec [Ring R] (T : ℕ) (P : Matrix (Fin n) (Fin n) R)
+    (e : Fin n → R) :
+    (1 - finTimeLayer T P) *ᵥ finTimeLayerPotential T P e = finTimeLayerReward T e := by
+  rw [one_sub_finTimeLayer, submatrix_mulVec_equiv]
+  simpa only [finTimeLayerPotential, finTimeLayerReward, Function.comp_def,
+    Equiv.apply_symm_apply] using
+    congrArg (fun f => f ∘ timeLayerEquiv T n) (one_sub_timeLayer_mulVec T P e)
+
+/-- The inverse-matrix formula is preserved by the explicit finite reindexing. -/
+theorem inv_one_sub_finTimeLayer_mulVec [CommRing R] (T : ℕ)
+    (P : Matrix (Fin n) (Fin n) R) (e : Fin n → R) :
+    (1 - finTimeLayer T P)⁻¹ *ᵥ finTimeLayerReward T e = finTimeLayerPotential T P e := by
+  rw [one_sub_finTimeLayer, inv_submatrix_equiv, submatrix_mulVec_equiv]
+  simpa only [finTimeLayerReward, finTimeLayerPotential, Function.comp_def,
+    Equiv.apply_symm_apply] using
+    congrArg (fun f => f ∘ timeLayerEquiv T n) (inv_one_sub_timeLayer_mulVec T P e)
+
+end Matrix
diff --git a/ComplexityTests/CompactConfigurationMatrix.lean b/ComplexityTests/CompactConfigurationMatrix.lean
new file mode 100644
index 0000000000..0c3fbbaaaf
--- /dev/null
+++ b/ComplexityTests/CompactConfigurationMatrix.lean
@@ -0,0 +1,245 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.CompactTimeLayer
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification
+import Mathlib.Tactic.NormNum
+
+/-!
+# Compact ambient matrix and numeric clock regressions
+
+A zero-work-tape machine outputs its coin and halts. Its actual acceptance probability is one
+half. At radix two, the rejecting output tag overflows, so the ambient row has mass one half;
+it is not falsely claimed stochastic. A radix-three ID with an invalid control tag has a zero
+row and zero reward. Numeric time layers advance the clock and pay only at the terminal layer.
+The always-accepting variant also discharges the complete BPL witness hypotheses.
+
+The one-coin replay and halting proof follow the concrete fixture in `RandomizedLogSpace`.
+-/
+
+namespace ComplexityTests.CompactConfigurationMatrix
+
+open Cslib Turing MultiTapeTM Matrix
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+private def machine (always : Bool) : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ _ _ _ bit :=
+    .step { inputTape := 0, workTapes := Fin.elim0, output := some (always || bit), state := none }
+      Empty.elim Empty.elim
+
+private theorem stepCoins (always : Bool) (input : List Bool) (bit : Bool) :
+    (machine always).stepCoins [bit] ((machine always).toNTM.initCfg input) =
+      ⟨none, 1, Fin.elim0, Fin.elim0, [always || bit]⟩ := by
+  rw [MultiTapePTM.initCfg_toNTM, ← MultiTapePTM.tapes_runClosedConfigFromCoins]
+  exact Cfg.ext_zero_tapes rfl rfl rfl
+
+private theorem timeBound (always : Bool) (input : List Bool) :
+    (machine always).toNTM.RunsInTime input 1 := by
+  refine (MultiTapePTM.runsInTime_toNTM_iff _).mpr fun final hfinal => ?_
+  rw [MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins] at hfinal
+  obtain ⟨coins, hcoins, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp hfinal
+  obtain ⟨bit, rfl⟩ : ∃ bit, coins = [bit] := by
+    rw [BitString.mem_support_uniformList_iff, List.length_eq_one_iff] at hcoins
+    exact hcoins
+  rw [MultiTapePTM.tapes_runClosedConfigFromCoins]
+  exact congrArg Cfg.state (stepCoins always input bit)
+
+private theorem accept_one (input : List Bool) : (machine false).acceptCoins input 1 = 1 := by
+  rw [MultiTapePTM.acceptCoins, Finset.card_eq_one]
+  refine ⟨fun _ => true, Finset.ext fun w => ?_⟩
+  have hw : List.ofFn w = [w 0] := by simp
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton, hw, stepCoins]
+  refine ⟨fun h => funext fun i => ?_, fun h => ?_⟩
+  · rw [Fin.fin_one_eq_zero i]
+    simpa using h
+  · subst h
+    simp
+
+private theorem accept_two (input : List Bool) : (machine true).acceptCoins input 1 = 2 := by
+  have h (w : Fin 1 → Bool) :
+      ((machine true).stepCoins (List.ofFn w) ((machine true).toNTM.initCfg input)).Halted ∧
+        ((machine true).stepCoins (List.ofFn w) ((machine true).toNTM.initCfg input)).output =
+          [true] := by
+    have hw : List.ofFn w = [w 0] := by simp
+    rw [hw, stepCoins]
+    simp [Cfg.Halted]
+  rw [MultiTapePTM.acceptCoins, Finset.filter_eq_self.mpr (fun w _ => h w)]
+  simp
+
+private theorem spaceBound (always : Bool) (input : List Bool) :
+    (machine always).toNTM.RunsInSpace input (0 * (Nat.log2 input.length + 1)) := by
+  rw [Nat.zero_mul]
+  exact MultiTapeNTM.runsInSpace_zero_tapes _ _ _
+
+-- The full (large) canonical box gives the actual probability without summing its rows by hand.
+example (input : List Bool) :
+    let B := radix (radixExponent Unit 0) input.length
+    (compactCoinMatrix (machine false) ℚ B input ^ 1 *ᵥ
+      compactAcceptVec (k := 0) (State := Unit) ℚ B input.length)
+      (compactStart (machine false) 0 (spaceBound false input)) = 1 / 2 := by
+  dsimp only
+  rw [compactCoinMatrix_pow_accept, accept_one]
+  norm_num
+
+example (input : List Bool) :
+    let B := radix (radixExponent Unit 0) input.length
+    let N := vertexBound (k := 0) B
+    finTimeLayerPotential 1 (compactCoinMatrix (machine false) ℝ B input)
+      (compactAcceptVec (k := 0) (State := Unit) ℝ B input.length)
+      ((timeLayerEquiv 1 N).symm (toLex (0, compactStart (machine false) 0
+        (spaceBound false input)))) = 1 / 2 := by
+  dsimp only
+  rw [finTimeLayer_compactCoinMatrix_acceptance, accept_one]
+  norm_num
+
+private def malformedRegisters : Register 0 → ℕ
+  | .control => 2
+  | _ => 0
+
+private theorem malformedFits : Fits 3 malformedRegisters := by
+  intro i
+  cases i <;> simp [malformedRegisters]
+
+private noncomputable def malformed : Fin (vertexBound (k := 0) 3) :=
+  ⟨Radix.pack 3 malformedRegisters, Radix.pack_lt (by decide) malformedFits⟩
+
+private theorem malformed_read : readRegisters 3 malformed = malformedRegisters := by
+  funext i
+  exact Radix.component_pack (by decide) malformedFits i
+
+private theorem malformed_invalid : valid (k := 0) (State := Unit) 3 0 malformed = false := by
+  simp [valid, malformed_read, malformedRegisters]
+
+-- This invalid source lies inside the ambient box; out-of-range guards alone would miss it.
+example (v : Fin (vertexBound (k := 0) 3)) :
+    compactCoinMatrix (machine false) ℚ 3 [] malformed v = 0 ∧
+      compactAcceptVec (k := 0) (State := Unit) ℚ 3 0 malformed = 0 := by
+  simp [compactCoinMatrix, coinCountWithSymbol, edgeWithSymbol, malformed_invalid,
+    compactAcceptVec, bad]
+
+private def initial : FiniteCfg 0 Bool Unit := ⟨[], some (), 1, Fin.elim0, []⟩
+private def stopped (bit : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨[], none, 1, Fin.elim0, [bit]⟩
+
+private theorem step_initial (bit : Bool) :
+    (machine false).viewCoinStep initial bit = stopped bit := by
+  cases bit <;>
+    simp [MultiTapePTM.viewCoinStep, machine, initial, stopped, MultiTapePTM.withCoin,
+      MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv, FiniteCfg.step,
+      FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, funext_iff]
+
+private theorem initial_fits : Fits 2 (registers initial) := by
+  intro i
+  cases i with
+  | inputPos => decide
+  | control => exact (Fintype.equivFin (Option Unit) (some ())).isLt
+  | output => decide
+  | head i => exact Fin.elim0 i
+  | left i => exact Fin.elim0 i
+  | right i => exact Fin.elim0 i
+
+private theorem accept_fits : Fits 2 (registers (stopped true)) := by
+  intro i
+  cases i with
+  | inputPos => decide
+  | control => exact (Fintype.equivFin (Option Unit) none).isLt
+  | output => decide
+  | head i => exact Fin.elim0 i
+  | left i => exact Fin.elim0 i
+  | right i => exact Fin.elim0 i
+
+private noncomputable def source : Fin (vertexBound (k := 0) 2) :=
+  ⟨vertexID 2 initial, vertexID_lt initial_fits⟩
+private noncomputable def accepting : Fin (vertexBound (k := 0) 2) :=
+  ⟨vertexID 2 (stopped true), vertexID_lt accept_fits⟩
+
+private theorem accepting_entry :
+    compactCoinMatrix (machine false) ℚ 2 [] source accepting = 1 / 2 := by
+  have hcoin (bit : Bool) := edgeWithSymbol_withCoin_iff (machine false)
+    (a := initial) (b := stopped true) rfl
+    (by simp [initial, MultiTapeNTM.outputClass])
+    (by simp [stopped, MultiTapeNTM.outputClass]) initial_fits accept_fits bit
+  simp only [step_initial] at hcoin
+  have ht := (hcoin true).mpr rfl
+  have hf : edgeWithSymbol ((machine false).withCoin false).toTM.toMultiTapeNTM
+      2 0 source accepting ([] : List Bool)[queryIndex (k := 0) 2 source]? = false := by
+    apply Bool.eq_false_iff.mpr
+    intro he
+    have ho := congrArg FiniteCfg.output ((hcoin false).mp he)
+    simp [stopped] at ho
+  change edgeWithSymbol ((machine false).withCoin false).toTM.toMultiTapeNTM
+    2 0 source accepting none = false at hf
+  change edgeWithSymbol ((machine false).withCoin true).toTM.toMultiTapeNTM
+    2 0 source accepting none = true at ht
+  change ((edgeWithSymbol ((machine false).withCoin false).toTM.toMultiTapeNTM
+      2 0 source accepting none).toNat +
+    (edgeWithSymbol ((machine false).withCoin true).toTM.toMultiTapeNTM
+      2 0 source accepting none).toNat : ℕ) / 2 = (1 / 2 : ℚ)
+  rw [hf, ht]
+  norm_num
+
+private theorem other_entry (v : Fin (vertexBound (k := 0) 2)) (hv : v ≠ accepting) :
+    compactCoinMatrix (machine false) ℚ 2 [] source v = 0 := by
+  have hzero (bit : Bool) : edgeWithSymbol ((machine false).withCoin bit).toTM.toMultiTapeNTM
+      2 0 source v ([] : List Bool)[queryIndex (k := 0) 2 source]? = false := by
+    apply Bool.eq_false_iff.mpr
+    intro he
+    obtain ⟨next, hstep, _, hid, hfit⟩ := edge_sound initial_fits he
+    have hn := (MultiTapePTM.viewStep_withCoin_iff (machine false) bit).mp hstep
+    rw [step_initial] at hn
+    subst next
+    cases bit
+    · have hbad := hfit .output
+      norm_num [registers, stopped, outputCode] at hbad
+    · exact hv (Fin.ext hid)
+  simp only [List.getElem?_nil] at hzero
+  simp [compactCoinMatrix, coinCountWithSymbol, hzero]
+
+-- The false branch leaves radix two through output tag 2; exactly one half of the row remains.
+example : (compactCoinMatrix (machine false) ℚ 2 [] *ᵥ 1) source = 1 / 2 := by
+  classical
+  rw [mulVec, dotProduct, Finset.sum_eq_single accepting]
+  · simpa only [Pi.one_apply, mul_one] using accepting_entry
+  · intro v _ hv
+    rw [other_entry v hv, zero_mul]
+  · simp
+
+-- The finite clock layout is quotient/remainder arithmetic, including a terminal index.
+example : timeLayerEquiv 2 8 (17 : Fin 24) = toLex ((2 : Fin 3), (1 : Fin 8)) := rfl
+
+example :
+    let P := compactCoinMatrix (machine false) ℚ 2 []
+    let E := timeLayerEquiv 2 (vertexBound (k := 0) 2)
+    finTimeLayer 2 P (E.symm (toLex (0, source))) (E.symm (toLex (1, accepting))) = 1 / 2 ∧
+      finTimeLayer 2 P (E.symm (toLex (0, source))) (E.symm (toLex (0, accepting))) = 0 ∧
+      finTimeLayer 2 P (E.symm (toLex (2, accepting))) (E.symm (toLex (0, source))) = 0 := by
+  simp [finTimeLayer, timeLayer, accepting_entry]
+
+example :
+    let e := compactAcceptVec (k := 0) (State := Unit) ℚ 2 0
+    let E := timeLayerEquiv 2 (vertexBound (k := 0) 2)
+    finTimeLayerReward 2 e (E.symm (toLex (1, accepting))) = 0 ∧
+      finTimeLayerReward 2 e (E.symm (toLex (2, accepting))) = 1 := by
+  have hb := (bad_vertexID accept_fits).mpr (by simp [stopped])
+  change bad (k := 0) (State := Unit) 2 0 (vertexID 2 (stopped true)) = true at hb
+  simp [finTimeLayerReward, timeLayerReward, compactAcceptVec, accepting, hb]
+
+-- A concrete always-accepting machine supplies all the class theorem's assumptions.
+private theorem univ_mem_BPL :
+    (Set.univ : Set (List Bool)) ∈ Complexity.BPL encBits := by
+  refine ⟨0, Unit, inferInstance, machine true, 0, fun input =>
+    ⟨spaceBound true input, 1, timeBound true input, fun _ => ?_, fun h => False.elim (h trivial)⟩⟩
+  rw [accept_two]
+  norm_num
+
+example : ∃ (N : ℕ) (S : Matrix (Fin N) (Fin N) ℝ) (e p : Fin N → ℝ) (x : Fin N),
+    S.IsStrictUpperTriangular ∧ (1 - S)⁻¹ *ᵥ e = p ∧ p ∈ Set.Icc 0 1 ∧ 2 / 3 ≤ p x := by
+  obtain ⟨k, State, _, M, c, d, hM⟩ := Complexity.exists_compactTimeLayer_of_mem_BPL univ_mem_BPL
+  obtain ⟨hs, _, _, hS, _, _, _, _, hinv, hp, hyes, _⟩ := hM []
+  exact ⟨_, _, _, _, _, hS, hinv, hp, hyes trivial⟩
+
+end ComplexityTests.CompactConfigurationMatrix