From 406a68d5c75e9ccf0ba540a18676d794046d1263 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:50:25 +0000 Subject: [PATCH 1/2] feat(logspace): certify local fair-coin configuration counts Read each fixed-coin edge of the compact configuration graph and add the two contributions, preserving multiplicity when the successors coincide. Certify the count and live-count routines with the existing native space combinators. Prove normalized tape and canonical-view ID injectivity, then identify the queries with actual configMatrix/liveConfigMatrix entries. Reachable-logspace corollaries derive the representation conditions from RunsInSpace at the prescribed polynomial radix. Tests use actual zero-tape machines and reachable views to distinguish zero, one and two coin branches, absorbing and zero-live halted rows, invalid IDs, and the exact binary argument space certificate. Validation on base df2279f9 plus this four-file diff: all three modules and the test pass direct Lean 4.36.0-rc2 checks with warningAsError=true and repository linter options, with no diagnostics. Focused hygiene --check-simp and staged git diff --check pass. Outputs are isolated and shared compiled dependencies are read-only. Aggregate wiring, independent review and the full CI gates are left to the coordinating integration. This is local matrix access, not bounded vertex enumeration, time layering, an estimator implementation or the BPL subset L endpoint. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-logspace-coin-multiplicity-20261030, wrote and validated these files. Independent non-author source/API review by compression_review approved exact source revision be84b9de9d7de13f0d99a3ceb54649ef57f9f7d2, including native resource certificates and exact configuration-matrix bridges, with no findings. Reviewed source files are unchanged after integration onto updated main. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 3 + .../Randomized/ConfigurationReader.lean | 195 ++++++++++++++++++ .../LogSpace/ConfigurationGraph/FairCoin.lean | 131 ++++++++++++ .../ConfigurationGraph/Injective.lean | 90 ++++++++ .../FairCoinConfigurationReader.lean | 159 ++++++++++++++ 5 files changed, 578 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean create mode 100644 ComplexityTests/FairCoinConfigurationReader.lean diff --git a/Complexity.lean b/Complexity.lean index 9735d61c91..7c91ae5924 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1068,6 +1068,7 @@ 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.ConfigurationMatrix +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs @@ -1527,6 +1528,8 @@ 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.Expr +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Injective public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Radix public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Routines public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Tape diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean new file mode 100644 index 0000000000..9ba13cdb2e --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean @@ -0,0 +1,195 @@ +/- +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.ConfigurationMatrix +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Injective + +/-! +# Reading the fair-coin configuration matrix from compact IDs + +The native compact-ID query `coinCountWithSymbol` agrees with the actual configuration matrix of +`MultiTapePTM`, counting both coins even when they select the same successor. Its live variant +agrees with the live configuration matrix. The correspondence uses the original input only at +the compact graph's `queryIndex`. + +For views reachable under a logarithmic space bound, the prescribed polynomial radix fits every +view and the output is already summarized. The final two corollaries derive these representation +conditions from the machine's space bound and reachability, so they apply to the reachable-view +sets in `exists_configMatrix_of_mem_BPL`. + +The count matrix gives halted views an absorbing edge of multiplicity two. The live matrix gives +halted views a zero row. These are the two conventions of `ConfigurationMatrix`, and do not assert +that halted executions consume further coins. This module supplies local access with the native +space certificates of `ConfigurationGraph.FairCoin`; bounded enumeration, time layering and the +full estimator remain separate constructions. + +## Main results + +* `Turing.MultiTapePTM.viewStep_withCoin_iff`: a fixed-coin native view edge is its coin successor. +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_eq_configMatrix`, + `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol_eq_liveConfigMatrix`: + exact matrix entries at fitting canonical views. +* The corresponding `*_of_reachable` results: the native logspace machine discharges the + representation hypotheses at its polynomial radix. +-/ + +public section + +namespace Turing.MultiTapePTM + +open MultiTapeNTM + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) + +/-- Fixing the coin gives exactly the corresponding deterministic view successor. -/ +theorem viewStep_withCoin_iff {a b : FiniteCfg k Bool State} (bit : Bool) : + (machine.withCoin bit).toTM.toMultiTapeNTM.ViewStep a b ↔ + machine.viewCoinStep a bit = b := by + cases hs : a.state <;> + simp [MultiTapeNTM.ViewStep, viewCoinStep, hs, MultiTapeTM.tr_iff, eq_comm] + +private theorem outputClass_idem (w : List Bool) : outputClass (outputClass w) = outputClass w := by + simpa only [Option.toList_none, List.append_nil] using outputClass_append w none + +private theorem viewCoinStep_input (a : FiniteCfg k Bool State) (bit : Bool) : + (machine.viewCoinStep a bit).input = a.input := by + cases hs : a.state <;> simp [viewCoinStep, hs, FiniteCfg.summarizeOutput, FiniteCfg.step] + +private theorem viewCoinStep_canonical {a : FiniteCfg k Bool State} + (ha : outputClass a.output = a.output) (bit : Bool) : + outputClass (machine.viewCoinStep a bit).output = (machine.viewCoinStep a bit).output := by + cases hs : a.state <;> + simp [viewCoinStep, hs, FiniteCfg.summarizeOutput, outputClass_idem, ha] + +namespace ConfigurationGraph + +open MultiTapeNTM.ConfigurationGraph + +variable [Fintype State] + +/-- The local edge test for one fixed coin is exact on fitting canonical views. -/ +theorem edgeWithSymbol_withCoin_iff {B : ℕ} {a b : FiniteCfg k Bool State} + (hinput : a.input = b.input) (ha : outputClass a.output = a.output) + (hb : outputClass b.output = b.output) + (hfitA : Fits B (registers a)) (hfitB : Fits B (registers b)) (bit : Bool) : + edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B a.input.length + (vertexID B a) (vertexID B b) a.input[queryIndex (k := k) B (vertexID B a)]? = true ↔ + machine.viewCoinStep a bit = b := by + change Edge (machine.withCoin bit).toTM.toMultiTapeNTM B a.input + (vertexID B a) (vertexID B b) ↔ _ + constructor + · intro he + obtain ⟨next, hstep, _, hid, hfit⟩ := edge_sound hfitA he + have hnext : machine.viewCoinStep a bit = next := (viewStep_withCoin_iff machine bit).mp hstep + subst next + exact vertexID_injective ((viewCoinStep_input machine a bit).trans hinput) + (viewCoinStep_canonical machine ha bit) hb hfit hfitB hid.symm + · intro he + exact edge_complete hfitA hfitB ((viewStep_withCoin_iff machine bit).mpr he) + +variable {R : Type*} [CommSemiring R] + +/-- The certified local coin count, cast to the coefficient semiring, is the actual matrix entry. +No closedness assumption on `V` is needed for this individual-entry identity. -/ +theorem coinCountWithSymbol_eq_configMatrix {B : ℕ} {V : Finset (FiniteCfg k Bool State)} + (x y : V) (hinput : (x : FiniteCfg k Bool State).input = y.val.input) + (hx : outputClass x.val.output = x.val.output) (hy : outputClass y.val.output = y.val.output) + (hfitX : Fits B (registers x.val)) (hfitY : Fits B (registers y.val)) : + (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) = + machine.configMatrix R V x y := by + classical + have hcoin (bit : Bool) : + ((edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B x.val.input.length + (vertexID B x.val) (vertexID B y.val) + x.val.input[queryIndex (k := k) B (vertexID B x.val)]?).toNat : R) = + if machine.viewCoinStep x bit = y then 1 else 0 := by + have he := edgeWithSymbol_withCoin_iff machine hinput hx hy hfitX hfitY bit + by_cases hb : machine.viewCoinStep x bit = y + · simp [he.mpr hb, hb] + · have hf : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B x.val.input.length + (vertexID B x.val) (vertexID B y.val) + x.val.input[queryIndex (k := k) B (vertexID B x.val)]? = false := + Bool.eq_false_iff.mpr fun h => hb (he.mp h) + simp [hf, hb] + rw [coinCountWithSymbol, Nat.cast_add, hcoin false, hcoin true, configMatrix, + Matrix.coinStepMatrix, Fintype.sum_bool] + exact add_comm _ _ + +/-- The certified local count with halted rows removed is the actual live matrix entry. -/ +theorem liveCoinCountWithSymbol_eq_liveConfigMatrix {B : ℕ} + {V : Finset (FiniteCfg k Bool State)} (x y : V) + (hinput : x.val.input = y.val.input) + (hx : outputClass x.val.output = x.val.output) (hy : outputClass y.val.output = y.val.output) + (hfitX : Fits B (registers x.val)) (hfitY : Fits B (registers y.val)) : + (liveCoinCountWithSymbol 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) = + machine.liveConfigMatrix R V x y := by + classical + rw [liveCoinCountWithSymbol, readRegisters_vertexID hfitX] + change ((if stateCode x.val.state = stateCode (none : Option State) then (0 : ℕ) + else 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) = _ + by_cases hs : x.val.state = none + · simp [hs, liveConfigMatrix, Matrix.liveCoinStepMatrix] + · have hcode : stateCode x.val.state ≠ stateCode (none : Option State) := + fun h => hs (stateCode_injective h) + rw [ite_eq_right hcode, liveConfigMatrix, Matrix.liveCoinStepMatrix, ite_eq_left hs] + 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} + (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 + rw [hrep.output, outputClass_idem] + +/-- Reachability and the native logarithmic space bound supply every representation hypothesis +for the count-matrix reader at the standard polynomial radix. -/ +theorem coinCountWithSymbol_eq_configMatrix_of_reachable (c : ℕ) {input : List Bool} + (hs : machine.toNTM.RunsInSpace input (c * (Nat.log2 input.length + 1))) + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ v ∈ V, Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v) + (x y : V) : + let B := radix (radixExponent State c) input.length + (coinCountWithSymbol machine B input.length (vertexID B x.val) (vertexID B y.val) + input[queryIndex (k := k) B (vertexID B x.val)]? : R) = machine.configMatrix R V x y := by + dsimp only + have hx := hV x x.property + have hy := hV y y.property + have hix : x.val.input = input := input_of_reachable hx + have hiy : y.val.input = input := input_of_reachable hy + simpa only [hix] using coinCountWithSymbol_eq_configMatrix machine x y (hix.trans hiy.symm) + (canonical_of_reachable machine hx) (canonical_of_reachable machine hy) + (fits_of_runsInSpace c hs hx) (fits_of_runsInSpace c hs hy) + +/-- The same reachable-view corollary for the live configuration matrix. -/ +theorem liveCoinCountWithSymbol_eq_liveConfigMatrix_of_reachable (c : ℕ) {input : List Bool} + (hs : machine.toNTM.RunsInSpace input (c * (Nat.log2 input.length + 1))) + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ v ∈ V, Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v) + (x y : V) : + let B := radix (radixExponent State c) input.length + (liveCoinCountWithSymbol machine B input.length (vertexID B x.val) (vertexID B y.val) + input[queryIndex (k := k) B (vertexID B x.val)]? : R) = machine.liveConfigMatrix R V x y := by + dsimp only + have hx := hV x x.property + have hy := hV y y.property + have hix : x.val.input = input := input_of_reachable hx + have hiy : y.val.input = input := input_of_reachable hy + simpa only [hix] using + liveCoinCountWithSymbol_eq_liveConfigMatrix machine x y (hix.trans hiy.symm) + (canonical_of_reachable machine hx) (canonical_of_reachable machine hy) + (fits_of_runsInSpace c hs hx) (fits_of_runsInSpace c hs hy) + +end ConfigurationGraph + +end Turing.MultiTapePTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean new file mode 100644 index 0000000000..1869f761ee --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean @@ -0,0 +1,131 @@ +/- +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.Routines +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness + +/-! +# Fair-coin transition counts on compact configuration IDs + +The nondeterministic compact graph records whether an edge exists. A fair-coin transition needs +its multiplicity: two coincident branches still contribute two. `coinCountWithSymbol` adds the +edge tests for the two fixed-coin machines. Each test reads the same supplied input symbol and +uses the existing guarded radix arithmetic. Halting views are absorbing for this count; +`liveCoinCountWithSymbol` instead gives them zero rows. + +The native space certificates charge the binary radix, input length, source and target IDs and +one supplied symbol. The input itself is accessed only at `queryIndex`. The matrix interpretation +is supplied in `Classes.LogSpace.Randomized.ConfigurationReader`. + +## Main definitions + +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol`: the sum of the two coin edges. +* `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol`: the count at running IDs. + +## Main results + +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_le_two`: every count is at most two. +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_budget`, + `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol_budget`: native space bounds. + +This is a local implementation of the fair-coin configuration matrix, not an enumeration of its +vertices or a time-layered matrix construction. It adds no estimator or derandomization claim. +-/ + +public section + +namespace Turing.MultiTapePTM.ConfigurationGraph + +open MultiTapeNTM.ConfigurationGraph +open Cslib.Turing MultiTapeTM ComputableInSpace + +variable {k : ℕ} {State : Type} [Fintype State] + +/-- The two fixed-coin edge predicates, counted separately even when their successors coincide. +The compact graph guards invalid IDs and successor overflow; its halted vertices are absorbing. -/ +@[expose] noncomputable def coinCountWithSymbol (machine : MultiTapePTM k Bool State) + (B n u v : ℕ) (symbol : Option Bool) : ℕ := + (edgeWithSymbol (machine.withCoin false).toTM.toMultiTapeNTM B n u v symbol).toNat + + (edgeWithSymbol (machine.withCoin true).toTM.toMultiTapeNTM B n u v symbol).toNat + +/-- The live transition count: rows whose control tag is halted are zero. -/ +@[expose] noncomputable def liveCoinCountWithSymbol (machine : MultiTapePTM k Bool State) + (B n u v : ℕ) (symbol : Option Bool) : ℕ := + if readRegisters (k := k) B u .control = stateCode (none : Option State) then 0 + else coinCountWithSymbol machine B n u v symbol + +/-- There are exactly two possible coin values, so the multiplicity is at most two. -/ +theorem coinCountWithSymbol_le_two (machine : MultiTapePTM k Bool State) + (B n u v : ℕ) (symbol : Option Bool) : + coinCountWithSymbol machine B n u v symbol ≤ 2 := by + unfold coinCountWithSymbol + cases edgeWithSymbol (machine.withCoin false).toTM.toMultiTapeNTM B n u v symbol <;> + cases edgeWithSymbol (machine.withCoin true).toTM.toMultiTapeNTM B n u v symbol <;> decide + +/-- An ID outside the bounded radix box has no outgoing coin edge. -/ +theorem coinCountWithSymbol_eq_zero_of_source_ge (machine : MultiTapePTM k Bool State) + {B n u v : ℕ} (hu : vertexBound (k := k) B ≤ u) (symbol : Option Bool) : + coinCountWithSymbol machine B n u v symbol = 0 := by + have h (bit : Bool) : + edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol = false := by + cases he : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol with + | false => rfl + | true => exact False.elim ((not_lt_of_ge hu) (lt_vertexBound_of_edgeWithSymbol he).1) + simp [coinCountWithSymbol, h] + +/-- An ID outside the bounded radix box cannot be the target of a coin edge. -/ +theorem coinCountWithSymbol_eq_zero_of_target_ge (machine : MultiTapePTM k Bool State) + {B n u v : ℕ} (hv : vertexBound (k := k) B ≤ v) (symbol : Option Bool) : + coinCountWithSymbol machine B n u v symbol = 0 := by + have h (bit : Bool) : + edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol = false := by + cases he : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol with + | false => rfl + | true => exact False.elim ((not_lt_of_ge hv) (lt_vertexBound_of_edgeWithSymbol he).2) + simp [coinCountWithSymbol, h] + +variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} + {B n u v : α → ℕ} {symbol : α → Option Bool} + +/-- Count the two coin branches within any common native space budget for the short arguments. -/ +theorem coinCountWithSymbol_budget (machine : MultiTapePTM k Bool State) + (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) + (hv : ComputableInSpace v enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) + (hin : (fun a => (enc a).length) ≼ S) : + ComputableInSpace (fun a => coinCountWithSymbol machine (B a) (n a) (u a) (v a) (symbol a)) + enc encNat S := + budget_natAdd + (budget_finite Bool.toNat + (edgeWithSymbol_budget (machine.withCoin false).toTM.toMultiTapeNTM hB hn hu hv hs hin)) + (budget_finite Bool.toNat + (edgeWithSymbol_budget (machine.withCoin true).toTM.toMultiTapeNTM hB hn hu hv hs hin)) + +/-- Zeroing the halted rows preserves the same native space budget. -/ +theorem liveCoinCountWithSymbol_budget (machine : MultiTapePTM k Bool State) + (hB : ComputableInSpace B enc encNat S) + (hn : ComputableInSpace n enc encNat S) + (hu : ComputableInSpace u enc encNat S) + (hv : ComputableInSpace v enc encNat S) + (hs : ComputableInSpace symbol enc (encOption encBool) S) + (hin : (fun a => (enc a).length) ≼ S) : + ComputableInSpace + (fun a => liveCoinCountWithSymbol machine (B a) (n a) (u a) (v a) (symbol a)) + enc encNat S := by + have hc : ComputableInSpace (fun a => readRegisters (k := k) (B a) (u a) .control) + enc encNat S := + budget_comp_linear (component_inSpace (Register.control : Register k)) (budget_prod hB hu) + simpa only [liveCoinCountWithSymbol, decide_eq_true_eq] using + budget_ite (budget_natEq hc (budget_const (stateCode (none : Option State)) hin)) + (budget_const 0 hin) (coinCountWithSymbol_budget machine hB hn hu hv hs hin) + +end Turing.MultiTapePTM.ConfigurationGraph diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean new file mode 100644 index 0000000000..5341a4f0b8 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean @@ -0,0 +1,90 @@ +/- +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 + +/-! +# Compact configuration IDs identify canonical views + +The radix encoding stores the full input-free configuration except for the output, which it +summarizes as empty, accepting, or rejecting. On views with already summarized output and a fixed +input, fitting IDs are injective. This lets a local query on IDs represent an individual matrix +entry, rather than an entire fiber of the encoding. + +## Main results + +* `Turing.MultiTapeNTM.ConfigurationGraph.stackCode_injective`: normalized ternary tape codes + distinguish stack tapes. +* `Turing.MultiTapeNTM.ConfigurationGraph.vertexID_injective`: equal fitting IDs, on the same + input and with canonical output, identify the same view. +-/ + +public section + +namespace Turing.MultiTapeNTM.ConfigurationGraph + +open Cslib.Turing + +/-- The normalized stack representation has a unique ternary code. -/ +theorem stackCode_injective : Function.Injective stackCode := by + suffices h : ∀ n : ℕ, ∀ a b : StackTape Bool, + a.toList.length + b.toList.length = n → stackCode a = stackCode b → a = b from + fun a b hab => h _ a b rfl hab + intro n + induction n using Nat.strong_induction_on with + | ind n ih => + intro a b hn hab + by_cases hz : n = 0 + · have ha : a.toList = [] := List.length_eq_zero_iff.mp (by omega) + have hb : b.toList = [] := List.length_eq_zero_iff.mp (by omega) + exact StackTape.ext (ha.trans hb.symm) + · have hlt : a.tail.toList.length + b.tail.toList.length < n := by + simp only [StackTape.tail_toList, List.length_tail] + omega + apply (StackTape.eq_iff a b).mpr + refine ⟨symbolCode_injective ?_, ih _ hlt a.tail b.tail rfl ?_⟩ + · rw [stackCode_head, stackCode_head, hab] + · rw [stackCode_tail, stackCode_tail, hab] + +private theorem outputClass_eq_of_outputCode_eq {a b : List Bool} + (h : outputCode a = outputCode b) : outputClass a = outputClass b := by + unfold outputClass + unfold outputCode at h + split_ifs at h ⊢ <;> simp_all + +variable {k : ℕ} {State : Type} [Fintype State] + +/-- The input-free registers distinguish views with the same input and canonical output. -/ +theorem registers_injective {a b : FiniteCfg k Bool State} + (hinput : a.input = b.input) (ha : outputClass a.output = a.output) + (hb : outputClass b.output = b.output) (h : registers a = registers b) : a = b := by + have hpos : a.inputPos.val = b.inputPos.val := congrFun h .inputPos + have hstate : a.state = b.state := stateCode_injective (congrFun h .control) + have hout : a.output = b.output := + ha.symm.trans ((outputClass_eq_of_outputCode_eq (congrFun h .output)).trans hb) + have hwork : a.workTapes = b.workTapes := by + funext i + exact BiTape.ext (symbolCode_injective (congrFun h (.head i))) + (stackCode_injective (congrFun h (.left i))) + (stackCode_injective (congrFun h (.right i))) + apply coreCode_injective hinput + change encCore (a.inputPos.val, a.state, a.workTapes, a.output) = + encCore (b.inputPos.val, b.state, b.workTapes, b.output) + rw [hpos, hstate, hwork, hout] + +/-- Equal IDs determine fitting views with the same input and already summarized output. -/ +theorem vertexID_injective {B : ℕ} {a b : FiniteCfg k Bool State} + (hinput : a.input = b.input) (ha : outputClass a.output = a.output) + (hb : outputClass b.output = b.output) + (hfitA : Fits B (registers a)) (hfitB : Fits B (registers b)) + (h : vertexID B a = vertexID B b) : a = b := by + apply registers_injective hinput ha hb + rw [← readRegisters_vertexID hfitA, ← readRegisters_vertexID hfitB, h] + +end Turing.MultiTapeNTM.ConfigurationGraph diff --git a/ComplexityTests/FairCoinConfigurationReader.lean b/ComplexityTests/FairCoinConfigurationReader.lean new file mode 100644 index 0000000000..b5623a8ee4 --- /dev/null +++ b/ComplexityTests/FairCoinConfigurationReader.lean @@ -0,0 +1,159 @@ +/- +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.ConfigurationReader + +/-! +# Fair-coin compact-reader tests + +A zero-work-tape machine either outputs its coin or outputs true on both branches. The tests +derive all representation hypotheses from its actual space bound and reachable configurations, +then evaluate the matrix entries through the new local reader. They distinguish zero, one and +two coin branches, and distinguish an absorbing halted row from the zero live row. Invalid IDs +and a native space certificate on the exact binary query tuple are also checked. +-/ + +namespace ComplexityTests.FairCoinConfigurationReader + +open Cslib.Turing Turing MultiTapeTM +open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph + +/-- With `different = true`, output the coin; otherwise both branches output true. -/ +private def machine (different : Bool) : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := + .step + { inputTape := 0 + workTapes := Fin.elim0 + output := some (if different then bit else true) + state := none } + Empty.elim Empty.elim + +private def stopped (input : List Bool) (bit : Bool) : FiniteCfg 0 Bool Unit := + ⟨input, none, 1, Fin.elim0, [bit]⟩ + +private theorem viewCoinStep_start (different bit : Bool) (input : List Bool) : + (machine different).viewCoinStep ((machine different).toNTM.initView input) bit = + stopped input (if different then bit else true) := by + cases different <;> cases bit <;> + simp [MultiTapePTM.viewCoinStep, machine, MultiTapePTM.withCoin, MultiTapeMachine.toTM, + MultiTapeMachine.Action.emptyOracleEquiv, + MultiTapeNTM.initView, MultiTapePTM.toNTM, MultiTapePTM.branches, MultiTapeMachine.toNTM, + FiniteCfg.init, FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, + stopped, funext_iff] + +private theorem stopped_injective (input : List Bool) : Function.Injective (stopped input) := by + intro a b h + have ho := congrArg FiniteCfg.output h + simpa only [stopped, List.cons.injEq, and_true] using ho + +private theorem stopped_ne_start (different bit : Bool) (input : List Bool) : + stopped input bit ≠ (machine different).toNTM.initView input := by + intro h + have hs := congrArg FiniteCfg.state h + cases hs + +private abbrev radixFor (input : List Bool) : ℕ := radix (radixExponent Unit 0) input.length + +private noncomputable def readCount (different : Bool) (input : List Bool) + (x y : FiniteCfg 0 Bool Unit) : ℕ := + coinCountWithSymbol (machine different) (radixFor input) input.length + (vertexID (radixFor input) x) (vertexID (radixFor input) y) + input[queryIndex (k := 0) (radixFor input) (vertexID (radixFor input) x)]? + +private noncomputable def readLiveCount (different : Bool) (input : List Bool) + (x y : FiniteCfg 0 Bool Unit) : ℕ := + liveCoinCountWithSymbol (machine different) (radixFor input) input.length + (vertexID (radixFor input) x) (vertexID (radixFor input) y) + input[queryIndex (k := 0) (radixFor input) (vertexID (radixFor input) x)]? + +private theorem reader_counts (different : Bool) (input : List Bool) : + readCount different input ((machine different).toNTM.initView input) (stopped input true) = + (if different then 1 else 2) ∧ + readCount different input ((machine different).toNTM.initView input) + ((machine different).toNTM.initView input) = 0 ∧ + readCount different input (stopped input true) (stopped input true) = 2 ∧ + readLiveCount different input (stopped input true) (stopped input true) = 0 := by + classical + have hs := MultiTapeNTM.runsInSpace_zero_tapes (machine different).toNTM input 0 + obtain ⟨V, hreach, hclosed, _⟩ := (machine different).exists_finset_reachable hs + have hinit : (machine different).toNTM.initView input ∈ V := (hreach _).mpr .refl + have hstop : stopped input true ∈ V := by + have h := hclosed _ hinit true + simp only [viewCoinStep_start, ite_self] at h + exact h + let x : V := ⟨(machine different).toNTM.initView input, hinit⟩ + let y : V := ⟨stopped input true, hstop⟩ + have hV v hv := (hreach v).mp hv + have hspace : (machine different).toNTM.RunsInSpace input + (0 * (Nat.log2 input.length + 1)) := by + rw [Nat.zero_mul] + exact hs + have hxy := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ) + (machine different) 0 hspace hV x y + have hxx := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ) + (machine different) 0 hspace hV x x + have hyy := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ) + (machine different) 0 hspace hV y y + have hlyy := liveCoinCountWithSymbol_eq_liveConfigMatrix_of_reachable (R := ℕ) + (machine different) 0 hspace hV y y + change readCount different input _ _ = _ at hxy hxx hyy + change readLiveCount different input _ _ = _ at hlyy + rw [hxy, hxx, hyy, hlyy] + refine ⟨?_, ?_, ?_, ?_⟩ + · simp only [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, Fintype.sum_bool, x, y, + viewCoinStep_start, (stopped_injective input).eq_iff] + cases different <;> decide + · simp [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, x, viewCoinStep_start, + stopped_ne_start] + · simp [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, MultiTapePTM.viewCoinStep, y, stopped] + · simp [MultiTapePTM.liveConfigMatrix, Matrix.liveCoinStepMatrix, y, stopped] + +-- The actual encoded reader sees one coin edge, including on the empty input boundary. +example : readCount true [] ((machine true).toNTM.initView []) (stopped [] true) = 1 := + (reader_counts true []).1 + +-- Coincident successor branches contribute two, rather than one Boolean adjacency edge. +example : readCount false [true, false] ((machine false).toNTM.initView [true, false]) + (stopped [true, false] true) = 2 := (reader_counts false [true, false]).1 + +-- There is no transition back to the initial running view. +example (input : List Bool) : + readCount true input ((machine true).toNTM.initView input) + ((machine true).toNTM.initView input) = 0 := (reader_counts true input).2.1 + +-- Halting is absorbing in the count matrix and has zero outgoing weight in the live matrix. +example : readCount true [] (stopped [] true) (stopped [] true) = 2 ∧ + readLiveCount true [] (stopped [] true) (stopped [] true) = 0 := + (reader_counts true []).2.2 + +-- Out-of-box IDs cannot create a spurious transition for either supplied input symbol. +example (B n v : ℕ) (symbol : Option Bool) : + coinCountWithSymbol (machine true) B n (vertexBound (k := 0) B) v symbol = 0 := + coinCountWithSymbol_eq_zero_of_source_ge _ (le_refl _) _ + +example (B n u : ℕ) (symbol : Option Bool) : + coinCountWithSymbol (machine true) B n u (vertexBound (k := 0) B) symbol = 0 := + coinCountWithSymbol_eq_zero_of_target_ge _ (le_refl _) _ + +/-- The runtime query stores only its radix, input length, two IDs, and one supplied symbol. -/ +private abbrev encQuery : ℕ × ℕ × ℕ × ℕ × Option Bool ↪ List Bool := + encPair encNat (encPair encNat (encPair encNat (encPair encNat (encOption encBool)))) + +open ComputableInSpace in +-- A concrete query on its exact binary argument encoding has a native linear-space certificate. +example : ComputableInSpace + (fun a : ℕ × ℕ × ℕ × ℕ × Option Bool => + liveCoinCountWithSymbol (machine true) a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) + encQuery encNat (fun a => (encQuery a).length) := by + have hr₁ := snd encNat (encPair encNat (encPair encNat (encPair encNat (encOption encBool)))) + have hr₂ := budget_comp_linear (snd _ _) hr₁ + have hr₃ := budget_comp_linear (snd _ _) hr₂ + exact liveCoinCountWithSymbol_budget (machine true) (fst _ _) + (budget_comp_linear (fst _ _) hr₁) (budget_comp_linear (fst _ _) hr₂) + (budget_comp_linear (fst _ _) hr₃) (budget_comp_linear (snd _ _) hr₃) (.refl _) + +end ComplexityTests.FairCoinConfigurationReader From 8e688004b8702396c244ee40c0f6167561a550ff Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 17:52:54 +0000 Subject: [PATCH 2/2] feat(logspace): clock actual fair-coin configuration matrices Construct a time-layered matrix with edges only to the next clock layer, terminal-only reward, and the explicit remaining-horizon potential. Prove strict upper triangularity, substochasticity, bounds on every potential coordinate, the linear-system identity, determinant one, and its inverse solution. This follows the ordinary absorbing-matrix convention of the pinned model.tex Lemma 2.1 (OpenAI2026LogSpace, revision 7ef5c0cc). Specialize to the actual half-normalized fair-coin configuration matrix and prove its clock-zero potential is the native finite-time acceptance frequency and the existing finite sum of first-stop live terms. Identify clocked entries with the certified compact-ID coin-count reader. Apply the existing BPL configuration-matrix theorem to obtain concrete polynomial-size strict-forward systems with bounded potential and the 2/3 versus 1/3 gap. Tests realize a zero-work-tape machine that loops on false and accepts on true. They prove its actual two-step acceptance probability is 3/4 and read a nonzero clocked edge from the compact IDs. Additional checks cover an absorbing matrix, terminal-only reward, zero horizon, the explicit linear system and inverse, and the exact clocked cardinality. Validation on base 406a68d5 plus this three-file diff: both library modules and ComplexityTests/TimeLayer.lean pass direct Lean 4.36.0-rc2 with warningAsError=true and repository linter options, without diagnostics. Focused check_hygiene.py --check-simp and staged git diff --check pass. Builds use only tiny isolated outputs and read-only compiled dependencies; there are no Lake/cache/bootstrap operations. Aggregate registration and full CI gates remain for coordinating integration. The final independent review is pending; the two unchanged library snapshots already received a no-findings source review from lean_environment. This is a concrete semantic reduction. Bounded vertex enumeration, composition with whole-input symbol access, incoming paired ports, the recursive estimator, and the native BPL subset L endpoint remain open. No selected abstract or catalogue impact. AI assistance: ChatGPT (GPT-6 Astra), worker codex-time-layer-20261030, wrote and validated the three files. Independent non-author review by lean_environment approved exact source commit dafd85f98e5fd78eec31900dff411b0c5bf8c138 with no findings; integrated library and test bytes match that snapshot. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 2 + .../LogSpace/Randomized/TimeLayer.lean | 237 ++++++++++++++++++ .../LinearAlgebra/Matrix/TimeLayer.lean | 201 +++++++++++++++ ComplexityTests/TimeLayer.lean | 185 ++++++++++++++ 4 files changed, 625 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/TimeLayer.lean create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer.lean create mode 100644 ComplexityTests/TimeLayer.lean diff --git a/Complexity.lean b/Complexity.lean index 7c91ae5924..92db55da7a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1069,6 +1069,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.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs @@ -2709,6 +2710,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