From 406a68d5c75e9ccf0ba540a18676d794046d1263 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:50:25 +0000 Subject: [PATCH] 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