From 406a68d5c75e9ccf0ba540a18676d794046d1263 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:50:25 +0000 Subject: [PATCH 1/5] 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/5] 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 From df9b44b3f16262b6e0589f6ad6535e0ed2f2185e Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 18:25:55 +0000 Subject: [PATCH 3/5] feat(logspace): read fair-coin counts from framed inputs Extract STCON's five-instruction input-symbol reader and its bounded ReachesOut proof into ConfigurationGraph.ReadSymbol, then make the existing STCON writer reuse both without changing its instruction labels. Compose that actual reader with the two fixed-coin arithmetic edge tests. The six-instruction block returns the exact 0/1/2 multiplicity in its scratch register, reads the original framed input, preserves the length and IDs, and emits nothing. Its concrete four-register program has native linear-space certificates for its query and execution callbacks. The entry length and compact IDs are preloaded explicitly. This is a native input-reading component, not a completed ambient enumeration, paired-port construction, or whole Phase 1 reduction. Focused validation: direct Lean 4.36.0-rc2 with the project options and -DwarningAsError=true passed without diagnostics for ReadSymbol, FairCoin.ReadInput, STCON.Reduction, STCON.Completeness, the new FairCoinInput tests, and the existing STCON tests. New tests read true, false, absent and empty-input symbols and prove bounded runs of an actual input-dependent machine with fixed compact IDs returning 0, 1 and 2. The hygiene check with --check-simp and git diff --check also passed. Shared dependency outputs were read-only; all direct-Lean outputs were private. Full repository CI and aggregate registration remain integration work. Independent exact-revision review is requested separately. AI assistance: ChatGPT worker codex-coin-input-20261030 implemented and self-checked this change under the coordinating agent's agreed scope. Independent non-author agent coin_input_review approved exact source commit 46dcedfed969a806887fb0fa3bcf04840530c940 with no findings and independently checked the behavioral tests. Integrated source/test bytes match that reviewed 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 + .../Complexity/Problems/STCON/Reduction.lean | 41 ++--- .../FairCoin/ReadInput.lean | 156 ++++++++++++++++ .../ConfigurationGraph/ReadSymbol.lean | 85 +++++++++ ComplexityTests/FairCoinInput.lean | 170 ++++++++++++++++++ 5 files changed, 423 insertions(+), 31 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean create mode 100644 ComplexityTests/FairCoinInput.lean diff --git a/Complexity.lean b/Complexity.lean index 92db55da7a..54452f9614 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1530,8 +1530,10 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS 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.FairCoin.ReadInput 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.ReadSymbol public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Routines public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Tape public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Configurations diff --git a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean index 8020124d9f..5472e88008 100644 --- a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean +++ b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean @@ -10,9 +10,8 @@ module public import Complexity.Computability.Complexity.Problems.STCON public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr -public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness -import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame /-! # The configuration graph as an instance of directed connectivity @@ -192,13 +191,9 @@ noncomputable def writer : CounterProgram where forCode 12 1 (vertexBoundExpr k (radixExpr D (reg 0))) 15 16 ++ [emit true 14, emit false 17] ++ forCode 17 1 (numVerticesExpr (k := k) D) 20 33 ++ forCode 20 2 (numVerticesExpr (k := k) D) 23 19 ++ - [lt (reg 2) (vertexBoundExpr k (radixExpr D (reg 0))) 24 30, - lt (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) (reg 0) 25 28, - read (add (mul (const 2) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))) (const 1)) 26 27 27, - assign 3 (const 2) 29, - assign 3 (const 1) 29, - assign 3 (const 0) 29, - lt (const 0) (edgeExpr ntm (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)) 31 32, + [lt (reg 2) (vertexBoundExpr k (radixExpr D (reg 0))) 24 30] ++ + readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) ++ + [lt (const 0) (edgeExpr ntm (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)) 31 32, lt (const 0) (badExpr k State (radixExpr D (reg 0)) (reg 0) (reg 1)) 31 32, emit true 22, emit false 22, @@ -293,29 +288,13 @@ private theorem reachesOut_entry_symbol (hL : w.length ≤ B) ∃ y' ≤ 2, y' = symbolCode w[queryIndex (k := k) (radix D w.length) u]? ∧ (writer ntm D).ReachesOut (frame w) ((writer ntm D).Active B) (24, [w.length, u, v, y]) (29, [w.length, u, v, y']) [] := by - -- the code of the symbol requested by the row `u` have hB : ∀ r ∈ [w.length, u, v, y], r ≤ B := bounded_regs hL (by omega) (by omega) (by omega) - set q := queryIndex (k := k) (radix D w.length) u with hq_def - by_cases hq : q < w.length - · obtain ⟨b, hb⟩ : ∃ b, w[q]? = some b := ⟨w[q], List.getElem?_eq_getElem hq⟩ - refine ⟨symbolCode (some b), by cases b <;> decide, by rw [hb], ?_⟩ - refine ReachesOut.lt (show (writer ntm D).instr 24 = _ from rfl) hB ?_ - simp only [eval_queryIndexExpr, eval_radixExpr, eval_reg, List.getD_cons_zero, - List.getD_cons_succ, ← hq_def, hq, ↓reduceIte] - refine ReachesOut.read (show (writer ntm D).instr 25 = _ from rfl) hB ?_ - simp only [eval_add, eval_mul, eval_const, eval_queryIndexExpr, eval_radixExpr, eval_reg, - List.getD_cons_zero, List.getD_cons_succ, ← hq_def, getElem?_frame_two_mul_add_one hq, hb] - cases b - · refine ReachesOut.assign (show (writer ntm D).instr 27 = _ from rfl) hB ?_ - simpa [symbolCode] using ReachesOut.refl _ - · refine ReachesOut.assign (show (writer ntm D).instr 26 = _ from rfl) hB ?_ - simpa [symbolCode] using ReachesOut.refl _ - · refine ⟨0, by omega, congrArg symbolCode (List.getElem?_eq_none (by omega)).symm, ?_⟩ - refine ReachesOut.lt (show (writer ntm D).instr 24 = _ from rfl) hB ?_ - simp only [eval_queryIndexExpr, eval_radixExpr, eval_reg, List.getD_cons_zero, - List.getD_cons_succ, ← hq_def, hq, ↓reduceIte] - refine ReachesOut.assign (show (writer ntm D).instr 28 = _ from rfl) hB ?_ - simpa using ReachesOut.refl _ + have hcode : (writer ntm D).CodeAt 24 + (readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))) := by + simp only [readSymbolCode, codeAt_cons, codeAt_nil, and_true] + exact ⟨rfl, rfl, rfl, rfl, rfl⟩ + refine ⟨_, Nat.le_of_lt_succ (symbolCode_lt _), rfl, ?_⟩ + simpa using reachesOut_readSymbolCode (w := w) hcode (by simp) hB /-- **An entry of the matrix**: the code of the requested input symbol is stored in register `3`, and the entry is written. -/ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean new file mode 100644 index 0000000000..c75e73a3a8 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean @@ -0,0 +1,156 @@ +/- +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.FairCoin +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol + +/-! +# A fair-coin count block reading the original input + +The six-instruction `coinCountCode` reads the one original input symbol requested by a compact +source ID, then evaluates both fixed-coin edges and adds their multiplicities. It uses four +registers: the original word length, source ID, target ID, and one scratch register. The scratch +register first holds the symbol code and then the count, which is zero, one, or two. + +`reachesOut_coinCountCode` proves execution on the actual framed input. The other registers do +not change, no output is emitted, and every intermediate register is bounded by any common bound +for the initial registers and two. Invalid compact IDs retain the existing guarded behavior. + +The concrete `coinCountProgram` places this block at label zero and a halt at label six. Its +query and execution callbacks have native linear-space certificates in the binary register-state +encoding. The execution theorem starts with the length and IDs already in registers; it does not +parse those parameters or enumerate a matrix. Connecting an ambient enumeration, paired ports, +and the time-layered matrix remains separate from this input-reading component. + +## Main definitions + +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountExpr`: arithmetic counting both coin edges. +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountCode`: the placed input-reading count block. +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram`: the concrete four-register program. + +## Main results + +* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinCountCode`: bounded execution from the + actual framed input, yielding the exact compact transition count. +* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinCountProgram`: the concrete program run. +* `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram_query_inSpace`, + `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram_exec_inSpace`: native space certificates + for the actual query and register-update routines. +-/ + +public section + +namespace Turing.MultiTapePTM.ConfigurationGraph + +open MultiTapeNTM.ConfigurationGraph CounterProgram Instr Expr MultiTapeTM +open Cslib.Turing + +variable {k : ℕ} {State : Type} [Fintype State] + +/-- Add the two fixed-coin arithmetic edge tests, retaining multiplicity when the successors +coincide. The symbol expression contains the ternary code used by `readSymbolCode`. -/ +noncomputable def coinCountExpr (machine : MultiTapePTM k Bool State) + (B n u v sym : Expr) : Expr := + add (edgeExpr (machine.withCoin false).toTM.toMultiTapeNTM B n u v sym) + (edgeExpr (machine.withCoin true).toTM.toMultiTapeNTM B n u v sym) + +/-- The count expression computes the existing compact fair-coin transition count. -/ +theorem eval_coinCountExpr (machine : MultiTapePTM k Bool State) + {B n u v sym : Expr} {regs : List ℕ} {symbol : Option Bool} + (hs : sym.eval regs = symbolCode symbol) : + (coinCountExpr machine B n u v sym).eval regs = + coinCountWithSymbol machine (B.eval regs) (n.eval regs) (u.eval regs) (v.eval regs) + symbol := by + rw [coinCountExpr, eval_add, eval_edgeExpr _ hs, eval_edgeExpr _ hs] + rfl + +/-- Read from `frame w` and store the coin count in register three, then continue at `exit`. +Registers zero through two hold `w.length`, the source ID, and the target ID. The radix is +`(w.length + 2) ^ D`; the six instructions start at `b`. -/ +@[expose] noncomputable def coinCountCode (machine : MultiTapePTM k Bool State) + (D b exit : ℕ) : List Instr := + readSymbolCode b 3 (b + 5) (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) ++ + [assign 3 (coinCountExpr machine (radixExpr D (reg 0)) + (reg 0) (reg 1) (reg 2) (reg 3)) exit] + +/-- The reader and the arithmetic assignment occupy six consecutive labels. -/ +@[simp] theorem length_coinCountCode (machine : MultiTapePTM k Bool State) (D b exit : ℕ) : + (coinCountCode machine D b exit).length = 6 := rfl + +/-- The actual block reads the original input and returns its exact fair-coin edge multiplicity. +All pre-exit register states satisfy the supplied common bound. No valid-ID or reachable-view +premise is needed: the existing compact edge predicates also define the invalid-ID cases. -/ +theorem reachesOut_coinCountCode (machine : MultiTapePTM k Bool State) + {P : CounterProgram} {D b exit S u v y : ℕ} {w : List Bool} + (hcode : P.CodeAt b (coinCountCode machine D b exit)) + (hS : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) : + P.ReachesOut (frame w) (P.Active S) (b, [w.length, u, v, y]) + (exit, [w.length, u, v, coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]?]) [] := by + simp only [coinCountCode, codeAt_append, length_readSymbolCode, codeAt_cons] at hcode + obtain ⟨hread, hassign, -⟩ := hcode + let symbol := w[queryIndex (k := k) (radix D w.length) u]? + have hr : P.ReachesOut (frame w) (P.Active S) (b, [w.length, u, v, y]) + (b + 5, [w.length, u, v, symbolCode symbol]) [] := by + simpa [symbol] using reachesOut_readSymbolCode (w := w) hread (by simp) hS + have hbound : ∀ r ∈ [w.length, u, v, symbolCode symbol], r ≤ S := by + intro r hr + have hm : r ∈ [w.length, u, v, y].set 3 (symbolCode symbol) := hr + rcases List.mem_or_eq_of_mem_set hm with hm | rfl + · exact hS r hm + · exact (Nat.le_of_lt_succ (symbolCode_lt symbol)).trans h2 + have heval : + (coinCountExpr machine (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)).eval + [w.length, u, v, symbolCode symbol] = + coinCountWithSymbol machine (radix D w.length) w.length u v symbol := by + simpa using eval_coinCountExpr machine (symbol := symbol) + (B := radixExpr D (reg 0)) (n := reg 0) (u := reg 1) (v := reg 2) (sym := reg 3) + (regs := [w.length, u, v, symbolCode symbol]) rfl + refine (hr.trans (ReachesOut.assign hassign hbound ?_)).of_eq rfl + rw [heval] + exact ReachesOut.refl _ + +/-- The count block followed by a halt. The caller supplies the original input length and the +two compact IDs in registers zero through two before entering the block. -/ +@[expose] noncomputable def coinCountProgram (machine : MultiTapePTM k Bool State) + (D : ℕ) : CounterProgram where + code := coinCountCode machine D 0 6 ++ [halt []] + registers := 4 + +/-- The concrete program reaches its halt label, returning the count in register three and +emitting nothing. The initial register values are explicit; they are not the zeroed program +initializer. -/ +theorem reachesOut_coinCountProgram (machine : MultiTapePTM k Bool State) + {D S u v y : ℕ} {w : List Bool} + (hS : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) : + (coinCountProgram machine D).ReachesOut (frame w) ((coinCountProgram machine D).Active S) + (0, [w.length, u, v, y]) + (6, [w.length, u, v, coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]?]) [] := + reachesOut_coinCountCode machine + (codeAt_of_code_eq (pre := []) (post := [halt []]) rfl) hS h2 + +/-- The concrete reader's query-index routine has a native linear-space certificate in its +binary label-and-register encoding, rather than the length of the original input word. -/ +theorem coinCountProgram_query_inSpace (machine : MultiTapePTM k Bool State) (D : ℕ) : + ComputableInSpace (coinCountProgram machine D).query Simulation.encConfig encNat + (fun s => (Simulation.encConfig s).length) := + (Simulation.query_inSpace (P := coinCountProgram machine D)).computableInSpace + +/-- The concrete reader's register-update routine has a native linear-space certificate in the +binary register state together with the one optional input bit returned by the native query. -/ +theorem coinCountProgram_exec_inSpace (machine : MultiTapePTM k Bool State) (D : ℕ) : + ComputableInSpace + (fun p : Config × Option Bool => (coinCountProgram machine D).exec p.1 p.2) + Simulation.encConfigRead Simulation.encConfig + (fun p => (Simulation.encConfigRead p).length) := + (Simulation.exec_inSpace (P := coinCountProgram machine D)).computableInSpace + +end Turing.MultiTapePTM.ConfigurationGraph diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean new file mode 100644 index 0000000000..1e5b8940ef --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean @@ -0,0 +1,85 @@ +/- +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.Tape +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame + +/-! +# Reading a configuration graph's input symbol + +`readSymbolCode` is the five-instruction block used by the STCON reduction to obtain the ternary +code of one original input bit. It checks the query against the stored input length, reads position +`2 * query + 1` of the framed input when in range, and stores zero otherwise. The block changes only +its destination register and emits no output. + +The query is a zero-based position in the original word. Configuration-head boundary conventions +are handled separately by the compact graph's edge test: this block returns the actual optional +word symbol, not the symbol after that boundary correction. + +## Main definitions + +* `Turing.MultiTapeNTM.ConfigurationGraph.readSymbolCode`: the relocatable input-reading block. + +## Main results + +* `Turing.MultiTapeNTM.ConfigurationGraph.reachesOut_readSymbolCode`: the actual block reads + `w[query]?` from `frame w`, preserving the bound on every pre-exit register state. +-/ + +public section + +namespace Turing.MultiTapeNTM.ConfigurationGraph + +open CounterProgram Instr Expr MultiTapeTM + +/-- Read one original input symbol from a framed word into `dst`, then continue at `exit`. +The five instructions start at `b`; `len` is the original word length and `query` its zero-based +index. The result is `symbolCode`: zero for no symbol, one for false, and two for true. -/ +@[expose] def readSymbolCode (b dst exit : ℕ) (len query : Expr) : List Instr := + [lt query len (b + 1) (b + 4), + read (add (mul (const 2) query) (const 1)) (b + 2) (b + 3) (b + 3), + assign dst (const 2) exit, + assign dst (const 1) exit, + assign dst (const 0) exit] + +/-- The reader occupies five consecutive instruction labels. -/ +@[simp] theorem length_readSymbolCode (b dst exit : ℕ) (len query : Expr) : + (readSymbolCode b dst exit len query).length = 5 := rfl + +/-- The placed block reads the original word's optional symbol, changes only `dst`, and emits +nothing. All states before the exit have the original registers, so their bound needs no extra +assumption. The final destination is at most two by `symbolCode_lt`. -/ +theorem reachesOut_readSymbolCode {P : CounterProgram} {b dst exit S : ℕ} + {len query : Expr} {regs : List ℕ} {w : List Bool} + (hcode : P.CodeAt b (readSymbolCode b dst exit len query)) + (hlen : len.eval regs = w.length) (hS : ∀ r ∈ regs, r ≤ S) : + P.ReachesOut (frame w) (P.Active S) (b, regs) + (exit, regs.set dst (symbolCode w[query.eval regs]?)) [] := by + simp only [readSymbolCode, codeAt_cons] at hcode + obtain ⟨h₀, h₁, h₂, h₃, h₄, -⟩ := hcode + simp only [Nat.add_assoc] at h₂ h₃ h₄ + refine ReachesOut.lt h₀ hS ?_ + rw [hlen] + by_cases hq : query.eval regs < w.length + · obtain ⟨bit, hb⟩ : ∃ bit, w[query.eval regs]? = some bit := + ⟨w[query.eval regs], List.getElem?_eq_getElem hq⟩ + rw [ite_eq_left hq, hb] + refine ReachesOut.read h₁ hS ?_ + simp only [eval_add, eval_mul, eval_const, getElem?_frame_two_mul_add_one hq, hb] + cases bit + · refine ReachesOut.assign h₃ hS ?_ + simpa only [eval_const, symbolCode] using ReachesOut.refl _ + · refine ReachesOut.assign h₂ hS ?_ + simpa only [eval_const, symbolCode] using ReachesOut.refl _ + · rw [ite_eq_right hq, List.getElem?_eq_none (by omega)] + refine ReachesOut.assign h₄ hS ?_ + simpa only [eval_const, symbolCode] using ReachesOut.refl _ + +end Turing.MultiTapeNTM.ConfigurationGraph diff --git a/ComplexityTests/FairCoinInput.lean b/ComplexityTests/FairCoinInput.lean new file mode 100644 index 0000000000..4c41283fa7 --- /dev/null +++ b/ComplexityTests/FairCoinInput.lean @@ -0,0 +1,170 @@ +/- +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.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ReadInput +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader + +/-! +# Fair-coin count blocks on actual framed inputs + +The shared reader obtains true, false, and absent symbols from actual framed words. A concrete +zero-work-tape machine then makes its output depend on both the input symbol and its coin. With +the same source and target compact IDs, changing the original input bit changes the block's +answer from one to zero. Making both coin branches coincide changes one to two. All representation +and runtime register bounds in these runs are discharged. +-/ + +namespace ComplexityTests.FairCoinInput + +open Cslib.Turing Turing MultiTapeTM CounterProgram Instr Expr +open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph + +private def symbolProgram : CounterProgram where + code := readSymbolCode 0 2 5 (reg 0) (reg 1) ++ [halt []] + registers := 3 + +-- The first original true bit is read from its data cell, not from a frame marker. +example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2) + (0, [2, 0, 0]) (5, [2, 0, 2]) [] := by + have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) := + codeAt_of_code_eq (pre := []) (post := [halt []]) rfl + simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false]) + (regs := [2, 0, 0]) hcode rfl (by simp) + +-- The second data cell is false, whose ternary code is one. +example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2) + (0, [2, 1, 0]) (5, [2, 1, 1]) [] := by + have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) := + codeAt_of_code_eq (pre := []) (post := [halt []]) rfl + simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false]) + (regs := [2, 1, 0]) hcode rfl (by simp) + +-- An index at the original length returns no symbol, despite the trailing frame marker. +example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2) + (0, [2, 2, 1]) (5, [2, 2, 0]) [] := by + have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) := + codeAt_of_code_eq (pre := []) (post := [halt []]) rfl + simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false]) + (regs := [2, 2, 1]) hcode rfl (by simp) + +-- Empty original input also returns no symbol and overwrites stale scratch data. +example : symbolProgram.ReachesOut (frame []) (symbolProgram.Active 2) + (0, [0, 0, 2]) (5, [0, 0, 0]) [] := by + have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) := + codeAt_of_code_eq (pre := []) (post := [halt []]) rfl + simpa [symbolCode] using reachesOut_readSymbolCode (w := []) + (regs := [0, 0, 2]) hcode rfl (by simp) + +/-- A true input symbol enables acceptance. When `different` is true, only the true coin accepts; +otherwise both coins accept. A false or absent input symbol always emits false. -/ +private def machine (different : Bool) : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ bit := + .step + { inputTape := 0 + workTapes := Fin.elim0 + output := some (symbol.getD false && (if different then bit else true)) + state := none } + Empty.elim Empty.elim + +private def running (input : Bool) : FiniteCfg 0 Bool Unit := + ⟨[input], some (), 1, Fin.elim0, []⟩ + +private def stopped (input output : Bool) : FiniteCfg 0 Bool Unit := + ⟨[input], none, 1, Fin.elim0, [output]⟩ + +private theorem viewCoinStep_running (different input bit : Bool) : + (machine different).viewCoinStep (running input) bit = + stopped input (input && (if different then bit else true)) := by + cases different <;> cases input <;> cases bit <;> + simp [MultiTapePTM.viewCoinStep, running, FiniteCfg.inputSymbol_eq_getD, machine, + MultiTapePTM.withCoin, MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv, + FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, stopped, funext_iff] + +private theorem stopped_injective (input : 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 fits_three (v : FiniteCfg 0 Bool Unit) (hinput : v.input.length = 1) : + Fits 3 (registers v) := by + intro i + cases i with + | inputPos => + change v.inputPos.val < 3 + simpa only [hinput] using v.inputPos.isLt + | control => + have h : stateCode v.state < 2 := (Fintype.equivFin (Option Unit) v.state).isLt + exact h.trans_le (by decide) + | output => exact outputCode_lt _ + | head i => exact Fin.elim0 i + | left i => exact Fin.elim0 i + | right i => exact Fin.elim0 i + +private theorem count_input (different input : Bool) : + coinCountWithSymbol (machine different) 3 1 + (vertexID 3 (running input)) (vertexID 3 (stopped input true)) + [input][queryIndex (k := 0) 3 (vertexID 3 (running input))]? = + if input then (if different then 1 else 2) else 0 := by + have hcoin (bit : Bool) := edgeWithSymbol_withCoin_iff (machine different) + (a := running input) (b := stopped input true) rfl + (by simp [running, MultiTapeNTM.outputClass]) + (by simp [stopped, MultiTapeNTM.outputClass]) + (fits_three _ rfl) (fits_three _ rfl) bit + simp only [viewCoinStep_running, (stopped_injective input).eq_iff] at hcoin + have hfalse := hcoin false + have htrue := hcoin true + rw [coinCountWithSymbol] + cases input <;> cases different <;> simp_all [running] + +private noncomputable def source : ℕ := vertexID 3 (running true) + +private noncomputable def target : ℕ := vertexID 3 (stopped true true) + +-- The original bit is not part of the compact ID; all runs below use these same two IDs. +example (input : Bool) : vertexID 3 (running input) = source ∧ + vertexID 3 (stopped input true) = target := ⟨rfl, rfl⟩ + +private theorem count_program (different input : Bool) : + (coinCountProgram (machine different) 1).ReachesOut (frame [input]) + ((coinCountProgram (machine different) 1).Active 27) + (0, [1, source, target, 0]) + (6, [1, source, target, if input then (if different then 1 else 2) else 0]) [] := by + have hbox : vertexBound (k := 0) 3 = 27 := by decide + have hu : source < 27 := by + simpa only [source, hbox] using vertexID_lt (fits_three (running true) rfl) + have hv : target < 27 := by + simpa only [target, hbox] using vertexID_lt (fits_three (stopped true true) rfl) + have hbound : ∀ r ∈ [1, source, target, 0], r ≤ 27 := by + simp only [List.mem_cons, List.not_mem_nil, or_false] + omega + have hr := reachesOut_coinCountProgram (machine different) (D := 1) (w := [input]) + hbound (by decide : 2 ≤ 27) + have hc : coinCountWithSymbol (machine different) (radix 1 [input].length) [input].length + source target [input][queryIndex (k := 0) (radix 1 [input].length) source]? = + if input then (if different then 1 else 2) else 0 := count_input different input + rw [hc] at hr + simpa only [List.length_singleton] using hr + +-- One accepting coin on the true input: the actual framed input reaches a count of one. +example : (coinCountProgram (machine true) 1).ReachesOut (frame [true]) + ((coinCountProgram (machine true) 1).Active 27) + (0, [1, source, target, 0]) (6, [1, source, target, 1]) [] := count_program true true + +-- Changing only that input bit to false changes the count to zero. +example : (coinCountProgram (machine true) 1).ReachesOut (frame [false]) + ((coinCountProgram (machine true) 1).Active 27) + (0, [1, source, target, 0]) (6, [1, source, target, 0]) [] := count_program true false + +-- Coincident accepting successors retain multiplicity two in the register result. +example : (coinCountProgram (machine false) 1).ReachesOut (frame [true]) + ((coinCountProgram (machine false) 1).Active 27) + (0, [1, source, target, 0]) (6, [1, source, target, 2]) [] := count_program false true + +-- The returned label is an actual halt of the concrete program. +example (different : Bool) : (coinCountProgram (machine different) 1).instr 6 = halt [] := rfl + +end ComplexityTests.FairCoinInput From a14b3f221339ea102d2aed1781f9617f416019c6 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 18:58:41 +0000 Subject: [PATCH 4/5] feat(logspace): write initialized compact fair-coin tables Enumerate every compact source/target pair from the actual zeroed counter program initializer on the original framed input. Reuse the existing word header, fair-coin input reader, counting-loop API, and row-major list API. Each two-bit entry records the exact count zero, one, or two, including coincident successors. Prove the entire transducer computable in native deterministic logarithmic space, with no preloaded parameter hypothesis. Move the existing STCON polynomial counter-bound proof into the shared configuration-graph layer and migrate STCON without weakening its result. Clocked enumeration, paired ports, the strict-forward-system bridge, and the recursive estimator remain open. No headline abstract or roadmap endpoint changes are warranted by this component milestone. Validation: strict direct Lean with project options and warningAsError=true passed without diagnostics for CounterBounds, FairCoin/Table, the new FairCoinTable tests, STCON Reduction, STCON Completeness, existing STCON tests, and existing FairCoinInput tests. Focused hygiene with --check-simp and git diff --check pass. New tests use actual initialized runs with 1458 output bits and nonzero input-dependent entries, coincident successors, empty input, and exponent zero. Full integration gates are left to PR CI. AI assistance: ChatGPT implementation worker coin_input_review authored this change. Independent non-author review is pending; the worker's prior review role on its parent change does not approve this implementation. Independent non-author agent polynomial_false_review approved exact source bb96980f7ce0502b155e116b8fff38bee416cb23 with no findings. Integrated source/test bytes match the reviewed revision. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 2 + .../Complexity/Problems/STCON/Reduction.lean | 23 +- .../ConfigurationGraph/CounterBounds.lean | 51 ++++ .../ConfigurationGraph/FairCoin/Table.lean | 288 ++++++++++++++++++ ComplexityTests/FairCoinTable.lean | 171 +++++++++++ 5 files changed, 514 insertions(+), 21 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean create mode 100644 ComplexityTests/FairCoinTable.lean diff --git a/Complexity.lean b/Complexity.lean index 54452f9614..3342168e09 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1528,9 +1528,11 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Basic 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.Expr public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ReadInput +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.Table 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.ReadSymbol diff --git a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean index 5472e88008..1e8e433436 100644 --- a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean +++ b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds /-! # The configuration graph as an instance of directed connectivity @@ -388,26 +389,6 @@ private theorem reachesOut_matrix (hL : w.length ≤ B) exact ⟨_, hreach, bounded_regs hL (by omega) (by omega) (by omega)⟩ -/-- The polynomial bound `((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1)` dominates -`vertexBound + 1`, `w.length`, and `2`. -/ -private theorem configurationInstance_bounds : - vertexBound (k := k) (radix D w.length) + 1 ≤ - ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ - w.length ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ - 2 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by - set L := w.length - set E := D * Fintype.card (Register k) - have hVB : vertexBound (k := k) (radix D L) = (L + 2) ^ E := vertexBound_eq_pow D L - have hpow : (L + 2) ^ E ≤ (2 * L + 2) ^ E := Nat.pow_le_pow_left (by omega) E - have hone : 1 ≤ (2 * L + 2) ^ E := Nat.one_le_pow _ _ (by omega) - have hB : ((frame w).length + 1) ^ (E + 1) = (2 * L + 2) ^ E * (2 * L + 2) := by - rw [length_frame, show 2 * L + 1 + 1 = 2 * L + 2 by omega, pow_succ] - have hmul : (2 * L + 2) ^ E * 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := - Nat.mul_le_mul_left _ (by omega) - have hmul' : 2 * L + 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := Nat.le_mul_of_pos_left _ hone - rw [hB] - exact ⟨by omega, by omega, by omega⟩ - /-- A `forCode` block in `writer` is at `b` when instructions `b`, `b + 1`, `b + 2` match. -/ private theorem codeAt_forCode {b u body exit : ℕ} {bound : Expr} (h₀ : (writer ntm D).instr b = .assign u (const 0) (b + 1)) @@ -429,7 +410,7 @@ theorem computableInLogSpace_configurationInstance : set S := startID ntm (radix D w.length) set B := ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) have hS : S < VB := startID_lt_vertexBound ntm c w.length - obtain ⟨hN, hL, h2⟩ := configurationInstance_bounds (k := k) (D := D) w + obtain ⟨hN, hL, h2⟩ := configurationCounter_bounds (k := k) D w have hreg (i : ℕ) (hi : i ≤ B) : ∀ r ∈ [w.length, i, 0, 0], r ≤ B := bounded_regs hL hi (by omega) (by omega) have hones₁ := reachesOut_ones (ntm := ntm) (D := D) w diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean new file mode 100644 index 0000000000..a018b8f44c --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean @@ -0,0 +1,51 @@ +/- +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.Bounds +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame + +/-! +# Polynomial counter bounds for configuration-graph writers + +The STCON writer and the fair-coin table writer enumerate the same polynomial compact box. +`configurationCounter_bounds` gives a common bound for the loop counters, original input length, +and ternary symbol/count scratch register in terms of the length of the framed input. + +## Main results + +* `Turing.MultiTapeNTM.ConfigurationGraph.configurationCounter_bounds`: the standard counter bound. +-/ + +public section + +namespace Turing.MultiTapeNTM.ConfigurationGraph + +open MultiTapeTM + +/-- The polynomial counter bound dominates the compact box plus one, the input length, and two. +The statement includes exponent zero and the empty original word. -/ +theorem configurationCounter_bounds {k : ℕ} (D : ℕ) (w : List Bool) : + vertexBound (k := k) (radix D w.length) + 1 ≤ + ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ + w.length ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧ + 2 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by + set L := w.length + set E := D * Fintype.card (Register k) + have hVB : vertexBound (k := k) (radix D L) = (L + 2) ^ E := vertexBound_eq_pow D L + have hpow : (L + 2) ^ E ≤ (2 * L + 2) ^ E := Nat.pow_le_pow_left (by omega) E + have hone : 1 ≤ (2 * L + 2) ^ E := Nat.one_le_pow _ _ (by omega) + have hB : ((frame w).length + 1) ^ (E + 1) = (2 * L + 2) ^ E * (2 * L + 2) := by + rw [length_frame, show 2 * L + 1 + 1 = 2 * L + 2 by omega, pow_succ] + have hmul : (2 * L + 2) ^ E * 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := + Nat.mul_le_mul_left _ (by omega) + have hmul' : 2 * L + 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := Nat.le_mul_of_pos_left _ hone + rw [hB] + exact ⟨by omega, by omega, by omega⟩ + +end Turing.MultiTapeNTM.ConfigurationGraph diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean new file mode 100644 index 0000000000..0d2733d780 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean @@ -0,0 +1,288 @@ +/- +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.FairCoin.ReadInput +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Words +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds +import Complexity.Foundations.Data.List.RowMajor + +/-! +# A native writer for the compact fair-coin table + +`coinTable` enumerates the polynomial compact box, including its guarded invalid IDs. Each entry +has two bits: `[false, false]`, `[true, false]`, or `[true, true]` records a coin count of zero, +one, or two. The order is row-major, with the two bits consecutive at each entry. + +`coinTableProgram` starts from its actual zeroed initializer on the original framed word. It +reads the input length with the existing word header, enumerates both compact IDs with bounded +counter loops, and calls `coinCountCode` for every entry. No input length or vertex ID is supplied +in advance. `computableInLogSpace_coinTable` is a native space certificate for the entire writer. + +This is the ambient ordinary coin-count table. Invalid compact IDs retain the existing edge +predicate's behavior. Clocked enumeration, the bridge to the strict-forward configuration system, +paired ports, and the recursive estimator remain separate. + +## Main definitions + +* `Turing.MultiTapePTM.ConfigurationGraph.coinTable`: the row-major two-bit count table. +* `Turing.MultiTapePTM.ConfigurationGraph.coinTableProgram`: its initialized counter transducer. + +## Main results + +* `Turing.MultiTapePTM.ConfigurationGraph.getD_coinTable`: the exact bit at a row-major index. +* `Turing.MultiTapePTM.ConfigurationGraph.coinTable_count`: decoding the two bits gives the count. +* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinTableProgram`: the actual initialized run. +* `Turing.MultiTapePTM.ConfigurationGraph.computableInLogSpace_coinTable`: native logarithmic space. +-/ + +public section + +namespace Turing.MultiTapePTM.ConfigurationGraph + +open MultiTapeNTM.ConfigurationGraph CounterProgram Instr Expr MultiTapeTM +open Cslib.Turing + +variable {k : ℕ} {State : Type} [Fintype State] + +/-- Every compact row and column, with two consecutive threshold bits encoding its coin count. +The original input is read at the source's existing `queryIndex`. -/ +noncomputable def coinTable (machine : MultiTapePTM k Bool State) (D : ℕ) (w : List Bool) : + List Bool := + let B := radix D w.length + let N := vertexBound (k := k) B + (List.finRange N).flatMap fun u : Fin N => (List.finRange N).flatMap fun v : Fin N => + List.ofFn fun b : Fin 2 => decide (b.val < + coinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B u]?) + +variable (machine : MultiTapePTM k Bool State) (D : ℕ) (w : List Bool) + +/-- The finite-index definition agrees with the natural-counter enumeration used by the writer. -/ +theorem coinTable_eq_flatMap : + coinTable machine D w = + (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun u => + (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v => + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + [decide (0 < c), decide (1 < c)] := by + have hval (n : ℕ) : (List.finRange n).map Fin.val = List.range n := by + apply List.ext_getElem <;> simp + dsimp only [coinTable] + conv_rhs => rw [← hval]; simp only [List.flatMap_map] + apply List.flatMap_congr + intro u _ + apply List.flatMap_congr + intro v _ + simp [List.ofFn_succ] + +/-- The table has exactly two bits for each ordered pair of compact IDs. -/ +@[simp] theorem length_coinTable : + (coinTable machine D w).length = + 2 * vertexBound (k := k) (radix D w.length) ^ 2 := by + dsimp only [coinTable] + simp_rw [List.flatMap_ofFn_prod] + simp only [List.length_ofFn] + ring + +/-- Reading either bit at its ordinary row-major address returns the corresponding threshold. -/ +theorem getD_coinTable + (u v : Fin (vertexBound (k := k) (radix D w.length))) (b : Fin 2) : + (coinTable machine D w).getD + (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + b.val) false = + decide (b.val < coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]?) := by + let p := finProdFinEquiv (u, finProdFinEquiv (v, b)) + have hp : 2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + b.val = p.val := by + simp only [p, finProdFinEquiv, Equiv.coe_fn_mk] + ring + rw [hp] + dsimp only [coinTable] + simp_rw [List.flatMap_ofFn_prod] + rw [List.getD_eq_getElem _ _ (by simp), List.getElem_ofFn] + simp only [Fin.eta, p, Equiv.symm_apply_apply] + +/-- Summing the two stored bits recovers the exact count, including coincident successors. -/ +theorem coinTable_count (u v : Fin (vertexBound (k := k) (radix D w.length))) : + ((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 = + coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? := by + have h0 := getD_coinTable machine D w u v 0 + have h1 := getD_coinTable machine D w u v 1 + simp only [Fin.val_zero, Fin.val_one, Nat.add_zero] at h0 h1 + rw [h0, h1] + have hc := coinCountWithSymbol_le_two machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + interval_cases coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? <;> rfl + +/-- The initialized writer. The header occupies labels zero to three, the two loops start at +four and seven, the count reader starts at ten, and labels sixteen to twenty-one emit its bits. +Label twenty-two halts. The four registers are length, row, column, and count scratch. -/ +@[expose] noncomputable def coinTableProgram : CounterProgram where + code := + Words.headerCode ++ + forCode 4 1 (vertexBoundExpr k (radixExpr D (reg 0))) 7 22 ++ + forCode 7 2 (vertexBoundExpr k (radixExpr D (reg 0))) 10 6 ++ + coinCountCode machine D 10 16 ++ + [lt (const 0) (reg 3) 17 18, emit true 19, emit false 19, + lt (const 1) (reg 3) 20 21, emit true 9, emit false 9, halt []] + registers := 4 + +variable {machine D w} {S : ℕ} + +private theorem bounded_regs {a b c d : ℕ} (ha : a ≤ S) (hb : b ≤ S) + (hc : c ≤ S) (hd : d ≤ S) : ∀ r ∈ [a, b, c, d], r ≤ S := by + simp only [List.mem_cons, List.not_mem_nil, or_false] + omega + +private theorem reachesOut_entry {u v y : ℕ} + (hregs : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) : + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + (coinTableProgram machine D).ReachesOut (frame w) ((coinTableProgram machine D).Active S) + (10, [w.length, u, v, y]) (9, [w.length, u, v, c]) + [decide (0 < c), decide (1 < c)] := by + let P := coinTableProgram machine D + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + have hc : c ≤ 2 := coinCountWithSymbol_le_two .. + have hb : ∀ r ∈ [w.length, u, v, c], r ≤ S := + bounded_regs (hregs _ (by simp)) (hregs _ (by simp)) (hregs _ (by simp)) (hc.trans h2) + have hcode : P.CodeAt 10 (coinCountCode machine D 10 16) := by + simp only [coinCountCode, readSymbolCode, codeAt_append, + codeAt_cons, codeAt_nil, and_true] + exact ⟨⟨rfl, rfl, rfl, rfl, rfl⟩, rfl⟩ + have hr := reachesOut_coinCountCode machine hcode hregs h2 + have hfirst : P.ReachesOut (frame w) (P.Active S) + (16, [w.length, u, v, c]) (19, [w.length, u, v, c]) [decide (0 < c)] := by + refine ReachesOut.lt (show P.instr 16 = _ from rfl) hb ?_ + simp only [eval_const, eval_reg, List.getD_cons_zero, List.getD_cons_succ] + by_cases h : 0 < c + · simpa [h] using ReachesOut.emit (show P.instr 17 = _ from rfl) hb (ReachesOut.refl _) + · simpa [h] using ReachesOut.emit (show P.instr 18 = _ from rfl) hb (ReachesOut.refl _) + have hsecond : P.ReachesOut (frame w) (P.Active S) + (19, [w.length, u, v, c]) (9, [w.length, u, v, c]) [decide (1 < c)] := by + refine ReachesOut.lt (show P.instr 19 = _ from rfl) hb ?_ + simp only [eval_const, eval_reg, List.getD_cons_zero, List.getD_cons_succ] + by_cases h : 1 < c + · simpa [h] using ReachesOut.emit (show P.instr 20 = _ from rfl) hb (ReachesOut.refl _) + · simpa [h] using ReachesOut.emit (show P.instr 21 = _ from rfl) hb (ReachesOut.refl _) + exact (hr.trans (hfirst.trans hsecond)).of_eq (by simp [c]) + +private theorem reachesOut_row + (hL : w.length ≤ S) (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S) + {u x y : ℕ} (hu : u < vertexBound (k := k) (radix D w.length)) + (hx : x ≤ vertexBound (k := k) (radix D w.length)) (hy : y ≤ 2) : + ∃ y' ≤ 2, (coinTableProgram machine D).ReachesOut (frame w) + ((coinTableProgram machine D).Active S) + (7, [w.length, u, x, y]) + (6, [w.length, u, vertexBound (k := k) (radix D w.length), y']) + ((List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v => + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + [decide (0 < c), decide (1 < c)]) := by + have hcode : (coinTableProgram machine D).CodeAt 7 + (forCode 7 2 (vertexBoundExpr k (radixExpr D (reg 0))) 10 6) := by + simp only [forCode, codeAt_cons, codeAt_nil, and_true] + exact ⟨rfl, rfl, rfl⟩ + obtain ⟨regs', hreach, y', rfl, -, hy'⟩ := reachesOut_forCode (w := frame w) + (o := fun v => + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + [decide (0 < c), decide (1 < c)]) + (N := vertexBound (k := k) (radix D w.length)) hcode + (fun v regs => ∃ y, regs = [w.length, u, v, y] ∧ + v ≤ vertexBound (k := k) (radix D w.length) ∧ y ≤ 2) hN + (by + rintro v regs ⟨y, rfl, hv, hy⟩ + exact ⟨rfl, by simp, by simp, bounded_regs hL (by omega) (by omega) (by omega)⟩) + (by + rintro v hv regs ⟨y, rfl, -, hy⟩ + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + have hc : c ≤ 2 := coinCountWithSymbol_le_two .. + exact ⟨[w.length, u, v, c], + reachesOut_entry (bounded_regs hL (by omega) (by omega) (by omega)) h2, + rfl, bounded_regs hL (by omega) (by omega) (hc.trans h2), c, by simp, by omega, hc⟩) + [w.length, u, x, y] (bounded_regs hL (by omega) (by omega) (by omega)) + ⟨y, by simp, by omega, hy⟩ + exact ⟨y', hy', hreach⟩ + +private theorem reachesOut_table + (hL : w.length ≤ S) (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S) : + ∃ regs, (coinTableProgram machine D).ReachesOut (frame w) + ((coinTableProgram machine D).Active S) + (4, [w.length, 0, 0, 0]) (22, regs) (coinTable machine D w) ∧ + ∀ r ∈ regs, r ≤ S := by + have hcode : (coinTableProgram machine D).CodeAt 4 + (forCode 4 1 (vertexBoundExpr k (radixExpr D (reg 0))) 7 22) := by + simp only [forCode, codeAt_cons, codeAt_nil, and_true] + exact ⟨rfl, rfl, rfl⟩ + obtain ⟨regs', hreach, x, y, rfl, -, hx, hy⟩ := reachesOut_forCode (w := frame w) + (o := fun u => (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v => + let c := coinCountWithSymbol machine (radix D w.length) w.length u v + w[queryIndex (k := k) (radix D w.length) u]? + [decide (0 < c), decide (1 < c)]) + (N := vertexBound (k := k) (radix D w.length)) hcode + (fun u regs => ∃ x y, regs = [w.length, u, x, y] ∧ + u ≤ vertexBound (k := k) (radix D w.length) ∧ + x ≤ vertexBound (k := k) (radix D w.length) ∧ y ≤ 2) hN + (by + rintro u regs ⟨x, y, rfl, hu, hx, hy⟩ + exact ⟨rfl, by simp, by simp, bounded_regs hL (by omega) (by omega) (by omega)⟩) + (by + rintro u hu regs ⟨x, y, rfl, -, hx, hy⟩ + obtain ⟨y', hy', hr⟩ := reachesOut_row (machine := machine) hL hN h2 hu hx hy + exact ⟨_, hr, rfl, bounded_regs hL (by omega) (by omega) (by omega), + _, y', by simp, by omega, le_rfl, hy'⟩) + [w.length, 0, 0, 0] (bounded_regs hL (by omega) (by omega) (by omega)) + ⟨0, 0, by simp, by omega, by omega, by omega⟩ + exact ⟨_, hreach.of_eq (coinTable_eq_flatMap machine D w).symm, + bounded_regs hL (by omega) (by omega) (by omega)⟩ + +variable (machine D w) + +/-- The actual zero-initialized program counts the input length, enumerates every compact pair, +emits the whole table, and reaches its halt with all final registers within the common bound. -/ +theorem reachesOut_coinTableProgram + (hinput : (frame w).length ≤ S) + (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S) : + ∃ regs, (coinTableProgram machine D).ReachesOut (frame w) + ((coinTableProgram machine D).Active S) (coinTableProgram machine D).init + (22, regs) (coinTable machine D w) ∧ ∀ r ∈ regs, r ≤ S := by + have hcode : (coinTableProgram machine D).CodeAt 0 Words.headerCode := by + simp only [Words.headerCode, codeAt_cons, codeAt_nil, and_true] + exact ⟨rfl, rfl, rfl, rfl⟩ + have hh := Words.reachesOut_header (w := w) (k := 0) hcode (by + simpa only [length_frame, Nat.add_zero] using hinput) + simp only [List.replicate_zero, List.append_nil] at hh + have hL : w.length ≤ S := by rw [length_frame] at hinput; omega + obtain ⟨regs, hr, hregs⟩ := reachesOut_table (machine := machine) hL hN h2 + exact ⟨regs, (hh.trans hr).of_eq (by simp), hregs⟩ + +/-- The entire compact coin table is computed from the original framed word in native +deterministic logarithmic space. No parameters or counters are preloaded. -/ +theorem computableInLogSpace_coinTable : + ComputableInLogSpace (coinTable machine D) (encFramed encBits) encBits := by + refine (coinTableProgram machine D).computableInLogSpace_of_reachesOut + (D * Fintype.card (Register k) + 1) fun w => ?_ + simp only [encFramed_apply, encBits_apply] + obtain ⟨hN, _, h2⟩ := configurationCounter_bounds (k := k) D w + have hinput : (frame w).length ≤ + ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by + rw [pow_succ] + have hone : 1 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k)) := + Nat.one_le_pow _ _ (by omega) + exact (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ hone) + obtain ⟨regs, hr, hregs⟩ := reachesOut_coinTableProgram machine D w hinput (by omega) h2 + exact ⟨(22, regs), _, [], hr, rfl, by simp, hregs⟩ + +end Turing.MultiTapePTM.ConfigurationGraph diff --git a/ComplexityTests/FairCoinTable.lean b/ComplexityTests/FairCoinTable.lean new file mode 100644 index 0000000000..e1f117f303 --- /dev/null +++ b/ComplexityTests/FairCoinTable.lean @@ -0,0 +1,171 @@ +/- +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.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.Table +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader + +/-! +# Initialized fair-coin table runs + +A concrete machine's entire 1458-bit table is emitted from zero registers on its original framed +one-bit input. At one fixed row and column, the two output bits change from `[true, false]` to +`[false, false]` when only the original input bit changes, and to `[true, true]` when the two coin +successors coincide. The output index is the ordinary row-major index, not an assumed oracle. +The empty input and exponent-zero compact box also have actual initialized runs. +-/ + +namespace ComplexityTests.FairCoinTable + +open Cslib.Turing Turing MultiTapeTM CounterProgram Instr +open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph + +private def machine (different : Bool) : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ bit := + .step + { inputTape := 0 + workTapes := Fin.elim0 + output := some (symbol.getD false && (if different then bit else true)) + state := none } + Empty.elim Empty.elim + +private def running (input : Bool) : FiniteCfg 0 Bool Unit := + ⟨[input], some (), 1, Fin.elim0, []⟩ + +private def stopped (input output : Bool) : FiniteCfg 0 Bool Unit := + ⟨[input], none, 1, Fin.elim0, [output]⟩ + +private theorem viewCoinStep_running (different input bit : Bool) : + (machine different).viewCoinStep (running input) bit = + stopped input (input && (if different then bit else true)) := by + cases different <;> cases input <;> cases bit <;> + simp [MultiTapePTM.viewCoinStep, running, FiniteCfg.inputSymbol_eq_getD, machine, + MultiTapePTM.withCoin, MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv, + FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, stopped, funext_iff] + +private theorem stopped_injective (input : 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 fits_three (v : FiniteCfg 0 Bool Unit) (hinput : v.input.length = 1) : + Fits 3 (registers v) := by + intro i + cases i with + | inputPos => + change v.inputPos.val < 3 + simpa only [hinput] using v.inputPos.isLt + | control => + have h : stateCode v.state < 2 := (Fintype.equivFin (Option Unit) v.state).isLt + exact h.trans_le (by decide) + | output => exact outputCode_lt _ + | head i => exact Fin.elim0 i + | left i => exact Fin.elim0 i + | right i => exact Fin.elim0 i + +private noncomputable def source : ℕ := vertexID 3 (running true) + +private noncomputable def target : ℕ := vertexID 3 (stopped true true) + +private noncomputable def address : ℕ := 2 * (source * 27 + target) + +-- Input symbols are absent from the compact IDs, so all runs use the same table address. +example (input : Bool) : vertexID 3 (running input) = source ∧ + vertexID 3 (stopped input true) = target := ⟨rfl, rfl⟩ + +private theorem count_input (different input : Bool) : + coinCountWithSymbol (machine different) 3 1 source target + [input][queryIndex (k := 0) 3 source]? = + if input then (if different then 1 else 2) else 0 := by + change coinCountWithSymbol (machine different) 3 1 + (vertexID 3 (running input)) (vertexID 3 (stopped input true)) + [input][queryIndex (k := 0) 3 (vertexID 3 (running input))]? = _ + have hcoin (bit : Bool) := edgeWithSymbol_withCoin_iff (machine different) + (a := running input) (b := stopped input true) rfl + (by simp [running, MultiTapeNTM.outputClass]) + (by simp [stopped, MultiTapeNTM.outputClass]) + (fits_three _ rfl) (fits_three _ rfl) bit + simp only [viewCoinStep_running, (stopped_injective input).eq_iff] at hcoin + have hfalse := hcoin false + have htrue := hcoin true + rw [coinCountWithSymbol] + cases input <;> cases different <;> simp_all [running] + +private theorem table_bits (different input : Bool) : + (coinTable (machine different) 1 [input]).getD address false = input ∧ + (coinTable (machine different) 1 [input]).getD (address + 1) false = + (input && !different) := by + have hbox : vertexBound (k := 0) 3 = 27 := by decide + have hu : source < vertexBound (k := 0) 3 := vertexID_lt (fits_three (running true) rfl) + have hv : target < vertexBound (k := 0) 3 := vertexID_lt (fits_three (stopped true true) rfl) + let u : Fin (vertexBound (k := 0) (radix 1 [input].length)) := ⟨source, hu⟩ + let v : Fin (vertexBound (k := 0) (radix 1 [input].length)) := ⟨target, hv⟩ + have h0 := getD_coinTable (machine different) 1 [input] u v 0 + have h1 := getD_coinTable (machine different) 1 [input] u v 1 + change (coinTable (machine different) 1 [input]).getD + (2 * (source * vertexBound (k := 0) 3 + target) + 0) false = + decide (0 < coinCountWithSymbol (machine different) 3 1 source target + [input][queryIndex (k := 0) 3 source]?) at h0 + change (coinTable (machine different) 1 [input]).getD + (2 * (source * vertexBound (k := 0) 3 + target) + 1) false = + decide (1 < coinCountWithSymbol (machine different) 3 1 source target + [input][queryIndex (k := 0) 3 source]?) at h1 + rw [hbox, count_input] at h0 h1 + cases input <;> cases different <;> simp_all [address] + +private theorem initialized_run (different input : Bool) : + ∃ regs out, (coinTableProgram (machine different) 1).ReachesOut (frame [input]) + ((coinTableProgram (machine different) 1).Active 27) + (0, [0, 0, 0, 0]) (22, regs) out ∧ + out.length = 1458 ∧ out.getD address false = input ∧ + out.getD (address + 1) false = (input && !different) := by + obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine different) 1 [input] + (S := 27) (by simp) (by change 27 ≤ 27; rfl) (by decide) + exact ⟨regs, coinTable (machine different) 1 [input], hr, + by rw [length_coinTable]; change 2 * 27 ^ 2 = 1458; norm_num, (table_bits different input).1, + (table_bits different input).2⟩ + +-- One accepting coin, with all parameters counted or enumerated from zero registers. +example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame [true]) + ((coinTableProgram (machine true) 1).Active 27) + (0, [0, 0, 0, 0]) (22, regs) out ∧ + out.length = 1458 ∧ out.getD address false = true ∧ + out.getD (address + 1) false = false := initialized_run true true + +-- Changing just the original input bit changes the same table entry to count zero. +example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame [false]) + ((coinTableProgram (machine true) 1).Active 27) + (0, [0, 0, 0, 0]) (22, regs) out ∧ + out.length = 1458 ∧ out.getD address false = false ∧ + out.getD (address + 1) false = false := initialized_run true false + +-- The same entry records two when the two coin successors coincide. +example : ∃ regs out, (coinTableProgram (machine false) 1).ReachesOut (frame [true]) + ((coinTableProgram (machine false) 1).Active 27) + (0, [0, 0, 0, 0]) (22, regs) out ∧ + out.length = 1458 ∧ out.getD address false = true ∧ + out.getD (address + 1) false = true := initialized_run false true + +-- Empty original input still counts its marker correctly and emits all 8 × 8 entries. +example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame []) + ((coinTableProgram (machine true) 1).Active 8) + (0, [0, 0, 0, 0]) (22, regs) out ∧ out.length = 128 := by + obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine true) 1 [] + (S := 8) (by decide) (by decide) (by decide) + exact ⟨regs, _, hr, by rw [length_coinTable]; decide⟩ + +-- Exponent zero produces a one-entry ambient box, with the count scratch still bounded by two. +example : ∃ regs out, (coinTableProgram (machine true) 0).ReachesOut (frame []) + ((coinTableProgram (machine true) 0).Active 2) + (0, [0, 0, 0, 0]) (22, regs) out ∧ out.length = 2 := by + obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine true) 0 [] + (S := 2) (by decide) (by decide) (by decide) + exact ⟨regs, _, hr, by rw [length_coinTable]; decide⟩ + +-- The final label is a halt; the entire counted table is emitted before reaching it. +example (different : Bool) : (coinTableProgram (machine different) 1).instr 22 = halt [] := rfl + +end ComplexityTests.FairCoinTable From 9895598086f473b8e12fe78a87b1f4d932451a11 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 19:34:00 +0000 Subject: [PATCH 5/5] feat(logspace): identify the clocked ambient configuration matrix Connect the initialized native coin-count table to the matrix on every compact configuration ID. Prove deterministic target uniqueness on arbitrary IDs, nonnegative substochastic rows, and exact finite-time machine acceptance from the original logarithmic-space witness, deriving the initial ID and all fitting conditions internally. Reuse time layering on explicit Fin ((T+1)*N) identifiers, preserving numeric strict forwardness, terminal reward, bounded potential and inverse equations. The real-valued BPL endpoint keeps the original space constant and supplies a polynomial dimension and the actual two-thirds versus one-third gap. Reusable pieces are closed-submatrix multiplication/power restriction, finite clock reindexing, and a shared polynomial bound for the clocked compact box. Expose the existing canonical reachable-output lemma instead of re-proving it. Clocked native serialization, directed paired ports and the native recursive estimator remain open; this is not BPL containment in L. Validation on the exact changes from published parent a14b3f221339ea102d2aed1781f9617f416019c6: - All seven changed/new library modules and the concrete new test pass the pinned Lean 4.36.0-rc2 compiler with project options, warningAsError and --error=warning, using private artifacts and existing read-only dependencies. - Eight affected existing source/test checks pass: FairCoin/Table, STCON Reduction and Completeness, randomized TimeLayer, and FairCoinConfigurationReader, FairCoinTable, TimeLayer and STCON tests. - Regression cases cover malformed in-box IDs, an overflowing rejecting branch with exact surviving row mass one half, actual finite-coin acceptance through both matrix bridges, numeric clock splitting, terminal-only reward and zero terminal rows, plus a concrete always-accepting BPL witness. - Focused check_hygiene.py --check-simp and git diff --check pass. Full project gates and aggregate registration are delegated to integration CI. AI assistance: ChatGPT worker coin_input_review authored and self-checked this change. A separate read-only helper identified existing matrix transport APIs. Independent non-author review of the frozen revision is pending coordinator integration; self-checking is not independent or human approval. Independent non-author agent polynomial_false_review approved exact source e3528ff495f376640e72a89414a7b85223ff1ca0 with no findings. Integration preserves the reviewed source/test bytes. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 5 + .../LogSpace/Randomized/CompactMatrix.lean | 203 +++++++++++++++ .../LogSpace/Randomized/CompactTimeLayer.lean | 143 ++++++++++ .../Randomized/ConfigurationReader.lean | 3 +- .../ConfigurationGraph/CounterBounds.lean | 24 ++ .../ConfigurationGraph/Deterministic.lean | 94 +++++++ .../LinearAlgebra/Matrix/ClosedSubmatrix.lean | 53 ++++ .../LinearAlgebra/Matrix/TimeLayer/Fin.lean | 144 ++++++++++ .../CompactConfigurationMatrix.lean | 245 ++++++++++++++++++ 9 files changed, 913 insertions(+), 1 deletion(-) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Deterministic.lean create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/ClosedSubmatrix.lean create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/TimeLayer/Fin.lean create mode 100644 ComplexityTests/CompactConfigurationMatrix.lean diff --git a/Complexity.lean b/Complexity.lean index 3342168e09..56faac5188 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1067,6 +1067,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.TimeLayer @@ -1529,6 +1531,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 @@ -2700,6 +2703,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 @@ -2715,6 +2719,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