From f64dca005030dcbcef0004bf8fb864d5d5e317bd Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:32:37 +0000 Subject: [PATCH 1/2] feat(LogSpace): configuration matrix of fair-coin machines (#474) Coin-driven transition matrices (Foundations) and, for a fair-coin machine on a closed set of views, the acceptance probability as an entry of N^t e, of the substochastic sum, and of (1 - S/2)^-1 e. BPL through polynomial-size configuration matrices. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Classes/LogSpace/Randomized.lean | 2 + .../Randomized/ConfigurationMatrix.lean | 379 ++++++++++++++++++ .../Complexity/LogSpace/Configurations.lean | 24 ++ .../Complexity/LogSpace/HaltingTime.lean | 26 +- .../Complexity/LogSpace/Reachability.lean | 16 +- .../LinearAlgebra/Matrix/CoinStep.lean | 204 ++++++++++ ComplexityTests/CoinStepMatrix.lean | 58 +++ ComplexityTests/RandomizedLogSpace.lean | 48 +++ references.bib | 21 + 10 files changed, 742 insertions(+), 38 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean create mode 100644 ComplexityTests/CoinStepMatrix.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..dccd11920 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1003,6 +1003,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Tr public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs @@ -2620,6 +2621,7 @@ public import Complexity.Foundations.LinearAlgebra.ExchangeReplacement public import Complexity.Foundations.LinearAlgebra.ImageSparsification public import Complexity.Foundations.LinearAlgebra.Interpolation public import Complexity.Foundations.LinearAlgebra.KernelVector +public import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep public import Complexity.Foundations.LinearAlgebra.Matrix.CutRank public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean index 414ac55d3..a1f91e687 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean @@ -32,6 +32,8 @@ instance. The threshold `1/2` for `RL` can be raised to `1 - 2 ^ (-r)` for any fixed `r` by repetition (`Cslib.Complexity.mem_RL_iff_error_le`), which also gives `Cslib.Complexity.RL_subset_BPL`. +The acceptance probability is an entry of a power or inverse of a polynomial-size configuration +matrix (`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). The model follows the decision recorded in issue #474: one-way coins, halting on every branch with the polynomial clock a derived lemma, acceptance by counting coin strings, and space as for `NL` diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean new file mode 100644 index 000000000..7f786876f --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean @@ -0,0 +1,379 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized +public import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep + +/-! +# The configuration matrix of a fair-coin machine + +A fair-coin machine moves each running view (`Turing.FiniteCfg`, the configuration with its work +tapes stored relative to their heads and its output summarized) to one of two views, selected by +the coin (`Turing.MultiTapePTM.viewCoinStep`); a halted view stays put. On a finite set `V` of +views closed under these steps, this gives two matrices indexed by `V`: + +* the *configuration matrix* `Turing.MultiTapePTM.configMatrix`, whose entry `(x, y)` counts the + coins moving `x` to `y`, so that half of it is the stochastic matrix of the run, with halted + views absorbing; +* the *live configuration matrix* `Turing.MultiTapePTM.liveConfigMatrix`, the same rows at + running views and zero rows at halted views, so that half of it is substochastic. + +With `e` the indicator of the accepting halted views (`Turing.FiniteCfg.acceptVec`), the number of +accepting coin strings of length `t` is the entry at the initial view of `N ^ t *ᵥ e` +(`Turing.MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec`), so the acceptance probability is +`((N / 2) ^ t *ᵥ e)(start)`. Splitting the coin strings by the time they halt gives the +substochastic form `∑ t ≤ T, ((S / 2) ^ t *ᵥ e)(start)` +(`Turing.MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix`). When every view of `V` is +reachable and every branch halts within `T` steps, `S / 2` is nilpotent, and the acceptance +probability is `((1 - S / 2)⁻¹ *ᵥ e)(start)` +(`Turing.MultiTapePTM.acceptCoins_div_eq_inv_mulVec`). + +The reachable views form such a set (`Turing.MultiTapePTM.exists_finset_reachable`), with at most +`2 ^ (2 * coreLengthBound k State n s + 1)` elements under a space bound `s`, polynomially many +under a logarithmic one. So a `BPL` language is decided by the entry at the initial view of +`(1 - S / 2)⁻¹ *ᵥ e` for a polynomial-size matrix `S` +(`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). This is the Markov chain of a probabilistic +machine on its configurations [Gill][Gill1977], whose powers and inverse Borodin, Cook and +Pippenger compute in parallel to place probabilistic space `s` in `DSPACE(s²)` +[Borodin, Cook and Pippenger][BorodinCookPippenger1983]; for `BPL` this gives +`BPL ⊆ DSPACE(log² n)` and `BPL ⊆ P` [Hoza, Section 4.3][Hoza2022]. Those algorithms are not +formalized here. + +The matrices are indexed by an arbitrary closed set of views rather than a set of +configurations of bounded size, and have no time layers: the model of `Cslib.Complexity.BPL` +requires every branch to halt, which already makes the live matrix nilpotent on the reachable +views. The form `N ^ t` with absorbing halted views is the one repeated squaring computes; the +form `(1 - S / 2)⁻¹` with a nilpotent substochastic matrix is the one of matrix inversion. + +## Main definitions + +* `Turing.MultiTapePTM.viewCoinStep`: the view reached under one coin. +* `Turing.FiniteCfg.acceptVec`: the indicator of the accepting halted views. +* `Turing.MultiTapePTM.configMatrix`, `Turing.MultiTapePTM.liveConfigMatrix`: the configuration + matrix and its rows at running views. + +## Main results + +* `Turing.MultiTapePTM.viewRep_foldl_viewCoinStep`: coin steps of views follow coin replays. +* `Turing.MultiTapePTM.reflTransGen_viewStep_toNTM_iff`: the reachable views are those reached by + coin strings. +* `Turing.MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec`: accepting coin strings are an + entry of a power of the configuration matrix. +* `Turing.MultiTapePTM.acceptCoins_div_eq_configMatrix_pow_mulVec`: the acceptance probability + is an entry of a power of the stochastic matrix. +* `Turing.MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix`: the substochastic form. +* `Turing.MultiTapePTM.liveConfigMatrix_pow_eq_zero`: under a halting time, the live matrix is + nilpotent on reachable views. +* `Turing.MultiTapePTM.acceptCoins_div_eq_inv_mulVec`: the acceptance probability is an entry of + `(1 - S / 2)⁻¹ *ᵥ e`. +* `Turing.MultiTapePTM.exists_finset_reachable`: the reachable views form a small closed set. +* `Cslib.Complexity.exists_configMatrix_of_mem_BPL`: `BPL` through polynomial-size configuration + matrices. + +## References + +* [A. Borodin, S. Cook, N. Pippenger, *Parallel computation for well-endowed rings and + space-bounded probabilistic machines*][BorodinCookPippenger1983] +* [W. Hoza, *Recent progress on derandomizing space-bounded computation*][Hoza2022] +* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977] +-/ + +@[expose] public section + +open Cslib.Turing + +namespace Turing + +open scoped Classical in +/-- The indicator of the accepting halted views in a set `V` of views: `1` at the halted views +with output `[true]`, `0` elsewhere. -/ +noncomputable def FiniteCfg.acceptVec {k : ℕ} {State : Type} (R : Type*) [Zero R] [One R] + (V : Finset (FiniteCfg k Bool State)) : V → R := + fun v => if (v : FiniteCfg k Bool State).state = none ∧ + (v : FiniteCfg k Bool State).output = [true] then 1 else 0 + +namespace MultiTapePTM + +open MultiTapeMachine Matrix + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) + +/-- **The view reached under one coin**: a halted view stays put; a running view takes the action +selected by the coin, and its output is summarized. -/ +noncomputable def viewCoinStep (finite : FiniteCfg k Bool State) (bit : Bool) : + FiniteCfg k Bool State := + match finite.state with + | none => finite + | some state => (finite.step ((machine.withCoin bit).toTM.tr state finite.inputSymbol + finite.workTapeSymbols)).summarizeOutput + +open scoped Classical in +/-- **The configuration matrix** on a set `V` of views: the entry at `(x, y)` counts the coins +that move `x` to `y`. Half of it is the stochastic matrix of the run, with halted views +absorbing. -/ +noncomputable def configMatrix (R : Type*) [CommSemiring R] (V : Finset (FiniteCfg k Bool State)) : + Matrix V V R := + Matrix.coinStepMatrix machine.viewCoinStep V + +open scoped Classical in +/-- **The live configuration matrix**: the rows of `Turing.MultiTapePTM.configMatrix` at running +views, and zero rows at halted views. Half of it is substochastic. -/ +noncomputable def liveConfigMatrix (R : Type*) [CommSemiring R] + (V : Finset (FiniteCfg k Bool State)) : Matrix V V R := + Matrix.liveCoinStepMatrix machine.viewCoinStep V fun finite => finite.state ≠ none + +variable {machine} + +/-- A halted view stays put. -/ +theorem viewCoinStep_of_halted {finite : FiniteCfg k Bool State} (h : finite.state = none) + (bit : Bool) : machine.viewCoinStep finite bit = finite := by + simp only [viewCoinStep, h] + +/-- **Coin steps of views follow coin steps of configurations.** -/ +theorem viewRep_viewCoinStep {input : List Bool} {finite : FiniteCfg k Bool State} + {cfg : Cfg k Bool State input} (h : MultiTapeNTM.ViewRep finite cfg) (bit : Bool) : + MultiTapeNTM.ViewRep (machine.viewCoinStep finite bit) + ((machine.withCoin bit).toTM.step cfg) := by + rcases hs : cfg.state with _ | state + · rw [MultiTapeTM.step_of_halt hs, viewCoinStep_of_halted (h.state.trans hs)] + exact h + · obtain ⟨hin, hwork⟩ := h.symbols + rw [MultiTapeTM.step_of_state hs] + simp only [MultiTapePTM.viewCoinStep, h.state.trans hs, hin, hwork] + exact h.step _ + +/-- **Coin strings replay on views as on configurations.** -/ +theorem viewRep_foldl_viewCoinStep {input : List Bool} {finite : FiniteCfg k Bool State} + {cfg : Cfg k Bool State input} (h : MultiTapeNTM.ViewRep finite cfg) (coins : List Bool) : + MultiTapeNTM.ViewRep (coins.foldl machine.viewCoinStep finite) + (machine.stepCoins coins cfg) := by + induction coins generalizing finite cfg with + | nil => exact h + | cons bit coins ih => exact ih (viewRep_viewCoinStep h bit) + +/-- The steps of the views of the nondeterministic view are the coin steps. -/ +theorem viewStep_toNTM_iff {finite next : FiniteCfg k Bool State} : + machine.toNTM.ViewStep finite next ↔ ∃ bit, machine.viewCoinStep finite bit = next := by + rcases hs : finite.state with _ | state + · simp only [MultiTapeNTM.ViewStep, hs, viewCoinStep_of_halted hs, exists_const] + exact eq_comm + · simp only [MultiTapeNTM.ViewStep, hs, viewCoinStep, tr_toNTM_iff, MultiTapeTM.tr_iff] + constructor + · rintro ⟨action, ⟨bit, rfl⟩, rfl⟩ + exact ⟨bit, rfl⟩ + · rintro ⟨bit, rfl⟩ + exact ⟨_, ⟨bit, rfl⟩, rfl⟩ + +/-- **The reachable views are those reached by coin strings.** -/ +theorem reflTransGen_viewStep_toNTM_iff {finite next : FiniteCfg k Bool State} : + Relation.ReflTransGen machine.toNTM.ViewStep finite next ↔ + ∃ coins : List Bool, coins.foldl machine.viewCoinStep finite = next := by + constructor + · intro h + induction h with + | refl => exact ⟨[], rfl⟩ + | tail _ hstep ih => + obtain ⟨coins, rfl⟩ := ih + obtain ⟨bit, rfl⟩ := viewStep_toNTM_iff.mp hstep + exact ⟨coins ++ [bit], by simp⟩ + · rintro ⟨coins, rfl⟩ + induction coins using List.reverseRecOn with + | nil => exact .refl + | append_singleton coins bit ih => + rw [List.foldl_append, List.foldl_cons, List.foldl_nil] + exact ih.tail (viewStep_toNTM_iff.mpr ⟨bit, rfl⟩) + +/-- The accepting coin strings are those whose replay on views ends in an accepting halted +view. -/ +private theorem acceptCoins_eq_card_views (input : List Bool) (t : ℕ) : + machine.acceptCoins input t = (Finset.univ.filter fun w : Fin t → Bool => + ((List.ofFn w).foldl machine.viewCoinStep (machine.toNTM.initView input)).state = none ∧ + ((List.ofFn w).foldl machine.viewCoinStep (machine.toNTM.initView input)).output = + [true]).card := by + classical + unfold acceptCoins + congr 1 + refine Finset.filter_congr fun w _ => ?_ + have h := viewRep_foldl_viewCoinStep (machine := machine) + (MultiTapeNTM.viewRep_init (ntm := machine.toNTM) input) (List.ofFn w) + rw [h.state, h.output, MultiTapeNTM.outputClass_eq_true_iff] + +open scoped Classical in +/-- **Accepting coin strings are an entry of a power of the configuration matrix**: on a set `V` +of views that contains the initial view and is closed under coin steps, the number of accepting +coin strings of length `t` is the entry at the initial view of `N ^ t *ᵥ e`. -/ +theorem acceptCoins_eq_configMatrix_pow_mulVec (R : Type*) [CommSemiring R] {input : List Bool} + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (t : ℕ) : + (machine.acceptCoins input t : R) = + (machine.configMatrix R V ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + classical + have := Matrix.coinStepMatrix_pow_mulVec (R := R) hV + (fun finite : FiniteCfg k Bool State => + if finite.state = none ∧ finite.output = [true] then 1 else 0) t ⟨_, hinit⟩ + rw [configMatrix] + convert this.symm using 1 + · rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_one, + acceptCoins_eq_card_views] + · rfl + +open scoped Classical in +/-- **The acceptance probability is an entry of a power of the stochastic matrix**: with +`P = N / 2` the stochastic matrix of the run, `acceptCoins input t / 2 ^ t` is the entry at the +initial view of `P ^ t *ᵥ e`. -/ +theorem acceptCoins_div_eq_configMatrix_pow_mulVec (R : Type*) [Field R] {input : List Bool} + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (t : ℕ) : + (machine.acceptCoins input t : R) / 2 ^ t = + (((2 : R)⁻¹ • machine.configMatrix R V) ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + rw [smul_pow, Matrix.smul_mulVec, Pi.smul_apply, + ← acceptCoins_eq_configMatrix_pow_mulVec R hV hinit, smul_eq_mul, inv_pow, div_eq_inv_mul] + +open scoped Classical in +/-- **The substochastic form**: splitting the coin strings by the time the run halts, +`acceptCoins input T / 2 ^ T` is the entry at the initial view of `∑ t ≤ T, (S / 2) ^ t *ᵥ e`, +with `S` the live configuration matrix. No halting time is needed. -/ +theorem acceptCoins_div_eq_sum_liveConfigMatrix (R : Type*) [Field R] [CharZero R] + {input : List Bool} {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (T : ℕ) : + (machine.acceptCoins input T : R) / 2 ^ T = ∑ t ∈ Finset.range (T + 1), + (((2 : R)⁻¹ • machine.liveConfigMatrix R V) ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + classical + have h := Matrix.coinStepMatrix_pow_mulVec_eq_sum (R := R) hV + (live := fun finite : FiniteCfg k Bool State => finite.state ≠ none) + (fun finite hfinite => viewCoinStep_of_halted (not_not.mp hfinite)) + (f := fun finite : FiniteCfg k Bool State => + if finite.state = none ∧ finite.output = [true] then 1 else 0) + (fun finite hfinite => ite_eq_right_iff.mpr fun h => absurd h.1 hfinite) T ⟨_, hinit⟩ + have hvec : (fun v : V => if (v : FiniteCfg k Bool State).state = none ∧ + (v : FiniteCfg k Bool State).output = [true] then (1 : R) else 0) = + FiniteCfg.acceptVec R V := rfl + rw [hvec] at h + rw [acceptCoins_eq_configMatrix_pow_mulVec R hV hinit, configMatrix] + convert congrArg (· / (2 : R) ^ T) h using 1 + · rw [Finset.sum_div] + refine Finset.sum_congr rfl fun t ht => ?_ + have htT : t ≤ T := Nat.lt_succ_iff.mp (Finset.mem_range.mp ht) + rw [smul_pow, Matrix.smul_mulVec, Pi.smul_apply, smul_eq_mul, liveConfigMatrix] + have h2 : (2 : R) ^ T = 2 ^ (T - t) * 2 ^ t := by rw [← pow_add, Nat.sub_add_cancel htT] + rw [h2, inv_pow, mul_div_mul_left _ _ (pow_ne_zero _ two_ne_zero), div_eq_inv_mul] + +open scoped Classical in +/-- **The live matrix is nilpotent on reachable views**: if every view of `V` is reachable and +every branch halts within `T` steps, then `S ^ (T + 1) = 0`. -/ +theorem liveConfigMatrix_pow_eq_zero (R : Type*) [CommSemiring R] {input : List Bool} {T : ℕ} + (ht : machine.toNTM.RunsInTime input T) {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hreach : ∀ finite ∈ V, + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) : + machine.liveConfigMatrix R V ^ (T + 1) = 0 := by + classical + refine Matrix.liveCoinStepMatrix_pow_eq_zero hV fun x hx w => ⟨Fin.last T, ?_⟩ + obtain ⟨coins, hcoins⟩ := reflTransGen_viewStep_toNTM_iff.mp (hreach x hx) + have h := viewRep_foldl_viewCoinStep (machine := machine) + (MultiTapeNTM.viewRep_init (ntm := machine.toNTM) input) (coins ++ (List.ofFn w).take T) + have hhalt := halted_stepCoins machine ht (coins := coins ++ (List.ofFn w).take T) + (by simp) + rw [List.foldl_append, hcoins] at h + simpa using h.state.trans hhalt + +open scoped Classical in +/-- **The acceptance probability is an entry of `(1 - S / 2)⁻¹ *ᵥ e`**: if every view of `V` is +reachable and every branch halts within `T` steps, then `acceptCoins input T / 2 ^ T` is the +entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e`, with `S` the live configuration matrix. -/ +theorem acceptCoins_div_eq_inv_mulVec (R : Type*) [Field R] [CharZero R] {input : List Bool} + {T : ℕ} (ht : machine.toNTM.RunsInTime input T) {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hreach : ∀ finite ∈ V, + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) + (hinit : machine.toNTM.initView input ∈ V) : + (machine.acceptCoins input T : R) / 2 ^ T = + ((1 - (2 : R)⁻¹ • machine.liveConfigMatrix R V)⁻¹ *ᵥ FiniteCfg.acceptVec R V) + ⟨_, hinit⟩ := by + rw [Matrix.inv_one_sub_eq_sum_pow (n := T + 1) (by + rw [smul_pow, liveConfigMatrix_pow_eq_zero R ht hV hreach, smul_zero]), + Matrix.sum_mulVec, Finset.sum_apply, acceptCoins_div_eq_sum_liveConfigMatrix R hV hinit] + +/-- **The reachable views form a small closed set**: under a space bound `s`, the views reachable +from the initial view form a finite set, closed under coin steps, with at most +`2 ^ (2 * coreLengthBound k State n s + 1)` elements. -/ +theorem exists_finset_reachable [Finite State] {input : List Bool} {s : ℕ} + (hs : machine.toNTM.RunsInSpace input s) : + ∃ V : Finset (FiniteCfg k Bool State), + (∀ finite, finite ∈ V ↔ + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) ∧ + (∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) ∧ + V.card ≤ 2 ^ (2 * MultiTapeNTM.coreLengthBound k State input.length s + 1) := by + set reach := {finite | Relation.ReflTransGen machine.toNTM.ViewStep + (machine.toNTM.initView input) finite} + have hfin : reach.Finite := by + by_contra hinf + obtain ⟨V, hsub, hcard⟩ := Set.Infinite.exists_subset_card_eq hinf + (2 ^ (2 * MultiTapeNTM.coreLengthBound k State input.length s + 1) + 1) + have := MultiTapeNTM.length_le_of_nodup_reachable hs V.nodup_toList + fun finite hf => hsub (Finset.mem_toList.mp hf) + rw [Finset.length_toList, hcard] at this + omega + refine ⟨hfin.toFinset, fun finite => hfin.mem_toFinset, fun finite hf bit => ?_, ?_⟩ + · rw [hfin.mem_toFinset] at hf ⊢ + exact Relation.ReflTransGen.tail hf (viewStep_toNTM_iff.mpr ⟨bit, rfl⟩) + · rw [← Finset.length_toList] + exact MultiTapeNTM.length_le_of_nodup_reachable hs (Finset.nodup_toList _) + fun finite hf => hfin.mem_toFinset.mp (Finset.mem_toList.mp hf) + +end MultiTapePTM + +end Turing + +namespace Cslib.Complexity + +open _root_.Turing Matrix + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} + +open scoped Classical in +/-- **`BPL` through polynomial-size configuration matrices**: a `BPL` machine has, on every +encoded instance of length `n`, a closed set `V` of at most `2 * (2 * (n + 1)) ^ d` views, +containing the initial view, such that the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is +at least `2/3` on members and at most `1/3` on non-members, with `S` the live configuration +matrix on `V` and `e` the indicator of the accepting halted views. -/ +theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : MultiTapePTM k Bool State) (d : ℕ), + ∀ a, ∃ (V : Finset (FiniteCfg k Bool State)) (hinit : M.toNTM.initView (enc a) ∈ V), + V.card ≤ 2 * (2 * ((enc a).length + 1)) ^ d ∧ + (∀ finite ∈ V, ∀ bit, M.viewCoinStep finite bit ∈ V) ∧ + (a ∈ A → 2 / 3 ≤ ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩) ∧ + (a ∉ A → ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ ≤ 1 / 3) := by + obtain ⟨k, State, hfin, M, c, hM⟩ := h + refine ⟨k, State, hfin, M, 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1), + fun a => ?_⟩ + obtain ⟨hs, t, ht, hmem, hnot⟩ := hM a + obtain ⟨V, hreach, hV, hcard⟩ := M.exists_finset_reachable hs + have hinit : M.toNTM.initView (enc a) ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, hcard.trans (MultiTapeNTM.two_pow_coreLengthBound_log_le k State c _), hV, + fun ha => ?_, fun ha => ?_⟩ + all_goals + rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV (fun finite hf => (hreach _).mp hf)] + · have h : ((2 * 2 ^ t : ℕ) : ℚ) ≤ ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) := + Nat.cast_le.mpr (hmem ha) + push_cast at h + rw [le_div_iff₀ (by positivity)] + linarith + · have h : ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) ≤ ((2 ^ t : ℕ) : ℚ) := + Nat.cast_le.mpr (hnot ha) + push_cast at h + rw [div_le_iff₀ (by positivity)] + linarith + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean index 192d76894..c3d7bdd0a 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Space public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding public import Complexity.Foundations.Data.BitString.Enumeration import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength +import Complexity.Foundations.Data.Nat.Log import Mathlib.Data.Nat.Size import Mathlib.Tactic.Linarith @@ -39,6 +40,8 @@ views are reachable (`Turing.MultiTapeNTM.length_le_of_nodup_reachable`), polyno * `Turing.MultiTapeNTM.coreCode_injective`: the code identifies views with the same input. * `Turing.MultiTapeNTM.length_coreCode_le`: reachable views have short codes. * `Turing.MultiTapeNTM.length_le_of_nodup_reachable`: few distinct views are reachable. +* `Turing.MultiTapeNTM.two_pow_coreLengthBound_log_le`: under a logarithmic space bound, + polynomially many. ## References @@ -145,4 +148,25 @@ theorem length_le_of_nodup_reachable (hs : ntm.RunsInSpace input s) (Cslib.BitString.length_padWord (length_coreCode_le hs (hreach finite hf))) simpa using hcodes.length_le_of_subset hsub +omit [Finite State] in +/-- **Logarithmic space has polynomially many views**: under the space bound `c * (log₂ n + 1)`, +the bound `2 ^ (2 * coreLengthBound k State n s + 1)` of +`Turing.MultiTapeNTM.length_le_of_nodup_reachable` is at most `2 * (2 * (n + 1)) ^ d`, with an +exponent `d` depending only on `k`, `State` and `c`. -/ +theorem two_pow_coreLengthBound_log_le (k : ℕ) (State : Type) (c n : ℕ) : + 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) ≤ + 2 * (2 * (n + 1)) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := by + set K := 8 + 2 * Nat.card (Option State) + 200 * k + have hcore : + coreLengthBound k State n (c * (Nat.log2 n + 1)) = K * (c + 1) * (Nat.log2 n + 1) := by + simp only [coreLengthBound, K] + ring + calc 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) + = 2 * (2 ^ (Nat.log2 n + 1)) ^ (2 * K * (c + 1)) := by + rw [hcore, ← pow_mul, pow_succ] + ring_nf + _ ≤ 2 * (2 * (n + 1)) ^ (2 * K * (c + 1)) := by + gcongr + exact Nat.two_pow_log2_succ_le n + end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean index 119aebd75..f7efea936 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean @@ -196,29 +196,6 @@ theorem runsInTime_of_runsInSpace {s t : ℕ} (hs : ntm.RunsInSpace input s) have hstate := (hrep i (by omega)).state exact hrun ⟨i, by omega⟩ (hstate.symm.trans (hqrep.state.trans hhalt)) -/-- The polynomial clock of `exists_runsInTime_polynomial_of_runsInSpace_log`, with its exponent -spelled out. -/ -private theorem runsInTime_polynomial_of_runsInSpace_log {c t : ℕ} - (hs : ntm.RunsInSpace input (c * (Nat.log2 input.length + 1))) - (ht : ntm.RunsInTime input t) : - ntm.RunsInTime input (2 * (2 * (input.length + 1)) ^ - (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1))) := by - refine (runsInTime_of_runsInSpace hs ht).mono ?_ - set K := 8 + 2 * Nat.card (Option State) + 200 * k - set L := Nat.log2 input.length - have hlog : 2 ^ L ≤ input.length + 1 := by - rcases Nat.eq_zero_or_pos input.length with h | h - · simp [L, h] - · rw [show L = Nat.log 2 input.length from Nat.log2_eq_log_two] - exact (Nat.pow_log_le_self 2 h.ne').trans (Nat.le_succ _) - have hcore : coreLengthBound k State input.length (c * (L + 1)) = K * (c + 1) * (L + 1) := by - simp only [coreLengthBound, K, L] - ring - have hbase : 2 ^ (L + 1) ≤ 2 * (input.length + 1) := by rw [pow_succ]; omega - calc 2 ^ (2 * coreLengthBound k State input.length (c * (L + 1)) + 1) - = 2 * (2 ^ (L + 1)) ^ (2 * K * (c + 1)) := by rw [hcore, ← pow_mul, pow_succ]; ring_nf - _ ≤ 2 * (2 * (input.length + 1)) ^ (2 * K * (c + 1)) := by gcongr - /-- **Logarithmic space gives a polynomial clock.** For every space constant `c` there is an exponent `d` such that on every input of length `n`, if every computation path stays within space `c * (log₂ n + 1)` and every computation path halts within some time, then every computation path @@ -227,6 +204,7 @@ theorem exists_runsInTime_polynomial_of_runsInSpace_log (ntm : MultiTapeNTM k Bo (c : ℕ) : ∃ d, ∀ {input : List Bool} {t : ℕ}, ntm.RunsInSpace input (c * (Nat.log2 input.length + 1)) → ntm.RunsInTime input t → ntm.RunsInTime input (2 * (2 * (input.length + 1)) ^ d) := - ⟨_, fun hs ht => runsInTime_polynomial_of_runsInSpace_log hs ht⟩ + ⟨_, fun hs ht => + (runsInTime_of_runsInSpace hs ht).mono (two_pow_coreLengthBound_log_le k State c _)⟩ end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 94e33e71e..c0b46a674 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -216,20 +216,8 @@ polynomial in the input length. -/ private theorem rounds_le (k : ℕ) (State : Type) (c n : ℕ) : 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) ≤ 2 * 2 ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) * - (n + 1) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := by - set M := 8 + 2 * Nat.card (Option State) + 200 * k - set D := 2 * M * (c + 1) - have hexp : 2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1 ≤ - (Nat.log2 n + 1) * D + 1 := by - simp only [coreLengthBound, D] - rw [← show M = 8 + 2 * Nat.card (Option State) + 200 * k from rfl] - nlinarith - calc 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) - ≤ 2 ^ ((Nat.log2 n + 1) * D + 1) := Nat.pow_le_pow_right (by norm_num) hexp - _ = 2 * (2 ^ (Nat.log2 n + 1)) ^ D := by rw [pow_succ, pow_mul, mul_comm] - _ ≤ 2 * (2 * (n + 1)) ^ D := - Nat.mul_le_mul_left 2 (Nat.pow_le_pow_left (Nat.two_pow_log2_succ_le n) D) - _ = 2 * 2 ^ D * (n + 1) ^ D := by rw [mul_pow, mul_assoc] + (n + 1) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := + (two_pow_coreLengthBound_log_le k State c n).trans_eq (by rw [mul_pow, ← mul_assoc]) open scoped Classical in /-- **Acceptance within logarithmic space is decided by breadth-first search in polynomial time.** diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean new file mode 100644 index 000000000..86b891820 --- /dev/null +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.Matrix.Mul +public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse +public import Mathlib.Data.Fintype.Pi +import Mathlib.Algebra.Ring.GeomSum +import Mathlib.Data.Fin.Tuple.Basic + +/-! +# Transition matrices of coin-driven maps + +A map `next : α → Bool → α` moves a state to one of two successors, selected by a coin. On a finite +set `s` of states closed under `next`, its *count matrix* `Matrix.coinStepMatrix next s` has as +entry `(x, y)` the number of coins that move `x` to `y`. Its powers count coin strings +(`Matrix.coinStepMatrix_pow_mulVec`): `(N ^ t *ᵥ f) x` is the sum of `f` over the endpoints of +the `2 ^ t` coin strings of length `t` replayed from `x`. Halving the entries gives the stochastic +matrix of the fair-coin random walk. + +Keeping only the rows of the *live* states gives `Matrix.liveCoinStepMatrix live next s`, which +counts coin strings along which every state before the last is live +(`Matrix.liveCoinStepMatrix_pow_mulVec`). When the other states are fixed by `next`, the walk +stops at the first state that is not live, and every coin string is counted by the time it stops +(`Matrix.coinStepMatrix_pow_mulVec_eq_sum`). When the live walks have bounded length, the live +matrix is nilpotent, and `1 - S` has the inverse `∑ i < n, S ^ i` +(`Matrix.inv_one_sub_eq_sum_pow`). + +## Main definitions + +* `Matrix.coinStepMatrix`: the count matrix of a coin-driven map on a finite set. +* `Matrix.liveCoinStepMatrix`: its rows at live states, zero rows elsewhere. + +## Main results + +* `Matrix.coinStepMatrix_pow_mulVec`: powers sum over coin strings. +* `Matrix.liveCoinStepMatrix_pow_mulVec`: powers of the live matrix sum over live coin strings. +* `Matrix.coinStepMatrix_pow_mulVec_eq_sum`: first-stop decomposition of the count matrix. +* `Matrix.liveCoinStepMatrix_pow_eq_zero`: bounded live walks make the live matrix nilpotent. +* `Matrix.inv_one_sub_eq_sum_pow`: the inverse of `1 - S` for nilpotent `S`. +-/ + +@[expose] public section + +namespace Matrix + +variable {α R : Type*} [DecidableEq α] + +section Semiring + +variable [CommSemiring R] (next : α → Bool → α) (s : Finset α) + +/-- **The count matrix of a coin-driven map** on a finite set `s`: the entry at `(x, y)` is the +number of coins `b` with `next x b = y`. -/ +def coinStepMatrix : Matrix s s R := + fun x y => ∑ b : Bool, if next x b = y then 1 else 0 + +variable (live : α → Prop) [DecidablePred live] + +/-- **The live count matrix**: the rows of `Matrix.coinStepMatrix` at states satisfying `live`, +and zero rows at the other states. -/ +def liveCoinStepMatrix : Matrix s s R := + fun x y => if live x then coinStepMatrix next s x y else 0 + +variable {next s live} + +/-- A row of the count matrix, applied to a vector, sums the two coin successors. -/ +theorem coinStepMatrix_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (g : s → R) (x : s) : + (coinStepMatrix next s *ᵥ g) x = ∑ b : Bool, g ⟨next x b, hs x x.2 b⟩ := by + simp only [mulVec, dotProduct, coinStepMatrix, Finset.sum_mul, ite_mul, one_mul, zero_mul] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun b _ => ?_ + rw [Finset.sum_eq_single ⟨next x b, hs x x.2 b⟩] + · simp + · intro y _ hy + simp only [show ¬ next x b = y from fun h => hy (Subtype.ext h.symm), ↓reduceIte] + · simp + +/-- A row of the live count matrix sums the two coin successors at a live state and vanishes +elsewhere. -/ +theorem liveCoinStepMatrix_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (g : s → R) (x : s) : + (liveCoinStepMatrix next s live *ᵥ g) x = + if live x then ∑ b : Bool, g ⟨next x b, hs x x.2 b⟩ else 0 := by + rw [← coinStepMatrix_mulVec hs] + simp only [mulVec, dotProduct, liveCoinStepMatrix] + split_ifs <;> simp + +/-- Sums over the coin strings of length `t + 1` split off the first coin. -/ +private theorem sum_fin_succ_bool {M : Type*} [AddCommMonoid M] (t : ℕ) + (g : (Fin (t + 1) → Bool) → M) : + ∑ w : Fin (t + 1) → Bool, g w = ∑ b : Bool, ∑ w : Fin t → Bool, g (Fin.cons b w) := by + rw [← Fintype.sum_prod_type', ← (Fin.consEquiv fun _ => Bool).sum_comp] + rfl + +/-- **Powers of the count matrix sum over coin strings**: `(N ^ t *ᵥ f) x` is the sum of `f` over +the states reached from `x` by the `2 ^ t` coin strings of length `t`. -/ +theorem coinStepMatrix_pow_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (f : α → R) (t : ℕ) + (x : s) : (coinStepMatrix next s ^ t *ᵥ fun y : s => f y) x = + ∑ w : Fin t → Bool, f ((List.ofFn w).foldl next x) := by + induction t generalizing f x with + | zero => simp + | succ t ih => + have hfun : (coinStepMatrix next s ^ t *ᵥ fun y : s => f y) = + fun y : s => ∑ w : Fin t → Bool, f ((List.ofFn w).foldl next y) := funext fun y => ih f y + rw [pow_succ', ← mulVec_mulVec, hfun, coinStepMatrix_mulVec hs, sum_fin_succ_bool] + simp [List.ofFn_succ] + +/-- **Powers of the live count matrix sum over live coin strings**: `(S ^ t *ᵥ f) x` is the sum +of `f` over the states reached from `x` by those coin strings of length `t` along which every +state before the last is live. -/ +theorem liveCoinStepMatrix_pow_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (f : α → R) (t : ℕ) + (x : s) : (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) x = + ∑ w : Fin t → Bool, if ∀ i : Fin t, live (((List.ofFn w).take i).foldl next x) then + f ((List.ofFn w).foldl next x) else 0 := by + classical + induction t generalizing f x with + | zero => simp + | succ t ih => + have hfun : (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) = + fun y : s => ∑ w : Fin t → Bool, if ∀ i : Fin t, + live (((List.ofFn w).take i).foldl next y) then f ((List.ofFn w).foldl next y) else 0 := + funext fun y => ih f y + rw [pow_succ', ← mulVec_mulVec, hfun, liveCoinStepMatrix_mulVec hs, sum_fin_succ_bool] + have hlive (b : Bool) (w : Fin t → Bool) : + (∀ i : Fin (t + 1), live (((List.ofFn (Fin.cons b w : Fin (t + 1) → Bool)).take i).foldl + next x)) ↔ live x ∧ ∀ i : Fin t, live (((List.ofFn w).take i).foldl next (next x b)) := by + rw [Fin.forall_fin_succ] + simp [List.ofFn_succ] + split_ifs with hx + · refine Finset.sum_congr rfl fun b _ => Finset.sum_congr rfl fun w _ => ?_ + simp only [hlive, hx, true_and] + simp [List.ofFn_succ] + · refine (Finset.sum_eq_zero fun b _ => Finset.sum_eq_zero fun w _ => ?_).symm + rw [ite_eq_right_iff, hlive] + exact fun h => absurd h.1 hx + +/-- **First-stop decomposition.** If the states that are not live are fixed by `next`, and `f` +vanishes at live states, then counting the coin strings of length `T` by `f` at their endpoint +is the same as counting, for each `t ≤ T`, the live coin strings of length `t` by `f`, each +weighted by the `2 ^ (T - t)` continuations after the walk has stopped. -/ +theorem coinStepMatrix_pow_mulVec_eq_sum (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) + (hfix : ∀ x, ¬ live x → ∀ b, next x b = x) {f : α → R} (hf : ∀ x, live x → f x = 0) + (T : ℕ) (x : s) : (coinStepMatrix next s ^ T *ᵥ fun y : s => f y) x = + ∑ t ∈ Finset.range (T + 1), + 2 ^ (T - t) * (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) x := by + induction T generalizing x with + | zero => simp + | succ T ih => + rw [pow_succ', ← mulVec_mulVec, coinStepMatrix_mulVec hs] + by_cases hx : live x + · rw [Finset.sum_range_succ', pow_zero, one_mulVec] + simp only [hf x hx, mul_zero, add_zero] + have hrow (t : ℕ) : (liveCoinStepMatrix next s live ^ (t + 1) *ᵥ fun y : s => f y) x = + ∑ b : Bool, (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) + ⟨next x b, hs x x.2 b⟩ := by + rw [pow_succ', ← mulVec_mulVec, liveCoinStepMatrix_mulVec hs] + simp only [hx, ↓reduceIte] + simp only [hrow, Finset.mul_sum, Nat.add_sub_add_right] + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun b _ => ih ⟨next x b, hs x x.2 b⟩ + · have hnext (b : Bool) : (⟨next x b, hs x x.2 b⟩ : s) = x := Subtype.ext (hfix x hx b) + have hzero (t : ℕ) : + (liveCoinStepMatrix next s live ^ (t + 1) *ᵥ fun y : s => f y) x = 0 := by + rw [pow_succ', ← mulVec_mulVec, liveCoinStepMatrix_mulVec hs] + simp only [hx, ↓reduceIte] + simp only [hnext] + rw [Fintype.sum_bool, ih x, Finset.sum_range_succ', Finset.sum_range_succ'] + simp only [hzero, mul_zero, Finset.sum_const_zero, zero_add, pow_zero, one_mulVec, + Nat.sub_zero] + ring + +/-- **Bounded live walks make the live matrix nilpotent**: if along every coin string of length +`n` from a state of `s` some state before the last is not live, then `S ^ n = 0`. -/ +theorem liveCoinStepMatrix_pow_eq_zero (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) {n : ℕ} + (h : ∀ x ∈ s, ∀ w : Fin n → Bool, ∃ i : Fin n, + ¬ live (((List.ofFn w).take i).foldl next x)) : + (liveCoinStepMatrix next s live : Matrix s s R) ^ n = 0 := by + ext x y + have hcol := liveCoinStepMatrix_pow_mulVec (R := R) (live := live) hs + (fun z => if z = y then 1 else 0) n x + have hvec : (fun z : s => if (z : α) = y then (1 : R) else 0) = Pi.single y 1 := by + funext z + simp only [Pi.single_apply, Subtype.ext_iff] + rw [hvec, mulVec_single_one, Finset.sum_eq_zero fun w _ => ?_] at hcol + · simpa using hcol + · obtain ⟨i, hi⟩ := h x x.2 w + exact ite_eq_right_iff.mpr fun hall => absurd (hall i) hi + +end Semiring + +/-- **Inverse of `1 - S` for nilpotent `S`**: if `S ^ n = 0`, then `1 - S` is invertible with +inverse the truncated geometric series `∑ i < n, S ^ i`. -/ +theorem inv_one_sub_eq_sum_pow {ι : Type*} [Fintype ι] [DecidableEq ι] [CommRing R] + {S : Matrix ι ι R} {n : ℕ} (h : S ^ n = 0) : + (1 - S)⁻¹ = ∑ i ∈ Finset.range n, S ^ i := + inv_eq_right_inv (by rw [mul_neg_geom_sum, h, sub_zero]) + +end Matrix diff --git a/ComplexityTests/CoinStepMatrix.lean b/ComplexityTests/CoinStepMatrix.lean new file mode 100644 index 000000000..dda73a8f9 --- /dev/null +++ b/ComplexityTests/CoinStepMatrix.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep + +/-! +# Tests for transition matrices of coin-driven maps +-/ + +namespace ComplexityTests.CoinStepMatrix + +open Matrix + +/-- From `0` the coin moves to `1` or `2`; the states `1` and `2` are fixed. -/ +private def next : Fin 3 → Bool → Fin 3 + | 0, b => if b then 1 else 2 + | x, _ => x + +private theorem next_mem (x : Fin 3) (_ : x ∈ (Finset.univ : Finset (Fin 3))) (b : Bool) : + next x b ∈ (Finset.univ : Finset (Fin 3)) := + Finset.mem_univ _ + +-- Half of the `8` coin strings of length three end in `1` from `0`: those starting with `true`. +example : (coinStepMatrix next Finset.univ ^ 3 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 4 := by + rw [coinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +/-- Only the state `0` is live, so the live matrix squares to zero. -/ +private theorem live_sq : (liveCoinStepMatrix next Finset.univ (· = 0) : Matrix _ _ ℚ) ^ 2 = 0 := + liveCoinStepMatrix_pow_eq_zero next_mem fun x _ w => by + refine ⟨1, ?_⟩ + fin_cases x <;> cases h : w 0 <;> simp [next, List.ofFn_succ, h] + +-- The walk from `0` stops after one step: one live coin string of length one ends in `1`, none +-- of length two, since the live condition fails at the second state. +example : (liveCoinStepMatrix next Finset.univ (· = 0) ^ 1 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 1 := by + rw [liveCoinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +example : (liveCoinStepMatrix next Finset.univ (· = 0) ^ 2 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 0 := by + rw [liveCoinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +-- With `S ^ 2 = 0`, the inverse of `1 - S` is `1 + S`. +example : (1 - (liveCoinStepMatrix next Finset.univ (· = 0) : Matrix _ _ ℚ))⁻¹ = + 1 + liveCoinStepMatrix next Finset.univ (· = 0) := by + rw [inv_one_sub_eq_sum_pow live_sq, Finset.sum_range_succ, Finset.sum_range_one, pow_zero, + pow_one] + +end ComplexityTests.CoinStepMatrix diff --git a/ComplexityTests/RandomizedLogSpace.lean b/ComplexityTests/RandomizedLogSpace.lean index e5684761a..c6b30b8a5 100644 --- a/ComplexityTests/RandomizedLogSpace.lean +++ b/ComplexityTests/RandomizedLogSpace.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Christian Reitwiessner -/ import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix import Complexity.Computability.Complexity.Classes.LogSpace.USTCON /-! @@ -151,4 +152,51 @@ example (enc : ℕ ↪ List Bool) : ∃ (k : ℕ) (State : Type) (_ : Finite Sta end Amplification +section ConfigurationMatrix + +open Cslib Turing Matrix + +open scoped Classical in +-- On the reachable views of `coinFlip`, the configuration matrix counts the one accepting coin +-- string of length one, and its stochastic power gives probability `1/2` at every later clock. +example (input : List Bool) : ∃ (V : Finset (FiniteCfg 0 Bool Unit)) + (hinit : coinFlip.toNTM.initView input ∈ V), + (coinFlip.configMatrix ℕ V ^ 1 *ᵥ FiniteCfg.acceptVec ℕ V) ⟨_, hinit⟩ = 1 ∧ + (((2 : ℚ)⁻¹ • coinFlip.configMatrix ℚ V) ^ 5 *ᵥ FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ = + 1 / 2 := by + obtain ⟨V, hreach, hV, -⟩ := + coinFlip.exists_finset_reachable (MultiTapeNTM.runsInSpace_zero_tapes _ input 0) + have hinit : coinFlip.toNTM.initView input ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, ?_, ?_⟩ + · rw [← MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec ℕ hV hinit, Nat.cast_id, + acceptCoins_coinFlip] + · have h5 := MultiTapePTM.acceptCoins_add coinFlip (runsInTime_coinFlip input) 4 + rw [← MultiTapePTM.acceptCoins_div_eq_configMatrix_pow_mulVec ℚ hV hinit, + show 5 = 1 + 4 from rfl, h5, acceptCoins_coinFlip] + norm_num + +open scoped Classical in +-- The same probability `1/2` as the entry of `(1 - S / 2)⁻¹ *ᵥ e`, and as the sum of the +-- substochastic powers up to the halting time `1`. +example (input : List Bool) : ∃ (V : Finset (FiniteCfg 0 Bool Unit)) + (hinit : coinFlip.toNTM.initView input ∈ V), + ((1 - (2 : ℚ)⁻¹ • coinFlip.liveConfigMatrix ℚ V)⁻¹ *ᵥ FiniteCfg.acceptVec ℚ V) + ⟨_, hinit⟩ = 1 / 2 ∧ + ∑ t ∈ Finset.range 2, (((2 : ℚ)⁻¹ • coinFlip.liveConfigMatrix ℚ V) ^ t *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ = 1 / 2 ∧ + coinFlip.liveConfigMatrix ℚ V ^ 2 = 0 := by + obtain ⟨V, hreach, hV, -⟩ := + coinFlip.exists_finset_reachable (MultiTapeNTM.runsInSpace_zero_tapes _ input 0) + have hinit : coinFlip.toNTM.initView input ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, ?_, ?_, ?_⟩ + · rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ (runsInTime_coinFlip input) hV + (fun finite hf => (hreach _).mp hf), acceptCoins_coinFlip] + norm_num + · rw [← MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix ℚ hV hinit 1, acceptCoins_coinFlip] + norm_num + · exact MultiTapePTM.liveConfigMatrix_pow_eq_zero ℚ (runsInTime_coinFlip input) hV + fun finite hf => (hreach _).mp hf + +end ConfigurationMatrix + end ComplexityTests.RandomizedLogSpace diff --git a/references.bib b/references.bib index ffd09ecfe..5e9ecd5ea 100644 --- a/references.bib +++ b/references.bib @@ -729,6 +729,18 @@ @article{BorchertHemaspaandraRothe2000 url = {https://arxiv.org/abs/cs/9907041} } +@article{BorodinCookPippenger1983, + author = {Borodin, Allan and Cook, Stephen and Pippenger, Nicholas}, + title = {Parallel Computation for Well-Endowed Rings and Space-Bounded Probabilistic + Machines}, + journal = {Information and Control}, + volume = {58}, + number = {1--3}, + pages = {113--136}, + year = {1983}, + doi = {10.1016/S0019-9958(83)80060-6} +} + @book{BorweinErdelyi1995, author = {Borwein, Peter and Erd{\'e}lyi, Tam{\'a}s}, title = {Polynomials and Polynomial Inequalities}, @@ -2234,6 +2246,15 @@ @book{ Hopcroft2006 address = {USA} } +@techreport{Hoza2022, + author = {Hoza, William M.}, + title = {Recent Progress on Derandomizing Space-Bounded Computation}, + institution = {Electronic Colloquium on Computational Complexity}, + number = {TR22-121}, + year = {2022}, + url = {https://eccc.weizmann.ac.il/report/2022/121/} +} + @article{Huang2019, author = {Huang, Hao}, title = {Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture}, From 3fd12172dcb5d7826ad87f5516e6c3f3ad765bd4 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:43:22 +0000 Subject: [PATCH 2/2] fix(LogSpace): Hoza citation scope; export reachability and nilpotency for BPL MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Hoza Section 4.3 states BPSPACE(S) ⊆ DSPACE(S^2); the inverse picture is Section 3.2, and BPL ⊆ P is no longer attributed to it. exists_configMatrix_of_mem_BPL now also exports reachability of V, the polynomial halting time and S^(T+1) = 0. Co-Authored-By: Claude Opus 5.5 --- .../Randomized/ConfigurationMatrix.lean | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean index 7f786876f..a81a7f8a1 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean @@ -39,10 +39,11 @@ The reachable views form such a set (`Turing.MultiTapePTM.exists_finset_reachabl under a logarithmic one. So a `BPL` language is decided by the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` for a polynomial-size matrix `S` (`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). This is the Markov chain of a probabilistic -machine on its configurations [Gill][Gill1977], whose powers and inverse Borodin, Cook and -Pippenger compute in parallel to place probabilistic space `s` in `DSPACE(s²)` -[Borodin, Cook and Pippenger][BorodinCookPippenger1983]; for `BPL` this gives -`BPL ⊆ DSPACE(log² n)` and `BPL ⊆ P` [Hoza, Section 4.3][Hoza2022]. Those algorithms are not +machine on its configurations [Gill][Gill1977]. Borodin, Cook and Pippenger compute its powers +and inverse in parallel [Borodin, Cook and Pippenger][BorodinCookPippenger1983], which gives +`BPSPACE(S) ⊆ DSPACE(S²)` [Hoza, Section 4.3][Hoza2022]; the inverse of `1 - W` as the sum +`W⁰ + W¹ + …` of transition-matrix powers is the picture of [Hoza, Section 3.2][Hoza2022]. +Exact evaluation of the polynomial-size matrix also gives `BPL ⊆ P`. None of these algorithms is formalized here. The matrices are indexed by an arbitrary closed set of views rather than a set of @@ -342,15 +343,21 @@ variable {α : Type} {enc : α ↪ List Bool} {A : Set α} open scoped Classical in /-- **`BPL` through polynomial-size configuration matrices**: a `BPL` machine has, on every -encoded instance of length `n`, a closed set `V` of at most `2 * (2 * (n + 1)) ^ d` views, -containing the initial view, such that the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is -at least `2/3` on members and at most `1/3` on non-members, with `S` the live configuration -matrix on `V` and `e` the indicator of the accepting halted views. -/ +encoded instance of length `n`, a set `V` of at most `2 * (2 * (n + 1)) ^ d` views, all reachable +from the initial view and closed under coin steps, such that every branch halts within +`T = 2 * (2 * (n + 1)) ^ d` steps, the live configuration matrix `S` on `V` satisfies +`S ^ (T + 1) = 0`, and the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is at least `2/3` on +members and at most `1/3` on non-members, with `e` the indicator of the accepting halted +views. -/ theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : MultiTapePTM k Bool State) (d : ℕ), ∀ a, ∃ (V : Finset (FiniteCfg k Bool State)) (hinit : M.toNTM.initView (enc a) ∈ V), V.card ≤ 2 * (2 * ((enc a).length + 1)) ^ d ∧ (∀ finite ∈ V, ∀ bit, M.viewCoinStep finite bit ∈ V) ∧ + (∀ finite ∈ V, + Relation.ReflTransGen M.toNTM.ViewStep (M.toNTM.initView (enc a)) finite) ∧ + M.toNTM.RunsInTime (enc a) (2 * (2 * ((enc a).length + 1)) ^ d) ∧ + M.liveConfigMatrix ℚ V ^ (2 * (2 * ((enc a).length + 1)) ^ d + 1) = 0 ∧ (a ∈ A → 2 / 3 ≤ ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩) ∧ (a ∉ A → ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ @@ -361,10 +368,14 @@ theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : obtain ⟨hs, t, ht, hmem, hnot⟩ := hM a obtain ⟨V, hreach, hV, hcard⟩ := M.exists_finset_reachable hs have hinit : M.toNTM.initView (enc a) ∈ V := (hreach _).mpr .refl - refine ⟨V, hinit, hcard.trans (MultiTapeNTM.two_pow_coreLengthBound_log_le k State c _), hV, - fun ha => ?_, fun ha => ?_⟩ - all_goals - rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV (fun finite hf => (hreach _).mp hf)] + have hpoly := MultiTapeNTM.two_pow_coreLengthBound_log_le k State c (enc a).length + have hreach' : ∀ finite ∈ V, + Relation.ReflTransGen M.toNTM.ViewStep (M.toNTM.initView (enc a)) finite := + fun finite hf => (hreach _).mp hf + have hT := (MultiTapeNTM.runsInTime_of_runsInSpace hs ht).mono hpoly + refine ⟨V, hinit, hcard.trans hpoly, hV, hreach', hT, + MultiTapePTM.liveConfigMatrix_pow_eq_zero ℚ hT hV hreach', fun ha => ?_, fun ha => ?_⟩ + all_goals rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV hreach'] · have h : ((2 * 2 ^ t : ℕ) : ℚ) ≤ ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) := Nat.cast_le.mpr (hmem ha) push_cast at h