From 406a68d5c75e9ccf0ba540a18676d794046d1263 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:50:25 +0000 Subject: [PATCH 1/3] 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 9735d61c9..7c91ae592 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 000000000..9ba13cdb2 --- /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 000000000..1869f761e --- /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 000000000..5341a4f0b --- /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 000000000..b5623a8ee --- /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/3] 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 7c91ae592..92db55da7 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 000000000..536fa5978 --- /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 000000000..63147d80d --- /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 000000000..861671546 --- /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/3] 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 92db55da7..54452f961 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 8020124d9..5472e8800 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 000000000..c75e73a3a --- /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 000000000..1e5b8940e --- /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 000000000..4c41283fa --- /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