From cdd8f312bcddc149c6cf2a500aac843be1ad2f69 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:39:53 -0400 Subject: [PATCH 01/10] feat(Classes/PP): unbounded-error probabilistic time PPTIME Define Turing.MultiTapePTM.DecidesByMajorityInTime and Cslib.Complexity.PPTIME, the strict-majority counterpart of BPTIME on the same fair-coin machines, and prove PPTIME_mono, BPTIME_subset_PPTIME, the count form decidesByMajorityInTime_iff, and mem_PP_iff_exists_mem_PPTIME, the machine characterisation of the verifier-based PP. Statement groundwork for #1833. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Computability/Complexity/Classes/PP.lean | 4 +- .../Complexity/Classes/PP/Time.lean | 221 ++++++++++++++++++ .../Complexity/Classes/Time.lean | 3 + ComplexityTests/PPTime.lean | 72 ++++++ 5 files changed, 300 insertions(+), 1 deletion(-) create mode 100644 Complexity/Computability/Complexity/Classes/PP/Time.lean create mode 100644 ComplexityTests/PPTime.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28b..0ef68184ef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1121,6 +1121,7 @@ public import Complexity.Computability.Complexity.Classes.PP.Bit public import Complexity.Computability.Complexity.Classes.PP.Characterization public import Complexity.Computability.Complexity.Classes.PP.Closure public import Complexity.Computability.Complexity.Classes.PP.Oracle +public import Complexity.Computability.Complexity.Classes.PP.Time public import Complexity.Computability.Complexity.Classes.PP.TruthTable public import Complexity.Computability.Complexity.Classes.Padding public import Complexity.Computability.Complexity.Classes.Padding.Polynomial diff --git a/Complexity/Computability/Complexity/Classes/PP.lean b/Complexity/Computability/Complexity/Classes/PP.lean index 37f7c119af..adc5b38ba6 100644 --- a/Complexity/Computability/Complexity/Classes/PP.lean +++ b/Complexity/Computability/Complexity/Classes/PP.lean @@ -27,7 +27,9 @@ verifier (`BPP_subset_PP`). Gill requires a strict majority on members, as here; the variant with a non-strict majority defines the same class (`Cslib.Complexity.mem_PP_iff_decidesByNonstrictMajority`). The -characterisation by probabilistic machines is not proved here. +characterisation by fair-coin machines deciding by strict majority within polynomial time is +`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`, in +`Complexity.Computability.Complexity.Classes.PP.Time`. ## Main definitions diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean new file mode 100644 index 0000000000..5775864e39 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -0,0 +1,221 @@ +/- +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.PP +public import Complexity.Computability.Complexity.Classes.Time +import Complexity.Computability.Complexity.Classes.SharpP.Probability +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput +import Complexity.Computability.Probabilistic.PPT.Capture +import Complexity.Computability.Probabilistic.PPT.Clock +import Complexity.Computability.Probabilistic.Sampling + +/-! +# Unbounded-error probabilistic time + +`Cslib.Complexity.PPTIME enc t` consists of the problems decided by strict majority within time +`O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, by a fair-coin machine with a +binary alphabet and finitely many states (`Turing.MultiTapePTM.DecidesByMajorityInTime`): every +run on that many coins has halted, and `a ∈ A` exactly when the run outputs `[true]` with +probability more than `1 / 2` [Gill][Gill1977]. It is the unbounded-error counterpart of +`Cslib.Complexity.BPTIME`, with the same machines and clocks. + +A fair-coin machine draws one coin per live step, so its acceptance probability within the clock +`t` is the number of accepting coin strings of length `t` divided by `2 ^ t`. Deciding by majority +is therefore the comparison `2 ^ t < 2 * count` of that count, an `Cslib.Complexity.acceptCount` +of the coin replay `Turing.MultiTapePTM.runClosedCoins` +(`Turing.MultiTapePTM.decidesByMajorityInTime_iff`). + +`PP` (`Cslib.Complexity.PP`) is defined through polynomial-time verifiers reading random strings. +It is the union of the classes `PPTIME (n ^ k)` (`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`), +by the argument for `BPP` and `BPTIME` (`Cslib.Complexity.mem_BPP_iff_exists_mem_BPTIME`): a +verifier run on sampled coins is a fair-coin machine with a halting polynomial clock, and a +fair-coin machine halting within `T` steps is a verifier replaying `T` coins. A bounded-error +decider decides by majority (`Cslib.Complexity.BPTIME_subset_PPTIME`). + +## Main definitions + +* `Turing.MultiTapePTM.DecidesByMajorityInTime`: strict majority within a clock. +* `Cslib.Complexity.PPTIME`: unbounded-error probabilistic time. + +## Main results + +* `Turing.MultiTapePTM.decidesByMajorityInTime_iff`: the majority condition as a count of + accepting coin strings. +* `Cslib.Complexity.PPTIME_mono`: `PPTIME` is monotone in the time bound. +* `Cslib.Complexity.BPTIME_subset_PPTIME`: bounded error is a strict majority. +* `Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`: `PP` is the union of the classes + `PPTIME (n ^ k)`. + +## References + +* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977] +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09] +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib +open scoped ENNReal + +variable {k : ℕ} {State : Type} {α : Type*} + +/-- `machine` decides `A` by strict majority within `t`, relative to the encoding `enc`: on every +encoded instance `enc a`, every run of `t a` steps with fair coins has halted, and `a ∈ A` exactly +when the run outputs `[true]` with probability more than `1 / 2` [Gill][Gill1977]. -/ +def DecidesByMajorityInTime (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) + (A : Set α) (t : α → ℕ) : Prop := + ∀ a, (∀ final ∈ (ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ A ↔ 1 / 2 < ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) + +/-- Time bounds can be increased: a halted run ignores further coins. -/ +theorem DecidesByMajorityInTime.mono {machine : MultiTapePTM k Bool State} + {enc : α ↪ List Bool} {A : Set α} {t t' : α → ℕ} + (h : machine.DecidesByMajorityInTime enc A t) (ht : ∀ a, t a ≤ t' a) : + machine.DecidesByMajorityInTime enc A t' := fun a => by + obtain ⟨hhalt, hmem⟩ := h a + refine ⟨?_, ?_⟩ + · rw [machine.eval_runClosedConfigFrom_eq_of_halted _ (ht a) hhalt] + exact hhalt + · rwa [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] + +/-- A probability `c / 2 ^ n` exceeds one half exactly when `2 ^ n < 2 * c`. -/ +private theorem half_lt_div_iff {c n : ℕ} : + (1 / 2 : ℝ≥0∞) < c / 2 ^ n ↔ 2 ^ n < 2 * c := by + have h2n : (2 : ℝ≥0∞) ^ n ≠ 0 := pow_ne_zero _ two_ne_zero + have h2n' : (2 : ℝ≥0∞) ^ n ≠ ⊤ := ENNReal.pow_ne_top ENNReal.ofNat_ne_top + rw [ENNReal.lt_div_iff_mul_lt (Or.inl h2n) (Or.inl h2n'), one_div, mul_comm, + ← div_eq_mul_inv, ENNReal.div_lt_iff (Or.inl two_ne_zero) (Or.inl ENNReal.ofNat_ne_top), + show ((c : ℝ≥0∞) * 2) = ((2 * c : ℕ) : ℝ≥0∞) by push_cast; ring, + show ((2 : ℝ≥0∞) ^ n) = ((2 ^ n : ℕ) : ℝ≥0∞) by push_cast; rfl] + exact Nat.cast_lt + +/-- **Deciding by majority is a count comparison.** A fair-coin machine decides `A` by strict +majority within `t` exactly when, on every instance, every run has halted by the clock and +`a ∈ A` exactly when more than half of the coin strings of length `t a` make the coin replay +`Turing.MultiTapePTM.runClosedCoins` output `[true]`. -/ +theorem decidesByMajorityInTime_iff {machine : MultiTapePTM k Bool State} + {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} : + machine.DecidesByMajorityInTime enc A t ↔ ∀ a, + (∀ final ∈ (ProbComp.eval + (machine.runClosedConfigFrom (t a) (machine.initialConfig (enc a)))).support, + final.tapes.state = none) ∧ + (a ∈ A ↔ 2 ^ t a < 2 * Complexity.acceptCount + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) + (enc a) (t a)) := by + refine forall_congr' fun a => and_congr_right' (iff_congr Iff.rfl ?_) + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, ← half_lt_div_iff] + simp only [Complexity.acceptCount, decide_eq_true_eq] + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM +open Cslib.Probability +open scoped ENNReal + +variable {α : Type*} + +/-- The problems decidable by strict majority within time `O(t n)`, that is `c₁ * t n + c₂` for +constants `c₁` and `c₂`, on instances whose encoding under `enc` has length `n`, by a fair-coin +machine with a binary alphabet and finitely many states: every run of that many steps has halted, +and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2` +[Gill][Gill1977]. -/ +def PPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := + {A | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) + (machine : MultiTapePTM k Bool State), + machine.DecidesByMajorityInTime enc A fun a => c₁ * t (enc a).length + c₂} + +/-- `PPTIME` is monotone in the time bound. -/ +theorem PPTIME_mono {enc : α ↪ List Bool} {t₁ t₂ : ℕ → ℕ} (h : ∀ n, t₁ n ≤ t₂ n) : + PPTIME enc t₁ ⊆ PPTIME enc t₂ := by + rintro A ⟨c₁, c₂, k, State, hfinite, machine, hA⟩ + exact ⟨c₁, c₂, k, State, hfinite, machine, + hA.mono fun a => Nat.add_le_add_right (Nat.mul_le_mul_left _ (h _)) _⟩ + +/-- **Bounded error is a strict majority**: a machine outputting the right answer with probability +at least `2 / 3` outputs `[true]` with probability at least `2 / 3` on members, and at most `1 / 3` +on the others. -/ +theorem BPTIME_subset_PPTIME {enc : α ↪ List Bool} {t : ℕ → ℕ} : + BPTIME enc t ⊆ PPTIME enc t := by + rintro A ⟨c₁, c₂, k, State, hfinite, machine, hA⟩ + refine ⟨c₁, c₂, k, State, hfinite, machine, fun a => ⟨(hA a).1, ?_⟩⟩ + have hprob := (hA a).2 + set p := ProbComp.eval (machine.runClosed (c₁ * t (enc a).length + c₂) (enc a)) + have hhalf : (1 / 2 : ℝ≥0∞) < 2 / 3 := by + refine (ENNReal.toReal_lt_toReal (ENNReal.div_ne_top (by norm_num) (by norm_num)) + (ENNReal.div_ne_top (by norm_num) (by norm_num))).mp ?_ + simp only [ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_ofNat] + norm_num + by_cases ha : a ∈ A + · simp only [MultiTapeTM.indicator, ha, ↓reduceIte] at hprob + exact iff_of_true ha (hhalf.trans_le hprob) + · simp only [MultiTapeTM.indicator, ha, ↓reduceIte] at hprob + refine iff_of_false ha fun hlt => ?_ + -- the outputs `[true]` and `[false]` together have probability at most one + have hsum : p [true] + p [false] ≤ 1 := by + calc p [true] + p [false] = ∑ x ∈ {[true], [false]}, p x := by + rw [Finset.sum_pair (by simp)] + _ ≤ ∑' x, p x := sum_le_tsum _ + _ = 1 := p.tsum_coe + have h1 : (1 / 2 : ℝ≥0∞) + 1 / 2 < p [true] + 1 / 2 := + ENNReal.add_lt_add_right (by norm_num) hlt + rw [ENNReal.add_halves] at h1 + exact (h1.trans_le ((add_le_add le_rfl (hhalf.le.trans hprob)).trans hsum)).false + +/-- **`PP` is the union of the classes `PPTIME (n ^ k)`** [Gill][Gill1977]: a polynomial-time +verifier run on uniformly sampled random strings is a fair-coin machine halting within a +polynomial clock, and a fair-coin machine halting within the clock `T` is a verifier replaying +random strings of length `T`. -/ +theorem mem_PP_iff_exists_mem_PPTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} : + A ∈ PP enc ↔ ∃ k, A ∈ PPTIME enc (· ^ k) := by + rw [mem_PP] + constructor + · rintro ⟨p, V, hV, hA⟩ + -- sample a random string and run the verifier on it + let program (a : α) : ProbComp Bool := + (fun w => V (a, w)) <$> BitString.sampleList (p.eval (enc a).length) + have hcount : ComputableInPolyTime (fun a => p.eval (enc a).length) enc encUnary := + (ComputableInPolyTime.unary_eval p).comp (ComputableInPolyTime.encoding_length enc) + have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with hV + obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hprogram.exists_halting_machine + refine ⟨d, c * 2 ^ d, c, k, State, hfinite, machine, + MultiTapePTM.DecidesByMajorityInTime.mono (t := fun a => c * ((enc a).length + 1) ^ d) + (fun a => ⟨hhalt (enc a), ?_⟩) fun a => Nat.mul_add_one_pow_le_two_pow c d _⟩ + -- the encoded output `[true]` has the probability of `true` + have htrue : + (ProbComp.eval (program a)).map encBool [true] = ProbComp.eval (program a) true := by + simp [PMF.map_apply, encBool_apply] + rw [← heval a, htrue] + simp only [program, ProbComp.eval_map, BitString.eval_sampleList] + rw [BitString.uniformList_map_apply, ← acceptCount, MultiTapePTM.half_lt_div_iff] + exact hA a + · rintro ⟨d, c₁, c₂, k, State, hfinite, machine, hA⟩ + -- replay the coins + refine ⟨Polynomial.C c₁ * Polynomial.X ^ d + Polynomial.C c₂, + fun x => decide (machine.runClosedCoins x.2 (enc x.1) = [true]), + ComputableInPolyTime.decide_eq' + ((MultiTapePTM.computableInPolyTime_runClosedCoins machine).comp + ((ComputableInPolyTime.snd enc encBits).prod + ((ComputableInPolyTime.of_eq (encOut := encBits) fun _ => rfl).comp + (ComputableInPolyTime.fst enc encBits)))) + (ComputableInPolyTime.const [true]), fun a => ?_⟩ + have heval : (Polynomial.C c₁ * Polynomial.X ^ d + Polynomial.C c₂).eval (enc a).length = + c₁ * (enc a).length ^ d + c₂ := by + simp + rw [heval, ((MultiTapePTM.decidesByMajorityInTime_iff.mp hA) a).2] + rfl + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean index 93d2df6a13..57c0226098 100644 --- a/Complexity/Computability/Complexity/Classes/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Time.lean @@ -45,6 +45,9 @@ instances, with a bound `t : ℕ → ℕ` of the length `n` of the encoded insta members and `[false]` for the others, with probability at least `2 / 3` [Arora and Barak, Definition 7.2][AroraBarak09]. +The unbounded-error class `Cslib.Complexity.PPTIME enc t`, decided by strict majority by the same +fair-coin machines, is in `Complexity.Computability.Complexity.Classes.PP.Time`. + Each polynomial class of the library is the union of the corresponding classes of time `O(n ^ k)`, as in the textbook [Arora and Barak, Definition 1.13, Theorem 2.6, Definition 7.2][AroraBarak09]: diff --git a/ComplexityTests/PPTime.lean b/ComplexityTests/PPTime.lean new file mode 100644 index 0000000000..3e01f752b4 --- /dev/null +++ b/ComplexityTests/PPTime.lean @@ -0,0 +1,72 @@ +/- +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.Inclusions +import Complexity.Computability.Complexity.Classes.PP.Time +import Complexity.Computability.Probabilistic.PPT.Clock +import Complexity.Tactic.PPT + +/-! Unbounded-error probabilistic time: members obtained from `P` through `BPP`, `PP` and +`BPTIME`, and a halting fair-coin machine that outputs `[true]` with probability exactly `1 / 2`, +which decides `∅` by strict majority but not `Set.univ`. -/ + +namespace ComplexityTests.PPTime + +open Cslib Cslib.Complexity Cslib.Probability Turing Turing.MultiTapeTM +open scoped ENNReal + +/-- Everything is decided by the constant `true`. -/ +theorem univ_mem_P : (Set.univ : Set (List Bool)) ∈ P encBits := + ⟨fun _ => true, .const true, fun _ => by simp⟩ + +/-- The words starting with `true`: neither empty nor everything. -/ +theorem headD_mem_P : {w : List Bool | w.headD false = true} ∈ P encBits := + ⟨fun w => w.headD false, by fun_prop, fun _ => Iff.rfl⟩ + +/-- `Set.univ` and the words starting with `true` are decided by strict majority in polynomial +time, through `PP`, and for the latter also through `BPTIME`. -/ +example : + (∃ k, (Set.univ : Set (List Bool)) ∈ PPTIME encBits (· ^ k)) ∧ + (∃ k, {w : List Bool | w.headD false = true} ∈ PPTIME encBits (· ^ k)) ∧ + (∃ k, {w : List Bool | w.headD false = true} ∈ PPTIME encBits (· ^ k)) := + ⟨mem_PP_iff_exists_mem_PPTIME.mp (BPP_subset_PP (P_subset_BPP univ_mem_P)), + mem_PP_iff_exists_mem_PPTIME.mp (BPP_subset_PP (P_subset_BPP headD_mem_P)), + let ⟨k, hk⟩ := mem_BPP_iff_exists_mem_BPTIME.mp (P_subset_BPP headD_mem_P) + ⟨k, BPTIME_subset_PPTIME hk⟩⟩ + +/-- A membership in `PPTIME (n ^ k)` gives back `PP`. -/ +example {A : Set (List Bool)} {k : ℕ} (h : A ∈ PPTIME encBits (· ^ k)) : A ∈ PP encBits := + mem_PP_iff_exists_mem_PPTIME.mpr ⟨k, h⟩ + +/-- **Strictness matters.** A halting fair-coin machine that outputs `[true]` with probability +exactly `1 / 2` decides `∅` by strict majority, and does not decide `Set.univ`. -/ +example : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) + (t : List Bool → ℕ), machine.DecidesByMajorityInTime encBits ∅ t ∧ + ¬ machine.DecidesByMajorityInTime encBits Set.univ t := by + have hcoin : IsPPTOn encBits encBool (fun _ => ProbComp.uniform Bool) := by fun_prop + obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hcoin.exists_halting_machine + have hhalf (w : List Bool) : + ProbComp.eval (machine.runClosed (c * ((encBits w).length + 1) ^ d) (encBits w)) [true] = + 1 / 2 := by + rw [← heval w] + simp [PMF.map_apply, encBool_apply] + refine ⟨k, State, hfinite, machine, fun w => c * ((encBits w).length + 1) ^ d, + fun w => ⟨hhalt w, ?_⟩, fun h => ?_⟩ + · rw [hhalf] + simp + · have := ((h []).2.mp (Set.mem_univ _)) + rw [hhalf] at this + exact lt_irrefl _ this + +/-- The count form of the majority condition: a machine deciding `Set.univ` by strict majority +accepts more than half of the coin strings of clock length on every word. -/ +example {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) {t : List Bool → ℕ} + (h : machine.DecidesByMajorityInTime encBits Set.univ t) (w : List Bool) : + 2 ^ t w < 2 * acceptCount + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) w (t w) := + ((MultiTapePTM.decidesByMajorityInTime_iff.mp h) w).2.mp (Set.mem_univ w) + +end ComplexityTests.PPTime From da93e6d6579ef4ba3ffca28fed5d8a91fff0018e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:41:53 -0400 Subject: [PATCH 02/10] feat(time): accepting choice-string counts for NTIME and BPTIME (#1833 H1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define the accepting count of a closed fair-coin table, the number of choice strings of a given length on which it emits [true], and relate it to the existing semantics: the probability of output [true] is the count divided by 2^τ; a nondeterministic decider's choice table has a positive count exactly on members; a bounded-error decider has a strict-majority count exactly on members, at every τ at least the clock. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Time/AcceptCount.lean | 137 +++++++++++++++ .../MultiTape/Probabilistic/AcceptCount.lean | 103 +++++++++++ ComplexityTests/HPVChoiceCount.lean | 161 ++++++++++++++++++ 4 files changed, 403 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean create mode 100644 ComplexityTests/HPVChoiceCount.lean diff --git a/Complexity.lean b/Complexity.lean index 3942e2e28b..ce92f5d3ef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1177,6 +1177,7 @@ public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Completeness public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Principles public import Complexity.Computability.Complexity.Classes.Time +public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting @@ -1795,6 +1796,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileC public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape diff --git a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean new file mode 100644 index 0000000000..47496225e5 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean @@ -0,0 +1,137 @@ +/- +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.Time +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount + +/-! +# Time classes through accepting choice strings + +Problems in `NTIME` and `BPTIME` are decided by comparing the accepting count of a fixed +binary-choice machine (`Turing.MultiTapePTM.acceptCount`) with a threshold, at every number `τ` +of choice bits at least a linear function of the time bound. This is the normal form used by +counting simulations of nondeterministic and probabilistic time, which compute the accepting +count exactly. + +* A nondeterministic decider is replayed by its choice table `Turing.MultiTapeNTM.choiceTable`, + which encodes each choice in binary and rejects at a stuck configuration: an instance is a + member exactly when the accepting count is positive + (`Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`). +* A bounded-error fair-coin decider accepts a member with probability at least `2 / 3` and a + nonmember with probability at most `1 / 3`, so an instance is a member exactly when more than + half of the choice strings accept + (`Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`). + +Both hold for every `τ` at least the clock: a halted table ignores further bits. + +## Main results + +* `Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`: nondeterministic + acceptance is a positive accepting count. +* `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`: + bounded-error acceptance is a strict-majority accepting count. +* `Cslib.Complexity.exists_acceptCount_of_mem_NTIME`, + `Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`: the class-level normal forms. +-/ + +public section + +namespace Turing.MultiTapeNTM + +variable {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} + +/-- **Nondeterministic acceptance is a positive accepting count.** If `ntm` decides `A` within +`t`, then `a ∈ A` exactly when some choice string of length `τ` makes the choice table accept, +for every `τ` of at least `M * t a`, where `M` is the number of actions. -/ +theorem DecidesInTime.mem_iff_acceptCount_choiceTable_pos {ntm : MultiTapeNTM k Bool State} + {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} + (hτ : Nat.card (Turing.Action k Bool State) * t a ≤ τ) : + a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ := by + rw [h.mem_iff_exists_checkChoices hτ, MultiTapePTM.acceptCount_pos_iff] + simp only [checkChoices, decide_eq_true_eq] + +end Turing.MultiTapeNTM + +namespace Turing.MultiTapePTM + +open Cslib +open scoped ENNReal + +variable {k : ℕ} {State : Type} {α : Type} {enc : α ↪ List Bool} + +/-- A probability of at least `2 / 3` is more than one half. -/ +private theorem inv_two_lt_of_two_div_three_le {p : ℝ≥0∞} (h : 2 / 3 ≤ p) : 2⁻¹ < p := by + refine lt_of_lt_of_le ?_ h + rw [ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ← ENNReal.div_eq_inv_mul, + ENNReal.div_lt_iff (by simp) (by simp)] + norm_num + +/-- Two distinct outcomes have total probability at most one. -/ +private theorem apply_add_apply_le_one {β : Type} (P : PMF β) {b b' : β} (hb : b ≠ b') : + P b + P b' ≤ 1 := by + classical + rw [← Finset.sum_pair hb, ← P.tsum_coe] + exact sum_le_tsum _ + +/-- **Bounded-error acceptance is a strict-majority accepting count.** If `machine` decides `A` +with bounded error within `t`, then `a ∈ A` exactly when more than half of the choice strings of +length `τ` accept, for every `τ` of at least `t a`. -/ +theorem DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount + {machine : MultiTapePTM k Bool State} {A : Set α} {t : α → ℕ} + (h : machine.DecidesWithBoundedErrorInTime enc A t) {a : α} {τ : ℕ} (hτ : t a ≤ τ) : + a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ := by + obtain ⟨hhalt, hprob⟩ := h a + rw [← machine.eval_runClosed_eq_of_halted (enc a) hτ hhalt] at hprob + rw [← half_lt_eval_runClosed_apply_iff] + by_cases ha : a ∈ A + · simp only [MultiTapeTM.indicator, ha] at hprob + exact iff_of_true ha (inv_two_lt_of_two_div_three_le hprob) + · simp only [MultiTapeTM.indicator, ha] at hprob + refine iff_of_false ha fun htrue => ?_ + have hsum := apply_add_apply_le_one (ProbComp.eval (machine.runClosed τ (enc a))) + (b := [true]) (b' := [false]) (by simp) + exact absurd ((ENNReal.inv_two_add_inv_two.symm.trans_lt + (ENNReal.add_lt_add htrue (inv_two_lt_of_two_div_three_le hprob))).trans_le hsum) + (lt_irrefl 1) + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} + +/-- **Nondeterministic time as accepting counts.** A problem in `NTIME enc t` is decided by a +fixed binary-choice machine with a binary alphabet and finitely many states: for constants `c₁` +and `c₂`, an instance is a member exactly when its accepting count on `τ` choice bits is +positive, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_NTIME (h : A ∈ NTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → (a ∈ A ↔ 0 < machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, ntm, hntm⟩ := h + set M := Nat.card (Turing.Action k Bool State) + refine ⟨k, _, inferInstance, ntm.choiceTable, M * c₁, M * c₂, fun a τ hτ => + hntm.mem_iff_acceptCount_choiceTable_pos ?_⟩ + rw [Nat.mul_add, ← Nat.mul_assoc] + exact hτ + +/-- **Bounded-error probabilistic time as accepting counts.** A problem in `BPTIME enc t` is +decided by a fixed fair-coin machine with a binary alphabet and finitely many states: for +constants `c₁` and `c₂`, an instance is a member exactly when more than half of its choice +strings of length `τ` accept, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_BPTIME (h : A ∈ BPTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → + (a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := h + exact ⟨k, State, hfinite, machine, c₁, c₂, fun a τ hτ => + hmachine.mem_iff_two_pow_lt_two_mul_acceptCount hτ⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean new file mode 100644 index 0000000000..1f0692c761 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean @@ -0,0 +1,103 @@ +/- +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.Machine.Nondeterministic +import Mathlib.Data.Fintype.Pi + +/-! +# Accepting choice strings of a fair-coin table + +A closed fair-coin table `Turing.MultiTapePTM k Bool State` is the binary-choice normal form of a +machine: a run is a deterministic replay of a list of choice bits, one bit per live step. When +both branches of an instruction agree, its bit is ignored, and a halted configuration ignores all +further bits (`Turing.MultiTapePTM.stepCoins`). So every run on `τ` bits is padded to exactly `τ` +steps. A nondeterministic machine with finitely many states and a binary alphabet is put in this +form by its choice table `Turing.MultiTapeNTM.choiceTable`, which encodes each choice in binary and +rejects at a stuck configuration. + +The *accepting count* `Turing.MultiTapePTM.acceptCount machine input τ` is the number of bit +strings `y ∈ {0,1}^τ` on which the table emits `[true]` on `input`: the count `A_M(x)` of the +counting simulations of nondeterministic and probabilistic time. Its fraction of all `2 ^ τ` +strings is exactly the probability that the closed fair-coin run outputs `[true]` +(`Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`). The membership characterizations +for nondeterministic and bounded-error deciders are in +`Complexity.Computability.Complexity.Classes.Time.AcceptCount`. + +## Main definitions + +* `Turing.MultiTapePTM.acceptCount`: the number of accepting choice strings of a given length. + +## Main results + +* `Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`: the probability of output `[true]` + is the accepting count divided by `2 ^ τ`. +* `Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff`: strict majority acceptance, as an + integer comparison `2 ^ τ < 2 * acceptCount`. +* `Turing.MultiTapePTM.acceptCount_pos_iff`: some choice string accepts. +* `Turing.MultiTapePTM.acceptCount_le_two_pow`: at most all `2 ^ τ` strings accept. +* `Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins`: the replay on upstream + configurations. +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib Cslib.Probability +open scoped ENNReal + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) + (τ : ℕ) + +/-- **The accepting count** `A_M(x)`: the number of choice strings `y ∈ {0,1}^τ` replaying +which the closed fair-coin table emits `[true]` on `input`. -/ +def acceptCount : ℕ := + (Finset.univ.filter fun y : Fin τ → Bool => + machine.runClosedCoins (List.ofFn y) input = [true]).card + +/-- At most all `2 ^ τ` choice strings accept. -/ +theorem acceptCount_le_two_pow : machine.acceptCount input τ ≤ 2 ^ τ := + (Finset.card_filter_le _ _).trans (by simp) + +/-- The accepting count is positive exactly when some choice string of length `τ` accepts. -/ +theorem acceptCount_pos_iff : + 0 < machine.acceptCount input τ ↔ + ∃ coins : List Bool, coins.length = τ ∧ machine.runClosedCoins coins input = [true] := by + rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] + constructor + · rintro ⟨y, -, hy⟩ + exact ⟨List.ofFn y, List.length_ofFn, hy⟩ + · rintro ⟨coins, rfl, hcoins⟩ + exact ⟨fun i => coins[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ + +/-- **Acceptance probability is the accepting fraction.** The closed fair-coin run with clock +`τ` outputs `[true]` with probability `acceptCount / 2 ^ τ`. -/ +theorem eval_runClosed_apply_eq_acceptCount : + ProbComp.eval (machine.runClosed τ input) [true] = + (machine.acceptCount input τ : ℝ≥0∞) / 2 ^ τ := by + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + rfl + +/-- **Strict majority acceptance** is the integer comparison `2 ^ τ < 2 * acceptCount`. -/ +theorem half_lt_eval_runClosed_apply_iff : + 2⁻¹ < ProbComp.eval (machine.runClosed τ input) [true] ↔ + 2 ^ τ < 2 * machine.acceptCount input τ := by + rw [eval_runClosed_apply_eq_acceptCount, ENNReal.lt_div_iff_mul_lt (by simp) (by simp), + ← ENNReal.div_eq_inv_mul, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] + exact_mod_cast Iff.rfl + +/-- The replay on the configurations of the shared interpreter is the replay on upstream +configurations, by deterministic steps under each coin. -/ +theorem runClosedCoins_eq_output_stepCoins (coins : List Bool) : + machine.runClosedCoins coins input = + (machine.stepCoins coins (Cfg.init machine.initial input)).output := by + rw [runClosedCoins, tapes_runClosedConfigFromCoins] + rfl + +end Turing.MultiTapePTM diff --git a/ComplexityTests/HPVChoiceCount.lean b/ComplexityTests/HPVChoiceCount.lean new file mode 100644 index 0000000000..d76ffc8f3b --- /dev/null +++ b/ComplexityTests/HPVChoiceCount.lean @@ -0,0 +1,161 @@ +/- +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.Time.AcceptCount + +/-! Accepting choice strings of concrete fair-coin and nondeterministic machines. -/ + +namespace ComplexityTests.HPVChoiceCount + +open Cslib Turing +open scoped ENNReal + +/-- Emit the first coin and halt. -/ +private def emitCoin : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none } + Empty.elim Empty.elim + +-- No step is taken without a choice bit: nothing is accepted. +example : emitCoin.acceptCount [] 0 = 0 := by decide + +-- After the first step the machine has halted, and the remaining bits are ignored. +example : emitCoin.acceptCount [] 1 = 1 := by decide +example : emitCoin.acceptCount [true, false] 3 = 4 := by decide + +-- The accepted fraction is the probability of output `[true]`. +example : ProbComp.eval (emitCoin.runClosed 3 [true, false]) [true] = 4 / 8 := by + rw [MultiTapePTM.eval_runClosed_apply_eq_acceptCount, + show emitCoin.acceptCount [true, false] 3 = 4 by decide] + norm_num + +-- Exactly half accept: this is not a strict majority. +example : ¬ 2⁻¹ < ProbComp.eval (emitCoin.runClosed 3 []) [true] := by + rw [MultiTapePTM.half_lt_eval_runClosed_apply_iff, + show emitCoin.acceptCount [] 3 = 4 by decide] + decide + +/-- Run two steps, each ignoring its coin, then emit `true` exactly when the input is +nonempty. -/ +private def readInput : MultiTapePTM 0 Bool (Fin 2) where + initial := 0 + tr state symbol _ _ _ := .step + (if state = 0 then { inputTape := 0, workTapes := Fin.elim0, output := none, state := some 1 } + else { inputTape := 0, workTapes := Fin.elim0, output := some symbol.isSome, state := none }) + Empty.elim Empty.elim + +-- Ignored bits still count: every string accepts, or none does. +example : readInput.acceptCount [false] 3 = 8 := by decide +example : readInput.acceptCount [] 3 = 0 := by decide +-- Before the decision step, no string accepts. +example : readInput.acceptCount [false] 1 = 0 := by decide + +/-! ### A bounded-error decider and the strict-majority criterion -/ + +/-- Emit `true` exactly when the first input symbol is `true`, ignoring the coin. -/ +private def echo : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ _ := .step + { inputTape := 0, workTapes := Fin.elim0, output := some (symbol == some true), state := none } + Empty.elim Empty.elim + +/-- `echo` decides `{true}` (encoded as one-symbol words) with no error within one step. -/ +private theorem echo_decides : + echo.DecidesWithBoundedErrorInTime MultiTapeTM.encBool {b | b = true} fun _ => 1 := by + intro a + refine ⟨fun final hfinal => ?_, ?_⟩ + · rw [MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins, PMF.mem_support_map_iff] at hfinal + obtain ⟨coins, hcoins, rfl⟩ := hfinal + obtain ⟨c, rfl⟩ := List.length_eq_one_iff.mp + (BitString.mem_support_uniformList_iff.mp hcoins) + cases a <;> cases c <;> rfl + · rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + cases a + · rw [show MultiTapeTM.indicator {b : Bool | b = true} false = false by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool false) = [false]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + · rw [show MultiTapeTM.indicator {b : Bool | b = true} true = true by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool true) = [true]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + +-- With more bits than the clock, a member is accepted by all `2 ^ 4` strings. +example : true ∈ {b : Bool | b = true} ↔ 2 ^ 4 < 2 * echo.acceptCount [true] 4 := + echo_decides.mem_iff_two_pow_lt_two_mul_acceptCount (a := true) (by norm_num) +example : echo.acceptCount [true] 4 = 16 ∧ echo.acceptCount [false] 4 = 0 := by decide + +/-! ### Nondeterministic deciders through their choice tables -/ + +/-- Halt with output `[b]`. -/ +private def emit (b : Bool) : Action 0 Bool Bool := + { inputTape := 0, workTapes := Fin.elim0, output := some b, state := none } + +/-- From its only running state, either accept or reject. -/ +private def guess : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr q _ _ action := q = false ∧ (action = emit true ∨ action = emit false) + +private theorem guess_decides : + guess.DecidesInTime (Function.Embedding.refl (List Bool)) Set.univ fun _ => 1 := by + intro a + refine ⟨MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun c hc => ?_, ?_⟩ + · simp only [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init] at hc + obtain ⟨action, ⟨-, rfl | rfl⟩, rfl⟩ := hc <;> rfl + · have hstep : guess.Step (guess.initCfg a) ((emit true).apply (guess.initCfg a)) := + ⟨emit true, ⟨rfl, .inl rfl⟩, rfl⟩ + exact iff_of_true trivial + ⟨⟨(RelSeries.singleton _ _).cons (guess.initCfg a) hstep, rfl⟩, rfl, rfl⟩ + +-- The accepting branch is encoded by some padded choice string, of every sufficient length. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + 0 < guess.choiceTable.acceptCount x τ := + (guess_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mp trivial + +/-- A machine permitting no action: its initial configuration is stuck. -/ +private def stuck : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr _ _ _ _ := False + +private theorem stuck_decides : + stuck.DecidesInTime (Function.Embedding.refl (List Bool)) ∅ fun _ => 1 := by + intro a + have hrun : stuck.RunsInTime a 1 := + MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun _ hc => by + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at hc + refine ⟨hrun, iff_of_false id fun hacc => ?_⟩ + obtain ⟨p, hp, -⟩ := (MultiTapeNTM.accepts_iff_exists_time_eq hrun).mp hacc + have h0 := p.toRunPath.step ⟨0, by + unfold MultiTapeNTM.ComputationPath.time MultiTapeNTM.RunPath.time at hp; omega⟩ + change stuck.Step (p.toRunPath 0) _ at h0 + rw [show p.toRunPath 0 = stuck.initCfg a from p.head_eq] at h0 + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at h0 + +-- The choice table rejects at the stuck configuration: no choice string accepts. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + stuck.choiceTable.acceptCount x τ = 0 := + Nat.eq_zero_of_not_pos fun h => + (stuck_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mpr h + +/-! ### Class-level normal forms -/ + +example : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1 := + ⟨1, 0, 0, Unit, inferInstance, echo, by simpa using echo_decides⟩ + +example (h : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) + (c₁ c₂ : ℕ), ∀ a τ, c₁ * 1 + c₂ ≤ τ → + (a ∈ {b : Bool | b = true} ↔ 2 ^ τ < 2 * machine.acceptCount (MultiTapeTM.encBool a) τ) := + Complexity.exists_acceptCount_of_mem_BPTIME h + +end ComplexityTests.HPVChoiceCount From 6f551680dd16ee5045925ad1d2643da3a62d2cc1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:54:12 -0400 Subject: [PATCH 03/10] refactor(Classes/PP): derive the majority count form from acceptCount_le_half_iff Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/PP/Time.lean | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean index 5775864e39..53c78531d3 100644 --- a/Complexity/Computability/Complexity/Classes/PP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -90,16 +90,15 @@ theorem DecidesByMajorityInTime.mono {machine : MultiTapePTM k Bool State} exact hhalt · rwa [machine.eval_runClosed_eq_of_halted _ (ht a) hhalt] -/-- A probability `c / 2 ^ n` exceeds one half exactly when `2 ^ n < 2 * c`. -/ -private theorem half_lt_div_iff {c n : ℕ} : - (1 / 2 : ℝ≥0∞) < c / 2 ^ n ↔ 2 ^ n < 2 * c := by - have h2n : (2 : ℝ≥0∞) ^ n ≠ 0 := pow_ne_zero _ two_ne_zero - have h2n' : (2 : ℝ≥0∞) ^ n ≠ ⊤ := ENNReal.pow_ne_top ENNReal.ofNat_ne_top - rw [ENNReal.lt_div_iff_mul_lt (Or.inl h2n) (Or.inl h2n'), one_div, mul_comm, - ← div_eq_mul_inv, ENNReal.div_lt_iff (Or.inl two_ne_zero) (Or.inl ENNReal.ofNat_ne_top), - show ((c : ℝ≥0∞) * 2) = ((2 * c : ℕ) : ℝ≥0∞) by push_cast; ring, - show ((2 : ℝ≥0∞) ^ n) = ((2 ^ n : ℕ) : ℝ≥0∞) by push_cast; rfl] - exact Nat.cast_lt +/-- More than half of the random words are accepted exactly when they are accepted with +probability more than one half. -/ +private theorem half_lt_uniformList_map_iff {β : Type} (V : β × List Bool → Bool) (b : β) + (n : ℕ) : 1 / 2 < ((BitString.uniformList n).map fun w => V (b, w)) true ↔ + 2 ^ n < 2 * Complexity.acceptCount V b n := by + have hne : ((BitString.uniformList n).map fun w => V (b, w)) true ≠ ⊤ := PMF.apply_ne_top _ _ + rw [← not_iff_not, not_lt, not_lt, Complexity.acceptCount_le_half_iff, + ← ENNReal.toReal_le_toReal hne (by simp)] + simp /-- **Deciding by majority is a count comparison.** A fair-coin machine decides `A` by strict majority within `t` exactly when, on every instance, every run has halted by the clock and @@ -115,8 +114,16 @@ theorem decidesByMajorityInTime_iff {machine : MultiTapePTM k Bool State} (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) (enc a) (t a)) := by refine forall_congr' fun a => and_congr_right' (iff_congr Iff.rfl ?_) - rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, ← half_lt_div_iff] - simp only [Complexity.acceptCount, decide_eq_true_eq] + -- the probability of `[true]` is the accepted fraction of the coin strings + have hprob : ProbComp.eval (machine.runClosed (t a) (enc a)) [true] = + ((BitString.uniformList (t a)).map fun w => + decide (machine.runClosedCoins w (enc a) = [true])) true := by + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply, + BitString.uniformList_map_apply] + simp only [decide_eq_true_eq] + rw [hprob] + exact half_lt_uniformList_map_iff + (fun x : List Bool × List Bool => decide (machine.runClosedCoins x.2 x.1 = [true])) _ _ end Turing.MultiTapePTM @@ -200,7 +207,7 @@ theorem mem_PP_iff_exists_mem_PPTIME {α : Type} {enc : α ↪ List Bool} {A : S simp [PMF.map_apply, encBool_apply] rw [← heval a, htrue] simp only [program, ProbComp.eval_map, BitString.eval_sampleList] - rw [BitString.uniformList_map_apply, ← acceptCount, MultiTapePTM.half_lt_div_iff] + rw [MultiTapePTM.half_lt_uniformList_map_iff] exact hA a · rintro ⟨d, c₁, c₂, k, State, hfinite, machine, hA⟩ -- replay the coins From 49bd81d41c598a1ffef95aabb5d9da390773d6c7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:58:23 -0400 Subject: [PATCH 04/10] feat(Foundations/Nat): exponent arithmetic and residue recovery for counting simulations Nat.SqrtLog: estimates for the scale n / Nat.sqrt (Nat.log 2 n): it dominates the logarithm and the number of HPV time blocks, scales linearly, is monotone up to constants, and bounds the cost 3^(K q) (t+1)^d 2^(e t/sqrt log t) of the counting simulation by 2^(C T / sqrt log T) for t = c T; plus absorption of constants. Nat.ResidueSum: streamed sums modulo m and exact recovery of a count below m. Tests compare the natural scale with the real n / sqrt(log2 n). E1 groundwork for #1833. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Foundations/Data/Nat/ResidueSum.lean | 59 ++++ Complexity/Foundations/Data/Nat/SqrtLog.lean | 269 ++++++++++++++++++ ComplexityTests/ResidueSum.lean | 32 +++ ComplexityTests/SqrtLog.lean | 121 ++++++++ 5 files changed, 483 insertions(+) create mode 100644 Complexity/Foundations/Data/Nat/ResidueSum.lean create mode 100644 Complexity/Foundations/Data/Nat/SqrtLog.lean create mode 100644 ComplexityTests/ResidueSum.lean create mode 100644 ComplexityTests/SqrtLog.lean diff --git a/Complexity.lean b/Complexity.lean index 1cd97a4651..5dd44a8b2f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2667,6 +2667,8 @@ public import Complexity.Foundations.Data.Nat.Prime public import Complexity.Foundations.Data.Nat.Primrec public import Complexity.Foundations.Data.Nat.Radix public import Complexity.Foundations.Data.Nat.Radix.Measurement +public import Complexity.Foundations.Data.Nat.ResidueSum +public import Complexity.Foundations.Data.Nat.SqrtLog public import Complexity.Foundations.Data.Nat.SqrtRatio public import Complexity.Foundations.Data.Nat.Subexponential public import Complexity.Foundations.Data.Option diff --git a/Complexity/Foundations/Data/Nat/ResidueSum.lean b/Complexity/Foundations/Data/Nat/ResidueSum.lean new file mode 100644 index 0000000000..11de1d9eb9 --- /dev/null +++ b/Complexity/Foundations/Data/Nat/ResidueSum.lean @@ -0,0 +1,59 @@ +/- +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 Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.List.Range +import Mathlib.Algebra.Order.BigOperators.Group.Finset + +/-! +# Exact counts from streamed residues + +A count `N` that is known to lie below a modulus `m` is recovered exactly from residues modulo +`m`: an accumulator that adds one term at a time and reduces modulo `m` ends at the sum of the terms +modulo `m` (`Nat.foldl_range_add_mod`), and if the terms are congruent to numbers summing to +`N < m`, it ends at `N` itself (`Nat.foldl_range_add_mod_eq_of_lt`). The workspace is one residue, +however many terms are added. + +This is how the deterministic counting simulations of #1833 obtain the exact number of accepting +choice strings, at most `2 ^ τ`, from contractions computed modulo `2 ^ (τ + 1)` and summed over +all movement schedules. + +## Main results + +* `Nat.foldl_range_add_mod`: streaming a sum modulo `m`. +* `Nat.foldl_range_add_mod_eq_of_lt`: exact recovery of a count below the modulus. +-/ + +public section + +namespace Nat + +/-- **Streaming a sum modulo `m`.** Adding the terms `f 0, …, f (n - 1)` one at a time to the +residue of `a` and reducing modulo `m` after each step gives `(a + ∑ f i) % m`. -/ +theorem foldl_range_add_mod (f : ℕ → ℕ) (m a n : ℕ) : + (List.range n).foldl (fun acc i => (acc + f i) % m) (a % m) = + (a + ∑ i ∈ Finset.range n, f i) % m := by + induction n with + | zero => simp + | succ n ih => + rw [List.range_succ, List.foldl_append, ih, List.foldl_cons, List.foldl_nil, + Finset.sum_range_succ, Nat.mod_add_mod, Nat.add_assoc] + +/-- **Exact recovery of a count below the modulus.** If each term `f i` is congruent modulo `m` +to `g i`, and the `g i` sum to `N < m`, the streamed sum of the `f i` modulo `m`, from `0`, is +exactly `N`. -/ +theorem foldl_range_add_mod_eq_of_lt {f g : ℕ → ℕ} {m n N : ℕ} + (hfg : ∀ i < n, f i % m = g i % m) (hsum : ∑ i ∈ Finset.range n, g i = N) (hN : N < m) : + (List.range n).foldl (fun acc i => (acc + f i) % m) 0 = N := by + have h := foldl_range_add_mod f m 0 n + rw [Nat.zero_mod, Nat.zero_add] at h + rw [h, Finset.sum_nat_mod, Finset.sum_congr rfl fun i hi => hfg i (Finset.mem_range.mp hi), + ← Finset.sum_nat_mod, hsum, Nat.mod_eq_of_lt hN] + +end Nat diff --git a/Complexity/Foundations/Data/Nat/SqrtLog.lean b/Complexity/Foundations/Data/Nat/SqrtLog.lean new file mode 100644 index 0000000000..d7ca69b97a --- /dev/null +++ b/Complexity/Foundations/Data/Nat/SqrtLog.lean @@ -0,0 +1,269 @@ +/- +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.Data.Nat.CeilDiv +public import Mathlib.Data.Nat.Log +public import Mathlib.Data.Nat.Sqrt +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# The scale `n / √(log n)` + +Natural-number estimates for the scale `n / Nat.sqrt (Nat.log 2 n)`, that is `⌊n / ⌊√⌊log₂ n⌋⌋⌋`, +in which the deterministic simulations of nondeterministic and probabilistic time by blocking and +tensor contraction are stated (#1833). From `n = 2` on the divisor is positive +(`Nat.one_le_sqrt_log_two`), and so is the scale (`Nat.one_le_div_sqrt_log_two`). + +The scale dominates the logarithm (`Nat.log_two_le_div_sqrt_log_two`), hence every polynomial in +the exponent, and the number `⌈n / ⌈log₂ (n + 2)⌉⌉` of time blocks of length `⌈log₂ (n + 2)⌉` +(`Nat.ceilDiv_clog_two_le`). Scaling `n` by a constant scales it by at most that constant, up to +an additive constant (`Nat.mul_div_sqrt_log_two_le`). The scale is not monotone, since the divisor +jumps, but it is monotone up to constants (`Nat.div_sqrt_log_two_le_of_le`), so a bound in a +smaller size, such as the number of edges of a network, transfers to the clock. Together these +give the exponent arithmetic of the simulation: for `t = c * T`, with `q = ⌈t / ⌈log₂ (t + 2)⌉⌉` +blocks, the cost `3 ^ (K * q) * (t + 1) ^ d * 2 ^ (e * t / √⌊log₂ t⌋)` of enumerating the movement +schedules, building the networks and contracting them is `2 ^ O(T / √⌊log₂ T⌋)` +(`Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`). + +The floors cost only constant factors: the natural scale is between the real scale +`n / √(log₂ n)` minus one and three times it, which is checked in the test suite. + +## Main results + +* `Nat.log_two_le_div_sqrt_log_two`: `⌊log₂ n⌋ ≤ n / √⌊log₂ n⌋`. +* `Nat.ceilDiv_clog_two_le`: `⌈n / ⌈log₂ (n + 2)⌉⌉ ≤ n / √⌊log₂ n⌋ + 1`. +* `Nat.mul_div_sqrt_log_two_le`: the scale of `c * n` is at most `c` times that of `n`, plus `c`. +* `Nat.div_sqrt_log_two_le_of_le`: the scale is monotone up to constants. +* `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`: the cost of the counting simulation. +* `Nat.mul_two_pow_add_le_two_pow`, `Nat.mul_two_pow_div_sqrt_log_two_add_le`, + `Nat.mul_add_one_pow_add_le_pow`: absorbing constants into exponential and polynomial bounds. +-/ + +public section + +namespace Nat + +/-- The divisor `√⌊log₂ n⌋` is positive from `n = 2` on. -/ +theorem one_le_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : 1 ≤ sqrt (log 2 n) := + le_sqrt.2 (by rw [one_mul]; exact log_pos one_lt_two hn) + +/-- The divisor `√⌊log₂ n⌋` is monotone. -/ +theorem sqrt_log_two_mono : Monotone fun n => sqrt (log 2 n) := + fun _ _ h => sqrt_le_sqrt (log_mono_right h) + +/-- `m ^ 3 ≤ 4 ^ m`. -/ +private theorem cube_le_four_pow : ∀ m : ℕ, m ^ 3 ≤ 4 ^ m + | 0 => by decide + | 1 => by decide + | 2 => by decide + | m + 3 => by + have ih := cube_le_four_pow (m + 2) + have h : (m + 3) ^ 3 ≤ 4 * (m + 2) ^ 3 := by ring_nf; nlinarith + calc (m + 3) ^ 3 ≤ 4 * (m + 2) ^ 3 := h + _ ≤ 4 * 4 ^ (m + 2) := Nat.mul_le_mul_left 4 ih + _ = 4 ^ (m + 3) := by ring + +/-- `⌊log₂ n⌋ * √⌊log₂ n⌋ ≤ n`: with `L = ⌊log₂ n⌋`, `(L √L) ^ 2 ≤ L ^ 3 ≤ 4 ^ L ≤ n ^ 2`. -/ +theorem log_two_mul_sqrt_log_two_le (n : ℕ) : log 2 n * sqrt (log 2 n) ≤ n := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + set L := log 2 n + have h2L : 2 ^ L ≤ n := pow_log_le_self 2 hn.ne' + have hsq : (L * sqrt L) ^ 2 ≤ (2 ^ L) ^ 2 := by + calc (L * sqrt L) ^ 2 = L * L * (sqrt L * sqrt L) := by ring + _ ≤ L * L * L := Nat.mul_le_mul_left _ (sqrt_le L) + _ = L ^ 3 := by ring + _ ≤ 4 ^ L := cube_le_four_pow L + _ = (2 ^ L) ^ 2 := by rw [← pow_mul, mul_comm, pow_mul]; norm_num + exact ((Nat.pow_le_pow_iff_left (by norm_num)).1 hsq).trans h2L + +/-- **The scale dominates the logarithm**: `⌊log₂ n⌋ ≤ n / √⌊log₂ n⌋`. -/ +theorem log_two_le_div_sqrt_log_two (n : ℕ) : log 2 n ≤ n / sqrt (log 2 n) := by + rcases Nat.lt_or_ge n 2 with hn | hn + · simp [log_of_lt hn] + · exact (le_div_iff_mul_le (one_le_sqrt_log_two hn)).2 (log_two_mul_sqrt_log_two_le n) + +/-- The scale is positive from `n = 2` on. -/ +theorem one_le_div_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : 1 ≤ n / sqrt (log 2 n) := + (log_pos one_lt_two hn).trans_le (log_two_le_div_sqrt_log_two n) + +/-- **Time blocks.** There are at most `n / √⌊log₂ n⌋ + 1` blocks of length `⌈log₂ (n + 2)⌉` in +`n` steps, since `√⌊log₂ n⌋ ≤ ⌈log₂ (n + 2)⌉`. -/ +theorem ceilDiv_clog_two_le (n : ℕ) : n ⌈/⌉ clog 2 (n + 2) ≤ n / sqrt (log 2 n) + 1 := by + have hb : 0 < clog 2 (n + 2) := clog_pos one_lt_two (by omega) + rw [ceilDiv_le_iff hb] + rcases Nat.lt_or_ge n 2 with hn | hn + · interval_cases n + · exact Nat.zero_le _ + · simp [show clog 2 3 = 2 by decide] + · have hr := one_le_sqrt_log_two hn + have hle : sqrt (log 2 n) ≤ clog 2 (n + 2) := + (sqrt_le_self _).trans ((log_mono_right (by omega : n ≤ n + 2)).trans (log_le_clog 2 _)) + calc n ≤ (n / sqrt (log 2 n) + 1) * sqrt (log 2 n) := by + have := lt_div_mul_add (a := n) hr + rw [add_mul, one_mul] + omega + _ ≤ _ := Nat.mul_le_mul_left _ hle + +/-- Multiplying before dividing gains less than the multiplier: `c * n / r ≤ c * (n / r) + c`. -/ +theorem mul_div_le_mul_div_add (c n r : ℕ) : c * n / r ≤ c * (n / r) + c := by + rcases Nat.eq_zero_or_pos r with rfl | hr + · simp + apply Nat.div_le_of_le_mul + have := lt_div_mul_add (a := n) hr + have h : n ≤ r * (n / r + 1) := by rw [mul_add, mul_one, mul_comm]; omega + calc c * n ≤ c * (r * (n / r + 1)) := Nat.mul_le_mul_left _ h + _ = r * (c * (n / r) + c) := by ring + +/-- **Scaling.** The scale of `c * n` is at most `c` times the scale of `n`, plus `c`: the divisor +only grows. -/ +theorem mul_div_sqrt_log_two_le (c n : ℕ) : + c * n / sqrt (log 2 (c * n)) ≤ c * (n / sqrt (log 2 n)) + c := by + rcases Nat.lt_or_ge n 2 with hn | hn + · calc c * n / _ ≤ c * n := div_le_self _ _ + _ ≤ c * 1 := Nat.mul_le_mul_left _ (by omega) + _ ≤ _ := by omega + rcases Nat.eq_zero_or_pos c with rfl | hc + · simp + have hr := one_le_sqrt_log_two hn + calc c * n / sqrt (log 2 (c * n)) ≤ c * n / sqrt (log 2 n) := + div_le_div_left (sqrt_log_two_mono (Nat.le_mul_of_pos_left n hc)) hr + _ ≤ c * (n / sqrt (log 2 n)) + c := mul_div_le_mul_div_add c n _ + +/-- **The scale is monotone up to constants**: `m ≤ n` gives +`m / √⌊log₂ m⌋ ≤ 2 * (n / √⌊log₂ n⌋) + 2`. When the divisors are within a factor `2` of each other +this is division by the smaller divisor; otherwise `m` is so much smaller than `n` that +`m * √⌊log₂ n⌋ ≤ n`. -/ +theorem div_sqrt_log_two_le_of_le {m n : ℕ} (h : m ≤ n) : + m / sqrt (log 2 m) ≤ 2 * (n / sqrt (log 2 n)) + 2 := by + rcases Nat.lt_or_ge m 2 with hm | hm + · simp [log_of_lt hm] + set a := sqrt (log 2 m) + set b := sqrt (log 2 n) + have ha : 1 ≤ a := one_le_sqrt_log_two hm + have hab : a ≤ b := sqrt_log_two_mono h + rcases le_or_gt b (2 * a) with hb | hb + · calc m / a ≤ n / a := Nat.div_le_div_right h + _ = 2 * n / (2 * a) := (Nat.mul_div_mul_left n a two_pos).symm + _ ≤ 2 * n / b := Nat.div_le_div_left hb (ha.trans hab) + _ ≤ 2 * (n / b) + 2 := mul_div_le_mul_div_add 2 n b + · -- `m < 2 ^ ((a + 1) ^ 2)` and `2 ^ (b ^ 2) ≤ n`, with `(a + 1) ^ 2 + b ≤ b ^ 2` + have hm2 : m < 2 ^ ((a + 1) * (a + 1)) := + (lt_pow_succ_log_self one_lt_two m).trans_le + (Nat.pow_le_pow_right two_pos (lt_succ_sqrt (log 2 m))) + have hn2 : 2 ^ (b * b) ≤ n := + (Nat.pow_le_pow_right two_pos (sqrt_le (log 2 n))).trans (pow_log_le_self 2 (by omega)) + have hexp : (a + 1) * (a + 1) + b ≤ b * b := by nlinarith + have hmb : m * b ≤ n := + calc m * b ≤ 2 ^ ((a + 1) * (a + 1)) * 2 ^ b := + Nat.mul_le_mul hm2.le Nat.lt_two_pow_self.le + _ = 2 ^ ((a + 1) * (a + 1) + b) := (pow_add _ _ _).symm + _ ≤ 2 ^ (b * b) := Nat.pow_le_pow_right two_pos hexp + _ ≤ n := hn2 + calc m / a ≤ m := Nat.div_le_self _ _ + _ ≤ n / b := (Nat.le_div_iff_mul_le (by omega)).2 hmb + _ ≤ 2 * (n / b) + 2 := by omega + +/-- **The cost of the counting simulation is `2 ^ O(T / √(log T))`** (#1833). For `t = c * T`, +time blocks of length `b = ⌈log₂ (t + 2)⌉` and `q = ⌈t / b⌉` blocks, the number `3 ^ (K * q)` of +movement schedules of `K` heads, a polynomial `(t + 1) ^ d` and a contraction cost +`2 ^ (e * t / √⌊log₂ t⌋)` multiply to at most `2 ^ (C * T / √⌊log₂ T⌋)` from `T = 2` on, for a +constant `C` depending only on `K`, `c`, `d` and `e`. -/ +theorem exists_three_pow_mul_le_two_pow_div_sqrt_log_two (K c d e : ℕ) : ∃ C, ∀ T, 2 ≤ T → + 3 ^ (K * (c * T ⌈/⌉ clog 2 (c * T + 2))) * (c * T + 1) ^ d * + 2 ^ (e * (c * T) / sqrt (log 2 (c * T))) ≤ + 2 ^ (C * T / sqrt (log 2 T)) := by + refine ⟨(2 * K + d + e) * (2 * c + 1), fun T hT => ?_⟩ + set S := T / sqrt (log 2 T) + set t := c * T + have hS : 1 ≤ S := one_le_div_sqrt_log_two hT + -- the scale of `t` is at most `2 c S` + have ht : t / sqrt (log 2 t) ≤ c * S + c := mul_div_sqrt_log_two_le c T + have hcS : c * S + c ≤ 2 * c * S := by nlinarith + -- the number of movement schedules + have hq : t ⌈/⌉ clog 2 (t + 2) ≤ (2 * c + 1) * S := by + have := ceilDiv_clog_two_le t + nlinarith + have h3 : 3 ^ (K * (t ⌈/⌉ clog 2 (t + 2))) ≤ 2 ^ (2 * K * ((2 * c + 1) * S)) := by + calc 3 ^ (K * (t ⌈/⌉ clog 2 (t + 2))) ≤ 4 ^ (K * (t ⌈/⌉ clog 2 (t + 2))) := + Nat.pow_le_pow_left (by norm_num) _ + _ = 2 ^ (2 * (K * (t ⌈/⌉ clog 2 (t + 2)))) := by + rw [show (4 : ℕ) = 2 ^ 2 by norm_num, ← pow_mul] + _ ≤ 2 ^ (2 * K * ((2 * c + 1) * S)) := Nat.pow_le_pow_right (by norm_num) (by + rw [← mul_assoc]; exact Nat.mul_le_mul_left _ hq) + -- the polynomial factor + have hpoly : (t + 1) ^ d ≤ 2 ^ (d * ((2 * c + 1) * S)) := by + have hlog : log 2 t + 1 ≤ (2 * c + 1) * S := by + have := log_two_le_div_sqrt_log_two t + nlinarith + calc (t + 1) ^ d ≤ (2 ^ (log 2 t + 1)) ^ d := + Nat.pow_le_pow_left (lt_pow_succ_log_self one_lt_two t) d + _ = 2 ^ (d * (log 2 t + 1)) := by rw [← pow_mul, mul_comm] + _ ≤ 2 ^ (d * ((2 * c + 1) * S)) := + Nat.pow_le_pow_right (by norm_num) (Nat.mul_le_mul_left _ hlog) + -- the contraction factor + have hcon : 2 ^ (e * t / sqrt (log 2 t)) ≤ 2 ^ (e * ((2 * c + 1) * S)) := by + refine Nat.pow_le_pow_right (by norm_num) ?_ + have := mul_div_le_mul_div_add e t (sqrt (log 2 t)) + nlinarith + calc 3 ^ (K * (t ⌈/⌉ clog 2 (t + 2))) * (t + 1) ^ d * 2 ^ (e * t / sqrt (log 2 t)) + ≤ 2 ^ (2 * K * ((2 * c + 1) * S)) * 2 ^ (d * ((2 * c + 1) * S)) * + 2 ^ (e * ((2 * c + 1) * S)) := Nat.mul_le_mul (Nat.mul_le_mul h3 hpoly) hcon + _ = 2 ^ ((2 * K + d + e) * (2 * c + 1) * S) := by rw [← pow_add, ← pow_add]; ring_nf + _ ≤ 2 ^ ((2 * K + d + e) * (2 * c + 1) * T / sqrt (log 2 T)) := + Nat.pow_le_pow_right (by norm_num) (mul_div_le_mul_div_assoc _ _ _) + +/-- A constant factor and an additive constant are absorbed by a positive exponent: +`a * 2 ^ (c * x) + b ≤ 2 ^ ((a + b + c) * x)` for `1 ≤ x`. -/ +theorem mul_two_pow_add_le_two_pow {a b c x : ℕ} (hx : 1 ≤ x) : + a * 2 ^ (c * x) + b ≤ 2 ^ ((a + b + c) * x) := by + have h1 : 1 ≤ 2 ^ (c * x) := Nat.one_le_two_pow + have hab : a + b < 2 ^ (a + b) := Nat.lt_two_pow_self + have hab' : 2 ^ (a + b) ≤ 2 ^ ((a + b) * x) := Nat.pow_le_pow_right (by norm_num) (by nlinarith) + calc a * 2 ^ (c * x) + b ≤ (a + b) * 2 ^ (c * x) := by nlinarith + _ ≤ 2 ^ ((a + b) * x) * 2 ^ (c * x) := Nat.mul_le_mul_right _ (hab.le.trans hab') + _ = 2 ^ ((a + b + c) * x) := by rw [← pow_add]; ring_nf + +/-- A constant factor and an additive constant are absorbed into the constant of +`2 ^ O(T / √⌊log₂ T⌋)` from `T = 2` on. -/ +theorem mul_two_pow_div_sqrt_log_two_add_le {a b C T : ℕ} (hT : 2 ≤ T) : + a * 2 ^ (C * T / sqrt (log 2 T)) + b ≤ + 2 ^ ((a + b + 1) * (C + 1) * T / sqrt (log 2 T)) := by + set x := (C + 1) * T / sqrt (log 2 T) + have hx : 1 ≤ x := + (one_le_div_sqrt_log_two hT).trans + ((Nat.le_mul_of_pos_left _ (Nat.succ_pos C)).trans (mul_div_le_mul_div_assoc _ _ _)) + have hCx : C * T / sqrt (log 2 T) ≤ 1 * x := by + rw [one_mul] + exact Nat.div_le_div_right (Nat.mul_le_mul_right _ (Nat.le_succ C)) + calc a * 2 ^ (C * T / sqrt (log 2 T)) + b ≤ a * 2 ^ (1 * x) + b := by + gcongr + _ ≤ 2 ^ ((a + b + 1) * x) := mul_two_pow_add_le_two_pow hx + _ ≤ 2 ^ ((a + b + 1) * (C + 1) * T / sqrt (log 2 T)) := by + refine Nat.pow_le_pow_right (by norm_num) ?_ + rw [mul_assoc] + exact mul_div_le_mul_div_assoc _ _ _ + +/-- A constant factor and an additive constant are absorbed by the degree from `n = 2` on: +`a * (n + 1) ^ d + b ≤ n ^ (a + b + 2 * d)`. -/ +theorem mul_add_one_pow_add_le_pow {a b d n : ℕ} (hn : 2 ≤ n) : + a * (n + 1) ^ d + b ≤ n ^ (a + b + 2 * d) := by + have hsq : (n + 1) ^ d ≤ n ^ (2 * d) := by + rw [pow_mul] + exact Nat.pow_le_pow_left (by nlinarith) d + have h1 : 1 ≤ n ^ (2 * d) := Nat.one_le_pow _ _ (by omega) + have hab : a + b < 2 ^ (a + b) := Nat.lt_two_pow_self + have hab' : 2 ^ (a + b) ≤ n ^ (a + b) := Nat.pow_le_pow_left hn _ + calc a * (n + 1) ^ d + b ≤ (a + b) * n ^ (2 * d) := by nlinarith + _ ≤ n ^ (a + b) * n ^ (2 * d) := Nat.mul_le_mul_right _ (hab.le.trans hab') + _ = n ^ (a + b + 2 * d) := by rw [← pow_add] + +end Nat diff --git a/ComplexityTests/ResidueSum.lean b/ComplexityTests/ResidueSum.lean new file mode 100644 index 0000000000..35d0e72ab6 --- /dev/null +++ b/ComplexityTests/ResidueSum.lean @@ -0,0 +1,32 @@ +/- +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.Foundations.Data.Nat.ResidueSum + +/-! Exact counts from streamed residues: recovery below the modulus, and its failure above. -/ + +namespace ComplexityTests.ResidueSum + +open Nat + +-- The terms `8, 9, 10` are `0, 1, 2` modulo `8`, which sum to `3 < 8`: the streamed residue is +-- the count `3`, by the lemma and by evaluation. +example : (List.range 3).foldl (fun acc i => (acc + (8 + i)) % 8) 0 = 3 := + foldl_range_add_mod_eq_of_lt (g := fun i => i) (fun i _ => by omega) (by decide) (by decide) + +example : (List.range 3).foldl (fun acc i => (acc + (8 + i)) % 8) 0 = 3 := by decide + +-- Above the modulus the residue loses the count: two terms `5` sum to `10`, streamed as `2`. +example : (List.range 2).foldl (fun acc _ => (acc + 5) % 8) 0 = 2 ∧ + ∑ _i ∈ Finset.range 2, 5 = 10 := by decide + +-- Streaming from a nonzero start adds its residue. +example (f : ℕ → ℕ) (n : ℕ) : + (List.range n).foldl (fun acc i => (acc + f i) % 2 ^ 5) (37 % 2 ^ 5) = + (37 + ∑ i ∈ Finset.range n, f i) % 2 ^ 5 := + foldl_range_add_mod f _ 37 n + +end ComplexityTests.ResidueSum diff --git a/ComplexityTests/SqrtLog.lean b/ComplexityTests/SqrtLog.lean new file mode 100644 index 0000000000..33ab6ed75e --- /dev/null +++ b/ComplexityTests/SqrtLog.lean @@ -0,0 +1,121 @@ +/- +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.Foundations.Data.Nat.SqrtLog +import Mathlib.Analysis.SpecialFunctions.Log.Base +import Mathlib.Analysis.SpecialFunctions.Pow.Real + +/-! The scale `n / √⌊log₂ n⌋` of the counting simulations: concrete values, the agreement of the +natural scale with the real scale `n / √(log₂ n)` up to constant factors, which makes +`2 ^ O(n / √⌊log₂ n⌋)` the usual `2 ^ O(n / √(log n))`, and the exponent arithmetic on an +instance. -/ + +namespace ComplexityTests.SqrtLog + +open Nat + +/-! ### Concrete values -/ + +-- `⌊log₂ 16⌋ = 4`, so the divisor is `2` and the scale is `8`. +example : 16 / sqrt (log 2 16) = 8 := by + have h1 : log 2 16 = 4 := by rw [show (16 : ℕ) = 2 ^ 4 by rfl, log_pow one_lt_two] + have h2 : sqrt 4 = 2 := (eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + rw [h1, h2] + +-- The divisor is `1` at `n = 2` and `n = 15`, and `0` at `n = 1`. +example : sqrt (log 2 15) = 1 ∧ sqrt (log 2 2) = 1 ∧ sqrt (log 2 1) = 0 := by + have h15 : log 2 15 = 3 := by rw [log_eq_iff (by norm_num)]; norm_num + have h2 : log 2 2 = 1 := by rw [log_eq_iff (by norm_num)]; norm_num + refine ⟨?_, ?_, by simp⟩ + · rw [h15] + exact (eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + · rw [h2] + exact (eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + +-- The scale is not monotone: it drops from `15` at `n = 15` to `8` at `n = 16`, where the divisor +-- jumps. It is monotone up to the constants of `div_sqrt_log_two_le_of_le`. +example : 16 / sqrt (log 2 16) < 15 / sqrt (log 2 15) ∧ + 15 / sqrt (log 2 15) ≤ 2 * (16 / sqrt (log 2 16)) + 2 := by + have h16 : log 2 16 = 4 := by rw [show (16 : ℕ) = 2 ^ 4 by rfl, log_pow one_lt_two] + have h15 : log 2 15 = 3 := by rw [log_eq_iff (by norm_num)]; norm_num + have h4 : sqrt 4 = 2 := (eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + have h3 : sqrt 3 = 1 := (eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + rw [h16, h15, h4, h3] + decide + +-- `20` steps in blocks of length `⌈log₂ 22⌉` need at most `20 / 2 + 1 = 11` blocks. +example : 20 ⌈/⌉ clog 2 (20 + 2) ≤ 20 / sqrt (log 2 20) + 1 := ceilDiv_clog_two_le 20 + +/-! ### The natural scale is the real scale up to constants -/ + +/-- The natural scale is at least the real scale, up to one. -/ +theorem div_sqrt_logb_le (n : ℕ) (hn : 2 ≤ n) : + (n : ℝ) / √(Real.logb 2 n) ≤ ((n / sqrt (log 2 n) : ℕ) : ℝ) + 1 := by + have hr := one_le_sqrt_log_two hn + have hlogb : 0 ≤ Real.logb 2 n := + Real.logb_nonneg (by norm_num) (by exact_mod_cast (by omega : 1 ≤ n)) + -- `√⌊log₂ n⌋ ≤ √(log₂ n)` + have hle : (sqrt (log 2 n) : ℝ) ≤ √(Real.logb 2 n) := by + rw [Real.le_sqrt (by positivity) hlogb] + have h1 : ((sqrt (log 2 n) * sqrt (log 2 n) : ℕ) : ℝ) ≤ (log 2 n : ℕ) := by + exact_mod_cast sqrt_le _ + have h2 := Real.natLog_le_logb n 2 + push_cast at h1 h2 + nlinarith + have hdiv : (n : ℝ) / √(Real.logb 2 n) ≤ (n : ℝ) / sqrt (log 2 n) := + div_le_div_of_nonneg_left (by positivity) (by exact_mod_cast hr) hle + refine hdiv.trans ?_ + rw [div_le_iff₀ (by exact_mod_cast hr)] + have : (n : ℝ) ≤ ((n / sqrt (log 2 n) : ℕ) : ℝ) * sqrt (log 2 n) + sqrt (log 2 n) := by + exact_mod_cast (lt_div_mul_add (a := n) hr).le + nlinarith + +/-- The natural scale is at most three times the real scale. -/ +theorem div_sqrt_log_two_le (n : ℕ) (hn : 2 ≤ n) : + ((n / sqrt (log 2 n) : ℕ) : ℝ) ≤ 3 * ((n : ℝ) / √(Real.logb 2 n)) := by + set L := log 2 n + set r := sqrt L + have hr : 1 ≤ r := one_le_sqrt_log_two hn + -- `log₂ n < L + 1 < (r + 1) ^ 2 + 1 ≤ 9 r ^ 2` + have hlogb : Real.logb 2 n < L + 1 := by + rw [Real.logb_lt_iff_lt_rpow (by norm_num) (by positivity)] + have h : (n : ℝ) < (2 : ℝ) ^ (L + 1) := by + exact_mod_cast lt_pow_succ_log_self one_lt_two n + rw [← Real.rpow_natCast] at h + exact_mod_cast h + have hLr : L < (r + 1) * (r + 1) := lt_succ_sqrt L + have hpos : 0 < Real.logb 2 n := Real.logb_pos (by norm_num) (by exact_mod_cast hn) + have hsq : √(Real.logb 2 n) ≤ 3 * r := by + rw [Real.sqrt_le_left (by positivity)] + have : (L : ℝ) + 1 ≤ 9 * (r : ℝ) ^ 2 := by + have h1 : (L : ℝ) < ((r : ℝ) + 1) * ((r : ℝ) + 1) := by exact_mod_cast hLr + have h2 : (1 : ℝ) ≤ r := by exact_mod_cast hr + nlinarith + nlinarith + calc ((n / r : ℕ) : ℝ) ≤ (n : ℝ) / r := Nat.cast_div_le + _ ≤ 3 * ((n : ℝ) / √(Real.logb 2 n)) := by + rw [mul_div_assoc', le_div_iff₀ (Real.sqrt_pos.2 hpos), div_mul_eq_mul_div, + div_le_iff₀ (by exact_mod_cast hr)] + nlinarith [(Nat.cast_nonneg n : (0 : ℝ) ≤ n)] + +/-! ### Exponent arithmetic -/ + +-- Two heads, a clock `3 T`, a cubic polynomial and a contraction exponent `5`: one constant +-- bounds the cost for every `T ≥ 2`, and also absorbs a factor `7` and an addend `11`. +example : ∃ C, ∀ T, 2 ≤ T → + 7 * (3 ^ (2 * (3 * T ⌈/⌉ clog 2 (3 * T + 2))) * (3 * T + 1) ^ 3 * + 2 ^ (5 * (3 * T) / sqrt (log 2 (3 * T)))) + 11 ≤ + 2 ^ (C * T / sqrt (log 2 T)) := by + obtain ⟨C, hC⟩ := exists_three_pow_mul_le_two_pow_div_sqrt_log_two 2 3 3 5 + exact ⟨(7 + 11 + 1) * (C + 1), fun T hT => + (Nat.add_le_add_right (Nat.mul_le_mul_left 7 (hC T hT)) 11).trans + (mul_two_pow_div_sqrt_log_two_add_le hT)⟩ + +-- The space bound: `5 (T + 1) ^ 4 + 9 ≤ T ^ 22` from `T = 2` on. +example (T : ℕ) (hT : 2 ≤ T) : 5 * (T + 1) ^ 4 + 9 ≤ T ^ 22 := + mul_add_one_pow_add_le_pow hT + +end ComplexityTests.SqrtLog From eee8995b80d817546a40bd3edcb2877b89ec5ebf Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:05:39 -0400 Subject: [PATCH 05/10] fix(Foundations/Nat): publicly import Complexity.Init in ResidueSum Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity/Foundations/Data/Nat/ResidueSum.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Complexity/Foundations/Data/Nat/ResidueSum.lean b/Complexity/Foundations/Data/Nat/ResidueSum.lean index 11de1d9eb9..96270db115 100644 --- a/Complexity/Foundations/Data/Nat/ResidueSum.lean +++ b/Complexity/Foundations/Data/Nat/ResidueSum.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Init public import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Data.List.Range import Mathlib.Algebra.Order.BigOperators.Group.Finset From b7576bcda7f3f2574939699dbf8735d15944e60f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:11:24 -0400 Subject: [PATCH 06/10] refactor(complexity): share the generic accepted-string count with machines Move `Cslib.Complexity.acceptCount` and its elementary lemmas unchanged from `Classes/SharpP.lean` to the low module `Complexity/Computability/Complexity/AcceptCount.lean`, which SharpP re-exports. Define `Turing.MultiTapePTM.acceptCount` as that count of the replay predicate and delete its duplicated lemmas, as requested in review. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Computability/Complexity/AcceptCount.lean | 119 ++++++++++++++++++ .../Complexity/Classes/SharpP.lean | 84 +------------ .../Complexity/Classes/Time/AcceptCount.lean | 4 +- .../MultiTape/Probabilistic/AcceptCount.lean | 32 ++--- 5 files changed, 134 insertions(+), 106 deletions(-) create mode 100644 Complexity/Computability/Complexity/AcceptCount.lean diff --git a/Complexity.lean b/Complexity.lean index ce92f5d3ef..f6e56784bc 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -984,6 +984,7 @@ public import Complexity.Computability.Communication.TopDown.Adversary public import Complexity.Computability.Communication.TopDown.Majority public import Complexity.Computability.Communication.TopDown.Parity public import Complexity.Computability.Communication.TopDown.Rectangle +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.AffineDisperser public import Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial public import Complexity.Computability.Complexity.AffineDisperser.Coordinates diff --git a/Complexity/Computability/Complexity/AcceptCount.lean b/Complexity/Computability/Complexity/AcceptCount.lean new file mode 100644 index 0000000000..c14ce50bbb --- /dev/null +++ b/Complexity/Computability/Complexity/AcceptCount.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.Fintype.Pi +import Complexity.Foundations.Data.BitString.WordCount + +/-! +# Counting accepted strings + +`Cslib.Complexity.acceptCount V a n` is the number of strings `w` of length `n` with +`V (a, w) = true`, for any Boolean predicate `V : α × List Bool → Bool`. No efficiency of `V` is +assumed. It counts the certificates of a verifier in the counting classes +(`Cslib.Complexity.SharpP`), the random strings accepted by a bounded-error or majority verifier, +and the choice strings accepted by a fair-coin machine (`Turing.MultiTapePTM.acceptCount`). + +## Main definitions + +* `Cslib.Complexity.acceptCount`: the number of accepted strings of a given length. + +## Main results + +* `Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`: the range + and support of the count. +* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. +* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, + `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +variable {α : Type} + +/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ +def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card + +section acceptCount + +variable {V : α × List Bool → Bool} {a : α} {n : ℕ} + +/-- At most all `2 ^ n` strings are accepted. -/ +theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := + (Finset.card_filter_le _ _).trans (by simp) + +/-- Some string of length `n` is accepted exactly when the count is positive. -/ +theorem acceptCount_pos_iff : + 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by + rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] + constructor + · rintro ⟨w, -, hw⟩ + exact ⟨List.ofFn w, List.length_ofFn, hw⟩ + · rintro ⟨w, rfl, hw⟩ + exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ + +/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ +theorem acceptCount_add_card_filter_eq_false : + acceptCount V a n + + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by + have := Finset.card_filter_add_card_filter_not (s := Finset.univ) + fun w : Fin n → Bool => V (a, List.ofFn w) = true + simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin] using this + +/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the +strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ +theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : + acceptCount V a (m + n) = + ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by + have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true + simp only [List.take_append_drop] at h + exact h + +/-- Verifiers that agree on an instance accept the same strings with it. -/ +theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : + acceptCount V a n = acceptCount W a n := by + simp only [acceptCount, h] + +/-- With no bits there is one string, the empty one. -/ +theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : + acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by + unfold acceptCount + rw [Finset.univ_unique, Finset.filter_singleton] + split_ifs with h₁ h₂ h₂ <;> simp_all + +/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ +@[simp] +theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by + simp [acceptCount] + +/-- The verifier rejecting everything accepts no string. -/ +@[simp] +theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by + simp [acceptCount] + +/-- A verifier and its negation together accept every string once. -/ +theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by + simpa only [acceptCount, Bool.not_eq_true'] using + acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) + +/-- The negation of a verifier accepts the strings that it rejects. -/ +theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by + have := acceptCount_add_acceptCount_not V a n + omega + +end acceptCount + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/SharpP.lean b/Complexity/Computability/Complexity/Classes/SharpP.lean index c61dce990f..a8141bc0e6 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP.lean @@ -7,12 +7,12 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.Classes.NP public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain public import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Algebra.Order.Group.Int public import Mathlib.Data.Fintype.Pi -import Complexity.Foundations.Data.BitString.WordCount /-! # The counting classes #P and GapP @@ -21,7 +21,8 @@ import Complexity.Foundations.Data.BitString.WordCount [Valiant][Valiant1979], [Arora and Barak, Chapter 17][AroraBarak09]: `f ∈ SharpP enc` when there are a polynomial `p` and a function `V : α × List Bool → Bool`, computable in polynomial time on inputs `encPair enc encBits (a, w) = frame (enc a) ++ w`, such that `f a` is the number of strings -`w` of length `p (enc a).length` with `V (a, w) = true`. The problems in `NP` are exactly the sets +`w` of length `p (enc a).length` with `V (a, w) = true`, the count `Cslib.Complexity.acceptCount` +of `Complexity.Computability.Complexity.AcceptCount`. The problems in `NP` are exactly the sets where functions in `#P` are nonzero (`mem_NP_iff_exists_SharpP`). `GapP` consists of the differences of two functions in `#P`. Fenner, Fortnow and Kurtz define it @@ -36,16 +37,11 @@ signed routing and the corresponding bidirectional `GapP` characterization. ## Main definitions -* `Cslib.Complexity.acceptCount`: the number of strings of a given length that a verifier accepts - together with an instance. * `Cslib.Complexity.SharpP`, `Cslib.Complexity.GapP`. ## Main results * `Cslib.Complexity.mem_NP_iff_exists_SharpP`: `NP` consists of the supports of functions in `#P`. -* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. -* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, - `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. * `Cslib.Complexity.SharpP.exists_le_two_pow`: functions in `#P` are at most exponential. * `Cslib.Complexity.GapP.exists_abs_le_two_pow`: every `GapP` function is bounded in absolute value by `2 ^ p(|x|)` for a polynomial `p`. @@ -66,80 +62,6 @@ open Turing.MultiTapeTM variable {α : Type} -/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ -def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card - -section acceptCount - -variable {V : α × List Bool → Bool} {a : α} {n : ℕ} - -theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := - (Finset.card_filter_le _ _).trans (by simp) - -theorem acceptCount_pos_iff : - 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by - rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] - constructor - · rintro ⟨w, -, hw⟩ - exact ⟨List.ofFn w, List.length_ofFn, hw⟩ - · rintro ⟨w, rfl, hw⟩ - exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ - -/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ -theorem acceptCount_add_card_filter_eq_false : - acceptCount V a n + - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by - have := Finset.card_filter_add_card_filter_not (s := Finset.univ) - fun w : Fin n → Bool => V (a, List.ofFn w) = true - simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, - Fintype.card_fin] using this - -/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the -strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ -theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : - acceptCount V a (m + n) = - ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by - have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true - simp only [List.take_append_drop] at h - exact h - -/-- Verifiers that agree on an instance accept the same strings with it. -/ -theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : - acceptCount V a n = acceptCount W a n := by - simp only [acceptCount, h] - -/-- With no bits there is one string, the empty one. -/ -theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : - acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by - unfold acceptCount - rw [Finset.univ_unique, Finset.filter_singleton] - split_ifs with h₁ h₂ h₂ <;> simp_all - -/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ -@[simp] -theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by - simp [acceptCount] - -/-- The verifier rejecting everything accepts no string. -/ -@[simp] -theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by - simp [acceptCount] - -/-- A verifier and its negation together accept every string once. -/ -theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by - simpa only [acceptCount, Bool.not_eq_true'] using - acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) - -/-- The negation of a verifier accepts the strings that it rejects. -/ -theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by - have := acceptCount_add_acceptCount_not V a n - omega - -end acceptCount - /-- The functions counting the certificates that a polynomial-time verifier accepts, with certificates of polynomial length, with respect to the encoding `enc` of instances. -/ def SharpP (enc : α ↪ List Bool) : Set (α → ℕ) := diff --git a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean index 47496225e5..714b56d7b4 100644 --- a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean +++ b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean @@ -53,8 +53,8 @@ theorem DecidesInTime.mem_iff_acceptCount_choiceTable_pos {ntm : MultiTapeNTM k {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} (hτ : Nat.card (Turing.Action k Bool State) * t a ≤ τ) : a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ := by - rw [h.mem_iff_exists_checkChoices hτ, MultiTapePTM.acceptCount_pos_iff] - simp only [checkChoices, decide_eq_true_eq] + rw [h.mem_iff_exists_checkChoices hτ, Cslib.Complexity.acceptCount_pos_iff] + rfl end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean index 1f0692c761..a81d09a827 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean @@ -7,8 +7,8 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic -import Mathlib.Data.Fintype.Pi /-! # Accepting choice strings of a fair-coin table @@ -23,7 +23,10 @@ rejects at a stuck configuration. The *accepting count* `Turing.MultiTapePTM.acceptCount machine input τ` is the number of bit strings `y ∈ {0,1}^τ` on which the table emits `[true]` on `input`: the count `A_M(x)` of the -counting simulations of nondeterministic and probabilistic time. Its fraction of all `2 ^ τ` +counting simulations of nondeterministic and probabilistic time. It is the generic count +`Cslib.Complexity.acceptCount` of the replay predicate, so the elementary lemmas about that count +(`Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`, …) apply +to it directly. Its fraction of all `2 ^ τ` strings is exactly the probability that the closed fair-coin run outputs `[true]` (`Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`). The membership characterizations for nondeterministic and bounded-error deciders are in @@ -39,8 +42,6 @@ for nondeterministic and bounded-error deciders are in is the accepting count divided by `2 ^ τ`. * `Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff`: strict majority acceptance, as an integer comparison `2 ^ τ < 2 * acceptCount`. -* `Turing.MultiTapePTM.acceptCount_pos_iff`: some choice string accepts. -* `Turing.MultiTapePTM.acceptCount_le_two_pow`: at most all `2 ^ τ` strings accept. * `Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins`: the replay on upstream configurations. -/ @@ -57,24 +58,9 @@ variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : /-- **The accepting count** `A_M(x)`: the number of choice strings `y ∈ {0,1}^τ` replaying which the closed fair-coin table emits `[true]` on `input`. -/ -def acceptCount : ℕ := - (Finset.univ.filter fun y : Fin τ → Bool => - machine.runClosedCoins (List.ofFn y) input = [true]).card - -/-- At most all `2 ^ τ` choice strings accept. -/ -theorem acceptCount_le_two_pow : machine.acceptCount input τ ≤ 2 ^ τ := - (Finset.card_filter_le _ _).trans (by simp) - -/-- The accepting count is positive exactly when some choice string of length `τ` accepts. -/ -theorem acceptCount_pos_iff : - 0 < machine.acceptCount input τ ↔ - ∃ coins : List Bool, coins.length = τ ∧ machine.runClosedCoins coins input = [true] := by - rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] - constructor - · rintro ⟨y, -, hy⟩ - exact ⟨List.ofFn y, List.length_ofFn, hy⟩ - · rintro ⟨coins, rfl, hcoins⟩ - exact ⟨fun i => coins[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ +abbrev acceptCount : ℕ := + Complexity.acceptCount + (fun p : List Bool × List Bool => decide (machine.runClosedCoins p.2 p.1 = [true])) input τ /-- **Acceptance probability is the accepting fraction.** The closed fair-coin run with clock `τ` outputs `[true]` with probability `acceptCount / 2 ^ τ`. -/ @@ -82,7 +68,7 @@ theorem eval_runClosed_apply_eq_acceptCount : ProbComp.eval (machine.runClosed τ input) [true] = (machine.acceptCount input τ : ℝ≥0∞) / 2 ^ τ := by rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] - rfl + simp only [Complexity.acceptCount, decide_eq_true_eq] /-- **Strict majority acceptance** is the integer comparison `2 ^ τ < 2 * acceptCount`. -/ theorem half_lt_eval_runClosed_apply_iff : From 9d3a07815efe9d48e13fef808b0264ca57cecf9f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:27:52 -0400 Subject: [PATCH 07/10] doc(Classes/PP): state the PPTIME threshold as a library convention Address the #1847 review: stop attributing the timed predicate to Gill. The module docstring now records the convention: strict acceptance, ties reject, outputs other than `[true]` unconstrained. It also records that the agreement with `PP` is a union over polynomial clocks and that no fixed-time comparison with other conventions is proved. Gill stays as background in the references. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/PP/Time.lean | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/PP/Time.lean b/Complexity/Computability/Complexity/Classes/PP/Time.lean index 53c78531d3..ed5778dabb 100644 --- a/Complexity/Computability/Complexity/Classes/PP/Time.lean +++ b/Complexity/Computability/Complexity/Classes/PP/Time.lean @@ -24,9 +24,19 @@ import Complexity.Computability.Probabilistic.Sampling `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, by a fair-coin machine with a binary alphabet and finitely many states (`Turing.MultiTapePTM.DecidesByMajorityInTime`): every run on that many coins has halted, and `a ∈ A` exactly when the run outputs `[true]` with -probability more than `1 / 2` [Gill][Gill1977]. It is the unbounded-error counterpart of +probability more than `1 / 2`. It is the unbounded-error counterpart of `Cslib.Complexity.BPTIME`, with the same machines and clocks. +**Convention.** Unbounded-error probabilistic computation goes back to Gill [Gill1977]. The timed +predicate here is this library's convention, not a transcription of a source definition: acceptance +is strict and ties reject. A nonmember may output `[true]` with probability exactly `1 / 2`, and +its other outputs are unconstrained, so it need not output `[false]` with probability more than +`1 / 2`. This is the threshold of the library's verifier-based `PP` +(`Cslib.Complexity.DecidesByMajority`), and the two agree at polynomial time +(`Cslib.Complexity.mem_PP_iff_exists_mem_PPTIME`). That equivalence is a union over all polynomial +clocks; for a fixed time bound, no comparison with conventions that require a strict majority of +`[false]` on nonmembers is proved here. + A fair-coin machine draws one coin per live step, so its acceptance probability within the clock `t` is the number of accepting coin strings of length `t` divided by `2 ^ t`. Deciding by majority is therefore the comparison `2 ^ t < 2 * count` of that count, an `Cslib.Complexity.acceptCount` @@ -71,7 +81,9 @@ variable {k : ℕ} {State : Type} {α : Type*} /-- `machine` decides `A` by strict majority within `t`, relative to the encoding `enc`: on every encoded instance `enc a`, every run of `t a` steps with fair coins has halted, and `a ∈ A` exactly -when the run outputs `[true]` with probability more than `1 / 2` [Gill][Gill1977]. -/ +when the run outputs `[true]` with probability more than `1 / 2`. Ties reject, and outputs other +than `[true]` are unconstrained; this is the library's convention, described in the module +docstring. -/ def DecidesByMajorityInTime (machine : MultiTapePTM k Bool State) (enc : α ↪ List Bool) (A : Set α) (t : α → ℕ) : Prop := ∀ a, (∀ final ∈ (ProbComp.eval @@ -138,8 +150,8 @@ variable {α : Type*} /-- The problems decidable by strict majority within time `O(t n)`, that is `c₁ * t n + c₂` for constants `c₁` and `c₂`, on instances whose encoding under `enc` has length `n`, by a fair-coin machine with a binary alphabet and finitely many states: every run of that many steps has halted, -and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2` -[Gill][Gill1977]. -/ +and `a ∈ A` exactly when the run outputs `[true]` with probability more than `1 / 2`. Ties reject +(`Turing.MultiTapePTM.DecidesByMajorityInTime`). -/ def PPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) := {A | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State), @@ -182,7 +194,7 @@ theorem BPTIME_subset_PPTIME {enc : α ↪ List Bool} {t : ℕ → ℕ} : rw [ENNReal.add_halves] at h1 exact (h1.trans_le ((add_le_add le_rfl (hhalf.le.trans hprob)).trans hsum)).false -/-- **`PP` is the union of the classes `PPTIME (n ^ k)`** [Gill][Gill1977]: a polynomial-time +/-- **`PP` is the union of the classes `PPTIME (n ^ k)`**: a polynomial-time verifier run on uniformly sampled random strings is a fair-coin machine halting within a polynomial clock, and a fair-coin machine halting within the clock `T` is a verifier replaying random strings of length `T`. -/ From 4fe33981a01ea0db45e8cfbecf7da6d0725e5043 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:38:58 -0400 Subject: [PATCH 08/10] feat(Classes/CountingSimulation): conditional assembly of the counting simulation (#1833 E1) The deterministic simulation of #1833, assembled from two stated interfaces: a network family (the block-counting step, H3) and a contraction algorithm (Theorem D.1 with l = 1, T2). Conditional on both. - Accumulate: streamed sum modulo a computed modulus over a binary index (IndexFold), with a native time/space certificate. - Interfaces: blocking parameters, ContractionAlgorithm, NetworkFamily. - Assembly: simulate, simulate_eq, exists_computableInO_simulate and exists_computableInO_count (time 2^(C T/sqrt(log T)), space T^d). - Tests: concrete sums and parameters, toy instances of both interfaces. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../CountingSimulation/Accumulate.lean | 287 +++++++++++ .../Classes/CountingSimulation/Assembly.lean | 464 ++++++++++++++++++ .../CountingSimulation/Interfaces.lean | 165 +++++++ ComplexityTests/CountingSimulation.lean | 140 ++++++ 5 files changed, 1059 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean create mode 100644 ComplexityTests/CountingSimulation.lean diff --git a/Complexity.lean b/Complexity.lean index 508a8e566b..649b3f7f52 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1027,6 +1027,9 @@ public import Complexity.Computability.Complexity.Classes.Constructible public import Complexity.Computability.Complexity.Classes.Constructible.Log public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace public import Complexity.Computability.Complexity.Classes.Counting.Space +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces public import Complexity.Computability.Complexity.Classes.DP public import Complexity.Computability.Complexity.Classes.EXP public import Complexity.Computability.Complexity.Classes.FewP diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean new file mode 100644 index 0000000000..a464744eb1 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean @@ -0,0 +1,287 @@ +/- +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.GenericRAM.Native.IndexFold +public import Complexity.Foundations.Data.Nat.ResidueSum +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv + +/-! +# Streamed sums modulo a computed modulus + +`Cslib.Complexity.CountingSimulation.modSum r modulus count c` adds the terms `r (c, 0)`, …, +`r (c, count c - 1)` to an accumulator one at a time, reducing modulo `modulus c` after each +addition. The terms are visited by the binary-index fold `Cslib.GenericRAM.IndexFold`, which keeps +only the index, the context `c` and the accumulator, so the workspace does not grow with the +number of terms. + +This is the outer loop of the deterministic counting simulation of #1833: the context is the input +and the clock, the terms are the residues of the contractions of the networks of the movement +schedules, and the modulus is a power of two above the count being recovered +(`Nat.foldl_range_add_mod_eq_of_lt`). + +The resource bound (`Cslib.Complexity.CountingSimulation.exists_computableInO_modSum`) is a native +multi-tape certificate: if the number of terms and the modulus are computable in polynomial time, +the terms lie below the modulus, and a certificate computes the term at every summed index within +time `R c` and space `Q c`, then the streamed sum is computable within time +`(count c + 1) * (poly + R c)` and space `poly + Q c`, for a polynomial in the encoded length of the +context. Neither `R` nor `Q` needs to be polynomial. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.modSumStep`: one round of the streamed sum. +* `Cslib.Complexity.CountingSimulation.modSum`: the streamed sum modulo the modulus. + +## Main results + +* `Cslib.Complexity.CountingSimulation.modSum_eq_sum_mod`: the streamed sum is the sum of the terms + modulo the modulus. +* `Cslib.Complexity.CountingSimulation.exists_computableInO_modSum`: its time and space bounds. +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM Cslib.GenericRAM + +variable {C : Type} + +/-- One round of the streamed sum at index `p.1`, with context `p.2.1` and accumulator `p.2.2`: +below the number of terms, add the term and reduce modulo the modulus; otherwise leave the state +unchanged. -/ +def modSumStep (r : C × ℕ → ℕ) (modulus count : C → ℕ) (p : ℕ × (C × ℕ)) : C × ℕ := + if p.1 < count p.2.1 then (p.2.1, (p.2.2 + r (p.2.1, p.1)) % modulus p.2.1) else p.2 + +/-- The terms `r (c, 0)`, …, `r (c, count c - 1)` summed one at a time from zero, reducing modulo +`modulus c` after each addition, by a streaming fold over a binary index. -/ +def modSum (r : C × ℕ → ℕ) (modulus count : C → ℕ) (c : C) : ℕ := + (IndexFold.run (modSumStep r modulus count) (count c) (c, 0)).2.2 + +variable {r : C × ℕ → ℕ} {modulus count : C → ℕ} + +/-- The state of the streamed sum after `j ≤ count c` rounds: the index `j`, the unchanged context +and the residue of the first `j` terms. -/ +theorem run_modSumStep {c : C} {j : ℕ} (hj : j ≤ count c) : + IndexFold.run (modSumStep r modulus count) j (c, 0) = + (j, (c, (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0)) := by + induction j with + | zero => rfl + | succ j ih => + rw [IndexFold.run_succ, ih (by omega)] + simp only [IndexFold.step, modSumStep, (show j < count c by omega), ↓reduceIte, List.range_succ, + List.foldl_append, List.foldl_cons, List.foldl_nil] + +/-- **The streamed sum is the sum modulo the modulus.** -/ +theorem modSum_eq_sum_mod (r : C × ℕ → ℕ) (modulus count : C → ℕ) (c : C) : + modSum r modulus count c = (∑ i ∈ Finset.range (count c), r (c, i)) % modulus c := by + have h := Nat.foldl_range_add_mod (fun i => r (c, i)) (modulus c) 0 (count c) + rw [Nat.zero_mod, Nat.zero_add] at h + rw [modSum, run_modSumStep le_rfl, h] + +private theorem foldl_add_mod_lt {f : ℕ → ℕ} {m : ℕ} (hm : 0 < m) (j : ℕ) : + (List.range j).foldl (fun acc i => (acc + f i) % m) 0 < m := by + cases j with + | zero => exact hm + | succ j => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil] + exact Nat.mod_lt _ hm + +private theorem polyBounded_comp_poly {size u : C → ℕ} {p : ℕ → ℕ} + (hp : Cslib.PolynomiallyBounded p) (hu : PolyBounded size u) : + PolyBounded size fun c => p (u c) := + (PolyBounded.of_polynomiallyBounded id hp).comp hu + +/-- **Resource bound of the streamed sum.** Suppose the number of terms and the modulus are +computable in polynomial time, the modulus is positive, every summed term lies below it, and a +native certificate computes the terms within time `R c` and space `Q c` at the summed indices. +Then the streamed sum is computable within time `(count c + 1) * (a * (n + 1) ^ d + R c)` and space +`a * (n + 1) ^ d + Q c`, where `n` is the encoded length of the context and `a`, `d` are constants: +the workspace holds one binary index, the context and an accumulator below the modulus. -/ +theorem exists_computableInO_modSum {encC : C ↪ List Bool} + (hmodulus : ComputableInPolyTime modulus encC encNat) + (hcount : ComputableInPolyTime count encC encNat) + (cr : NativeCertificate r (encPair encC encNat) encNat) + (hpos : ∀ c, 0 < modulus c) (hr : ∀ c i, i < count c → r (c, i) < modulus c) + (R Q : C → ℕ) (hR : ∀ c i, i < count c → cr.time (c, i) ≤ R c) + (hQ : ∀ c i, i < count c → cr.space (c, i) ≤ Q c) : + ∃ a d : ℕ, ComputableInO (modSum r modulus count) encC encNat + (fun c => (count c + 1) * (a * ((encC c).length + 1) ^ d + R c)) + (fun c => a * ((encC c).length + 1) ^ d + Q c) := by + -- The polynomial-time pieces of a round. + have htest : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => decide (p.1 < count p.2.1)) + (encPair encNat (encPair encC encNat)) encBool := by fun_prop + have hctx : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2.1) + (encPair encNat (encPair encC encNat)) encC := by fun_prop + have hacc : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2.2) + (encPair encNat (encPair encC encNat)) encNat := by fun_prop + have hswap : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => (p.2.1, p.1)) + (encPair encNat (encPair encC encNat)) (encPair encC encNat) := by fun_prop + have hmod : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => modulus p.2.1) + (encPair encNat (encPair encC encNat)) encNat := by fun_prop + have hno : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2) + (encPair encNat (encPair encC encNat)) (encPair encC encNat) := by fun_prop + have hadd : ComputableInPolyTime (fun q : ℕ × ℕ × ℕ => (q.1 + q.2.1) % q.2.2) + (encPair encNat (encPair encNat encNat)) encNat := by fun_prop + have hinit : ComputableInPolyTime (fun c : C => (c, 0)) encC (encPair encC encNat) := by + fun_prop + -- The round: a test, then either the addition or nothing. + let yes : NativeCertificate + (fun p : ℕ × (C × ℕ) => (p.2.1, (p.2.2 + r (p.2.1, p.1)) % modulus p.2.1)) + (encPair encNat (encPair encC encNat)) (encPair encC encNat) := + (NativeCertificate.ofPolyTime hctx).prod + ((NativeCertificate.ofPolyTime hadd).comp + ((NativeCertificate.ofPolyTime hacc).prod + ((cr.comp (NativeCertificate.ofPolyTime hswap)).prod + (NativeCertificate.ofPolyTime hmod)))) + let cstep : NativeCertificate (modSumStep r modulus count) + (encPair encNat (encPair encC encNat)) (encPair encC encNat) := + (NativeCertificate.branch (NativeCertificate.ofPolyTime htest) yes + (NativeCertificate.ofPolyTime hno)).congr fun p => by + simp only [modSumStep, decide_eq_true_eq] + -- Monotone polynomial bounds of the pieces. + obtain ⟨pT, hpT, mT, bT⟩ := exists_mono_poly_cert htest + obtain ⟨pC, hpC, mC, bC⟩ := exists_mono_poly_cert hctx + obtain ⟨pA, hpA, mA, bA⟩ := exists_mono_poly_cert hacc + obtain ⟨pW, hpW, mW, bW⟩ := exists_mono_poly_cert hswap + obtain ⟨pM, hpM, mM, bM⟩ := exists_mono_poly_cert hmod + obtain ⟨pN, hpN, mN, bN⟩ := exists_mono_poly_cert hno + obtain ⟨pD, hpD, mD, bD⟩ := exists_mono_poly_cert hadd + obtain ⟨pI, hpI, -, bI⟩ := exists_mono_poly_cert hinit + obtain ⟨pK, hpK, -, bK⟩ := exists_mono_poly_cert hcount + -- Sizes: the context, the modulus and the number of terms. + set L : C → ℕ := fun c => (encC c).length with hL + set lm : C → ℕ := fun c => (encNat (modulus c)).length with hlm + set lk : C → ℕ := fun c => (encNat (count c)).length with hlk + have hLp : PolyBounded L L := PolyBounded.self + have hlmp : PolyBounded L lm := hmodulus.polyBounded_length + have hlkp : PolyBounded L lk := hcount.polyBounded_length + -- A state `(j, (c, acc))` with `j ≤ count c` and `acc < modulus c` has length at most `S c`; the + -- input of the addition has length at most `S' c`; the accumulator pair at most `B c`. + let S : C → ℕ := fun c => 2 * lk c + 2 * L c + lm c + 2 + let S' : C → ℕ := fun c => 5 * lm c + 2 + let B : C → ℕ := fun c => 2 * L c + 1 + lm c + let U : C → ℕ := fun c => pT (S c) + pC (S c) + pA (S c) + pW (S c) + pM (S c) + pD (S' c) + + pN (S c) + have hstate (c : C) (j : ℕ) (hj : j ≤ count c) : + (encPair encNat (encPair encC encNat) + (IndexFold.run (modSumStep r modulus count) j (c, 0))).length ≤ S c := by + rw [run_modSumStep hj] + have hacc := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le + have hj' := length_encNat_mono hj + simp only [length_encPair, S, L, lm, lk] at hacc hj' ⊢ + omega + have hround_time (c : C) (j : ℕ) (hj : j ≤ count c) : + cstep.time (IndexFold.run (modSumStep r modulus count) j (c, 0)) ≤ U c + R c := by + have hs := hstate c j hj + rw [run_modSumStep hj] at hs ⊢ + set acc := (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0 + simp only [cstep, yes, NativeCertificate.congr, NativeCertificate.branch_time, + NativeCertificate.prod_time, NativeCertificate.comp_time, Function.comp_apply] + have h1 := (bT (j, (c, acc))).1.trans (mT hs) + split_ifs with hlt + · have hjc : j < count c := of_decide_eq_true hlt + have hacc_lt : acc < modulus c := foldl_add_mod_lt (hpos c) j + have hrj := hr c j hjc + have hq : (encPair encNat (encPair encNat encNat) + (acc, r (c, j), modulus c)).length ≤ S' c := by + have := length_encNat_mono hacc_lt.le + have := length_encNat_mono hrj.le + simp only [length_encPair, S', lm] at * + omega + have h2 := (bC (j, (c, acc))).1.trans (mC hs) + have h3 := (bA (j, (c, acc))).1.trans (mA hs) + have h4 := (bW (j, (c, acc))).1.trans (mW hs) + have h5 := (bM (j, (c, acc))).1.trans (mM hs) + have h6 := (bD (acc, r (c, j), modulus c)).1.trans (mD hq) + have h7 := hR c j hjc + simp only [U] + omega + · have h2 := (bN (j, (c, acc))).1.trans (mN hs) + simp only [U] + omega + have hround_space (c : C) (j : ℕ) (hj : j ≤ count c) : + cstep.space (IndexFold.run (modSumStep r modulus count) j (c, 0)) ≤ U c + Q c := by + have hs := hstate c j hj + rw [run_modSumStep hj] at hs ⊢ + set acc := (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0 + simp only [cstep, yes, NativeCertificate.congr, NativeCertificate.branch_space, + NativeCertificate.prod_space, NativeCertificate.comp_space, Function.comp_apply] + have h1 := (bT (j, (c, acc))).2.trans (mT hs) + split_ifs with hlt + · have hjc : j < count c := of_decide_eq_true hlt + have hacc_lt : acc < modulus c := foldl_add_mod_lt (hpos c) j + have hrj := hr c j hjc + have hq : (encPair encNat (encPair encNat encNat) + (acc, r (c, j), modulus c)).length ≤ S' c := by + have := length_encNat_mono hacc_lt.le + have := length_encNat_mono hrj.le + simp only [length_encPair, S', lm] at * + omega + have h2 := (bC (j, (c, acc))).2.trans (mC hs) + have h3 := (bA (j, (c, acc))).2.trans (mA hs) + have h4 := (bW (j, (c, acc))).2.trans (mW hs) + have h5 := (bM (j, (c, acc))).2.trans (mM hs) + have h6 := (bD (acc, r (c, j), modulus c)).2.trans (mD hq) + have h7 := hQ c j hjc + simp only [U] + omega + · have h2 := (bN (j, (c, acc))).2.trans (mN hs) + simp only [U] + omega + have hacc_len (c : C) (j : ℕ) (hj : j ≤ count c) : + (encPair encC encNat (IndexFold.run (modSumStep r modulus count) j (c, 0)).2).length ≤ + B c := by + rw [run_modSumStep hj] + have := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le + simp only [length_encPair, B, L, lm] at this ⊢ + omega + have hrun := IndexFold.computableInO (NativeCertificate.ofPolyTime hcount) + (NativeCertificate.ofPolyTime hinit) cstep (fun c => U c + R c) (fun c => U c + Q c) B + hround_time hround_space hacc_len + have hout := (ComputableInO.snd encC encNat).comp_linear + ((ComputableInO.snd encNat (encPair encC encNat)).comp_linear hrun) + -- Collect the polynomial overhead. + let V : C → ℕ := fun c => pK (L c) + (L c + pI (L c)) + 2 * (2 * lk c + 1 + B c) + + 2 * (lk c + 1) ^ 2 + (lk c + 1) + lk c + U c + have hSp : PolyBounded L S := + ((((PolyBounded.const 2).mul hlkp).add ((PolyBounded.const 2).mul hLp)).add hlmp).add + (PolyBounded.const 2) + have hS'p : PolyBounded L S' := ((PolyBounded.const 5).mul hlmp).add (PolyBounded.const 2) + have hBp : PolyBounded L B := + ((((PolyBounded.const 2).mul hLp).add (PolyBounded.const 1))).add hlmp + have hUp : PolyBounded L U := + ((((((polyBounded_comp_poly hpT hSp).add (polyBounded_comp_poly hpC hSp)).add + (polyBounded_comp_poly hpA hSp)).add (polyBounded_comp_poly hpW hSp)).add + (polyBounded_comp_poly hpM hSp)).add (polyBounded_comp_poly hpD hS'p)).add + (polyBounded_comp_poly hpN hSp) + have hVp : PolyBounded L V := + ((((((polyBounded_comp_poly hpK hLp).add (hLp.add (polyBounded_comp_poly hpI hLp))).add + ((PolyBounded.const 2).mul ((((PolyBounded.const 2).mul hlkp).add + (PolyBounded.const 1)).add hBp))).add + ((PolyBounded.const 2).mul ((hlkp.add (PolyBounded.const 1)).pow 2))).add + (hlkp.add (PolyBounded.const 1))).add hlkp).add hUp + obtain ⟨a, d, hV⟩ := hVp.exists_le + refine ⟨a, d, (hout.mono_le (fun c => ?_) fun c => ?_).of_enc_eq fun c => rfl⟩ + · have hK := (bK c).1 + have hI := (bI c).1 + have hVc := hV c + have hone : 1 ≤ count c + 1 := by omega + have hmul : V c + R c ≤ (count c + 1) * (V c + R c) := Nat.le_mul_of_pos_left _ hone + have hmono : (count c + 1) * (V c + R c) ≤ (count c + 1) * (a * (L c + 1) ^ d + R c) := + Nat.mul_le_mul_left _ (by omega) + simp only [V, L, lk] at hK hI hVc hmul hmono ⊢ + nlinarith + · have hK := (bK c).2 + have hI := (bI c).2 + have hVc := hV c + simp only [V, L, lk] at hK hI hVc ⊢ + omega + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean new file mode 100644 index 0000000000..6411651625 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean @@ -0,0 +1,464 @@ +/- +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.CountingSimulation.Accumulate +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces +public import Complexity.Computability.Complexity.Classes.Constructible +public import Complexity.Foundations.Data.Nat.SqrtLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith + +/-! +# The deterministic counting simulation, assembled from its interfaces + +This module assembles the deterministic simulation of #1833 from the two interfaces of +`Cslib.Complexity.CountingSimulation.NetworkFamily` and +`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`. **It is conditional**: every result +here assumes a network family and a contraction algorithm, which are proved separately. + +On an input `x` with clock `t`, the simulation (`Cslib.Complexity.CountingSimulation.simulate`) +visits the `scheduleCount heads t` movement schedules one at a time, contracts the network of each +modulo `2 ^ (paddedTime t + 1)`, and adds the residues modulo the same power of two +(`Cslib.Complexity.CountingSimulation.modSum`). Since the count is at most `2 ^ (paddedTime t)`, +the residue of the sum is the count itself (`Cslib.Complexity.CountingSimulation.simulate_eq`). + +Its cost is the number of schedules times the cost of one network, and its workspace that of one +network and an accumulator (`Cslib.Complexity.CountingSimulation.exists_computableInO_simulate`). +With the clock `t = c * T n` of a time-constructible `T n ≥ max n 2`, the schedules number +`3 ^ O(T / log T)`, so the total time is `2 ^ O(T / √(log T))` in the natural-number scale of +`Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`, and the space is polynomial in `T` +(`Cslib.Complexity.CountingSimulation.exists_computableInO_count`). The result may be any +polynomial-time function of the padded time and the count, such as a comparison deciding +acceptance. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.scheduleResidue`: the contraction of the network of one + schedule, modulo `2 ^ (paddedTime t + 1)`. +* `Cslib.Complexity.CountingSimulation.simulate`: the streamed sum of these residues. + +## Main results + +* `Cslib.Complexity.CountingSimulation.simulate_eq`: the simulation computes the count. +* `Cslib.Complexity.CountingSimulation.exists_computableInO_simulate`: its time and space bounds in + terms of the clock. +* `Cslib.Complexity.CountingSimulation.exists_computableInO_count`: from a time-constructible bound, + the count at the padded clock, or any polynomial-time function of it and the padded time, within + time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`. +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM Cslib.GenericRAM + +variable {N : Type} {encN : N ↪ List Bool} {value : N → ℕ} {Admissible : ℕ → ℕ → N → Prop} + {count : List Bool → ℕ → ℕ} + +/-! ### The algorithm and its correctness -/ + +/-- The value of the network of the schedule `p.2` for the input `p.1.1` and the clock `p.1.2`, +modulo `2 ^ (paddedTime p.1.2 + 1)`. -/ +def scheduleResidue (F : NetworkFamily encN value Admissible count) (p : (List Bool × ℕ) × ℕ) : + ℕ := + value (F.net (p.1.1, p.1.2, p.2)) % 2 ^ (paddedTime p.1.2 + 1) + +/-- **The simulation** on the input `p.1` with the clock `p.2`: when `|p.1| ≤ p.2` and `2 ≤ p.2`, +the residues of the networks of all schedules, summed one at a time modulo +`2 ^ (paddedTime p.2 + 1)`; otherwise `0`. -/ +def simulate (F : NetworkFamily encN value Admissible count) (p : List Bool × ℕ) : ℕ := + if p.1.length ≤ p.2 ∧ 2 ≤ p.2 then + modSum (scheduleResidue F) (fun p => 2 ^ (paddedTime p.2 + 1)) + (fun p => scheduleCount F.heads p.2) p + else 0 + +/-- **The simulation computes the count**: when `|x| ≤ t` and `2 ≤ t`, and the count at the padded +time is at most `2 ^ paddedTime t`, the residue of the sum of the network values modulo +`2 ^ (paddedTime t + 1)` is the count itself. -/ +theorem simulate_eq (F : NetworkFamily encN value Admissible count) {x : List Bool} {t : ℕ} + (hx : x.length ≤ t) (ht : 2 ≤ t) (hcount : count x (paddedTime t) ≤ 2 ^ paddedTime t) : + simulate F (x, t) = count x (paddedTime t) := by + rw [simulate, ite_eq_left_of_eq_true _ _ (eq_true (⟨hx, ht⟩ : x.length ≤ t ∧ 2 ≤ t)), + modSum_eq_sum_mod] + simp only [scheduleResidue] + rw [← Finset.sum_nat_mod, F.sum_value x t hx ht] + exact Nat.mod_eq_of_lt (hcount.trans_lt (Nat.pow_lt_pow_right one_lt_two (Nat.lt_succ_self _))) + +/-! ### Polynomial-time parameters -/ + +private theorem paddedTime_eq (t : ℕ) : + paddedTime t = (t + Nat.clog 2 (t + 2) - 1) / Nat.clog 2 (t + 2) * Nat.clog 2 (t + 2) := by + rw [paddedTime, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div] + +private theorem computableInPolyTime_paddedTime_succ : + ComputableInPolyTime (fun t => paddedTime t + 1) encUnary encNat := by + simp only [paddedTime_eq] + fun_prop + +private theorem computableInPolyTime_paddedTime : + ComputableInPolyTime paddedTime encUnary encNat := by + rw [show paddedTime = _ from funext paddedTime_eq] + fun_prop + +private theorem computableInPolyTime_two_pow_paddedTime : + ComputableInPolyTime (fun t => 2 ^ (paddedTime t + 1)) encUnary encNat := by + simp only [paddedTime_eq] + fun_prop + +private theorem computableInPolyTime_scheduleCount (heads : ℕ) : + ComputableInPolyTime (scheduleCount heads) encUnary encNat := by + have h : ComputableInPolyTime + (fun t => 3 ^ (heads * ((t + Nat.clog 2 (t + 2) - 1) / Nat.clog 2 (t + 2)))) encUnary + encNat := + ComputableInPolyTime.binary_pow' (ComputableInPolyTime.const (encOut := encNat) 3) (by fun_prop) + convert h using 2 with t + rw [scheduleCount, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div] + +/-! ### Resource bounds -/ + +/-- **Time and space of the simulation** (conditional on the interfaces). For a constant `k`, the +simulation on an input `x` with clock `t` runs within time +`k * (|x| + t + 1) ^ k * scheduleCount heads t * 2 ^ (k * t / √⌊log₂ t⌋)` and space +`k * (|x| + t + 1) ^ k`: it contracts one network per schedule, keeping one network, its +contraction workspace and an accumulator. -/ +theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible count) + (A : ContractionAlgorithm encN value Admissible) : + ∃ k : ℕ, ComputableInO (simulate F) (encPair encBits encUnary) encNat + (fun p => k * (p.1.length + p.2 + 1) ^ k * scheduleCount F.heads p.2 * + 2 ^ (k * p.2 / Nat.sqrt (Nat.log 2 p.2))) + (fun p => k * (p.1.length + p.2 + 1) ^ k) := by + classical + -- The polynomial-time pieces. + have hP : ComputableInPolyTime (fun p : (List Bool × ℕ) × ℕ => paddedTime p.1.2 + 1) + (encPair (encPair encBits encUnary) encNat) encNat := + computableInPolyTime_paddedTime_succ.comp (by fun_prop) + have hPc : ComputableInPolyTime (fun p : List Bool × ℕ => paddedTime p.2 + 1) + (encPair encBits encUnary) encNat := + computableInPolyTime_paddedTime_succ.comp (by fun_prop) + have hnet : ComputableInPolyTime (fun p : (List Bool × ℕ) × ℕ => F.net (p.1.1, p.1.2, p.2)) + (encPair (encPair encBits encUnary) encNat) encN := + F.polyTime.comp (by fun_prop) + have hmod : ComputableInPolyTime (fun p : List Bool × ℕ => 2 ^ (paddedTime p.2 + 1)) + (encPair encBits encUnary) encNat := + computableInPolyTime_two_pow_paddedTime.comp (by fun_prop) + have hcnt : ComputableInPolyTime (fun p : List Bool × ℕ => scheduleCount F.heads p.2) + (encPair encBits encUnary) encNat := + (computableInPolyTime_scheduleCount F.heads).comp (by fun_prop) + have hguard : ComputableInPolyTime + (fun p : List Bool × ℕ => decide (p.1.length ≤ p.2 ∧ 2 ≤ p.2)) + (encPair encBits encUnary) encBool := by fun_prop + -- The residue of one schedule: the contraction of its network at the precision. + let cr : NativeCertificate (scheduleResidue F) (encPair (encPair encBits encUnary) encNat) + encNat := + A.certificate.comp ((NativeCertificate.ofPolyTime hP).prod (NativeCertificate.ofPolyTime hnet)) + let R : List Bool × ℕ → ℕ := fun c => + (Finset.range (scheduleCount F.heads c.2)).sup fun i => cr.time (c, i) + let Q : List Bool × ℕ → ℕ := fun c => + (Finset.range (scheduleCount F.heads c.2)).sup fun i => cr.space (c, i) + obtain ⟨a, d, hms⟩ := exists_computableInO_modSum hmod hcnt cr (fun _ => by positivity) + (fun c i _ => Nat.mod_lt _ (by positivity)) R Q + (fun c i hi => Finset.le_sup (f := fun i => cr.time (c, i)) (Finset.mem_range.mpr hi)) + (fun c i hi => Finset.le_sup (f := fun i => cr.space (c, i)) (Finset.mem_range.mpr hi)) + let cms : NativeCertificate (modSum (scheduleResidue F) (fun p => 2 ^ (paddedTime p.2 + 1)) + (fun p => scheduleCount F.heads p.2)) (encPair encBits encUnary) encNat := ⟨_, _, hms⟩ + let csim : NativeCertificate (simulate F) (encPair encBits encUnary) encNat := + (NativeCertificate.branch (NativeCertificate.ofPolyTime hguard) cms + (NativeCertificate.const 0)).congr fun p => by simp only [simulate, decide_eq_true_eq] + -- Bounds on the pieces. + obtain ⟨K, hK⟩ := A.bound F.constant 2 + obtain ⟨pP, hpP, mP, bP⟩ := exists_mono_poly_cert hP + obtain ⟨pN, hpN, mN, bN⟩ := exists_mono_poly_cert hnet + obtain ⟨pG, hpG, -, bG⟩ := exists_mono_poly_cert hguard + obtain ⟨an, dn, hnl⟩ := hnet.polyBounded_length.exists_le + set sz : List Bool × ℕ → ℕ := fun c => (encPair encBits encUnary c).length with hsz + let Z : List Bool × ℕ → ℕ := fun c => 2 * sz c + 1 + (encNat (scheduleCount F.heads c.2)).length + let Y : List Bool × ℕ → ℕ := fun c => + 2 * (encNat (paddedTime c.2 + 1)).length + 1 + an * (Z c + 1) ^ dn + let U : List Bool × ℕ → ℕ := fun c => pP (Z c) + pN (Z c) + K * (Y c + 1) ^ K + let E : List Bool × ℕ → ℕ := fun c => 2 ^ (K * c.2 / Nat.sqrt (Nat.log 2 c.2)) + have hE (c : List Bool × ℕ) : 1 ≤ E c := Nat.one_le_two_pow + have hcnt1 (c : List Bool × ℕ) : 1 ≤ scheduleCount F.heads c.2 := Nat.one_le_pow _ _ (by norm_num) + -- One schedule at a good context. + have hone (c : List Bool × ℕ) (hc : c.1.length ≤ c.2 ∧ 2 ≤ c.2) (i : ℕ) + (hi : i < scheduleCount F.heads c.2) : + cr.time (c, i) ≤ U c * E c ∧ cr.space (c, i) ≤ U c := by + have hZ : (encPair (encPair encBits encUnary) encNat (c, i)).length ≤ Z c := by + have := (length_encNat_mono hi.le) + simp only [length_encPair, Z, sz] at this ⊢ + omega + have hG : (encN (F.net (c.1, c.2, i))).length ≤ + an * ((encPair (encPair encBits encUnary) encNat (c, i)).length + 1) ^ dn := hnl (c, i) + have hY : (encPair encNat encN (paddedTime c.2 + 1, F.net (c.1, c.2, i))).length ≤ Y c := by + have hG' := hG.trans + (Nat.mul_le_mul_left an (Nat.pow_le_pow_left (Nat.add_le_add_right hZ 1) dn)) + rw [length_encPair] + simp only [Y] + omega + have hA := hK c.2 (paddedTime c.2 + 1) (F.net (c.1, c.2, i)) hc.2 (by omega) + (paddedTime_add_one_le hc.2) (F.admissible c.1 c.2 i hc.1 hc.2 hi) + have hKY := Nat.mul_le_mul_left K (Nat.pow_le_pow_left (Nat.add_le_add_right hY 1) K) + have h1 := (bP (c, i)).1.trans (mP hZ) + have h2 := (bN (c, i)).1.trans (mN hZ) + have h3 := (bP (c, i)).2.trans (mP hZ) + have h4 := (bN (c, i)).2.trans (mN hZ) + have hEc := hE c + simp only [cr, NativeCertificate.comp_time, NativeCertificate.comp_space, + NativeCertificate.prod_time, NativeCertificate.prod_space] + constructor + · have hmul : K * ((encPair encNat encN (paddedTime c.2 + 1, F.net (c.1, c.2, i))).length + + 1) ^ K * E c ≤ K * (Y c + 1) ^ K * E c := Nat.mul_le_mul_right _ hKY + have hpe : pP (Z c) + pN (Z c) ≤ (pP (Z c) + pN (Z c)) * E c := Nat.le_mul_of_pos_right _ hEc + simp only [U, E] at hA hmul hpe ⊢ + nlinarith [hA.1] + · simp only [U] at hA ⊢ + omega + -- Collect the polynomial overhead. + let V : List Bool × ℕ → ℕ := fun c => pG (sz c) + sz c + 2 * (a * (sz c + 1) ^ d + U c) + have hszp : PolyBounded sz sz := PolyBounded.self + have hcntp : PolyBounded sz fun c => (encNat (scheduleCount F.heads c.2)).length := + hcnt.polyBounded_length + have hPcp : PolyBounded sz fun c => (encNat (paddedTime c.2 + 1)).length := hPc.polyBounded_length + have hZp : PolyBounded sz Z := + (((PolyBounded.const 2).mul hszp).add (PolyBounded.const 1)).add hcntp + have hYp : PolyBounded sz Y := + ((((PolyBounded.const 2).mul hPcp).add (PolyBounded.const 1))).add + ((PolyBounded.const an).mul ((hZp.add (PolyBounded.const 1)).pow dn)) + have hUp : PolyBounded sz U := + (((PolyBounded.of_polynomiallyBounded id hpP).comp hZp).add + ((PolyBounded.of_polynomiallyBounded id hpN).comp hZp)).add + ((PolyBounded.const K).mul ((hYp.add (PolyBounded.const 1)).pow K)) + have hVp : PolyBounded sz V := + (((PolyBounded.of_polynomiallyBounded id hpG).comp hszp).add hszp).add + ((PolyBounded.const 2).mul (((PolyBounded.const a).mul + ((hszp.add (PolyBounded.const 1)).pow d)).add hUp)) + obtain ⟨k₀, d₀, hV⟩ := hVp.exists_le + -- The simulation's time and space. + have htime (c : List Bool × ℕ) : + csim.time c ≤ V c * scheduleCount F.heads c.2 * E c := by + have hG := (bG c).1 + have hVc : pG (sz c) + sz c + 2 * (a * (sz c + 1) ^ d + U c) = V c := rfl + have hcE : 1 ≤ scheduleCount F.heads c.2 * E c := Nat.one_le_iff_ne_zero.mpr + (Nat.mul_ne_zero (by have := hcnt1 c; omega) (by have := hE c; omega)) + simp only [csim, cms, NativeCertificate.congr, NativeCertificate.branch_time, + NativeCertificate.const_time] + split_ifs with hc + · have hc' : c.1.length ≤ c.2 ∧ 2 ≤ c.2 := of_decide_eq_true hc + have hR : R c ≤ U c * E c := + Finset.sup_le fun i hi => (hone c hc' i (Finset.mem_range.mp hi)).1 + have h1 : (scheduleCount F.heads c.2 + 1) * (a * (sz c + 1) ^ d + R c) ≤ + 2 * (a * (sz c + 1) ^ d + U c) * (scheduleCount F.heads c.2 * E c) := by + have hAE : a * (sz c + 1) ^ d ≤ a * (sz c + 1) ^ d * E c := Nat.le_mul_of_pos_right _ (hE c) + calc _ ≤ (scheduleCount F.heads c.2 + 1) * (a * (sz c + 1) ^ d + U c * E c) := + Nat.mul_le_mul_left _ (by omega) + _ ≤ (2 * scheduleCount F.heads c.2) * ((a * (sz c + 1) ^ d + U c) * E c) := + Nat.mul_le_mul (by have := hcnt1 c; omega) + ((Nat.add_le_add_right hAE (U c * E c)).trans_eq (Nat.add_mul _ _ _).symm) + _ = _ := by ring + have h2 : pG (sz c) ≤ pG (sz c) * (scheduleCount F.heads c.2 * E c) := + Nat.le_mul_of_pos_right _ hcE + calc _ ≤ pG (sz c) * (scheduleCount F.heads c.2 * E c) + + 2 * (a * (sz c + 1) ^ d + U c) * (scheduleCount F.heads c.2 * E c) := by + simp only [sz] at hG h1 h2 ⊢ + omega + _ ≤ V c * (scheduleCount F.heads c.2 * E c) := by + rw [← hVc, ← Nat.add_mul] + exact Nat.mul_le_mul_right _ (by omega) + _ = _ := by ring + · have h2 : pG (sz c) + sz c ≤ (pG (sz c) + sz c) * (scheduleCount F.heads c.2 * E c) := + Nat.le_mul_of_pos_right _ hcE + calc _ ≤ (pG (sz c) + sz c) * (scheduleCount F.heads c.2 * E c) := by + simp only [sz] at hG h2 ⊢ + omega + _ ≤ V c * (scheduleCount F.heads c.2 * E c) := Nat.mul_le_mul_right _ (by omega) + _ = _ := by ring + have hspace (c : List Bool × ℕ) : csim.space c ≤ V c := by + have hG := (bG c).2 + simp only [csim, cms, NativeCertificate.congr, NativeCertificate.branch_space, + NativeCertificate.const_space] + split_ifs with hc + · have hc' : c.1.length ≤ c.2 ∧ 2 ≤ c.2 := of_decide_eq_true hc + have hQ : Q c ≤ U c := Finset.sup_le fun i hi => (hone c hc' i (Finset.mem_range.mp hi)).2 + simp only [V, sz] at hG hQ ⊢ + omega + · simp only [V, sz] at hG ⊢ + omega + -- Absorb the constants. + set k := k₀ * 2 ^ d₀ + d₀ + K with hk + have hVk (c : List Bool × ℕ) : V c ≤ k * (c.1.length + c.2 + 1) ^ k := by + have hszc : sz c + 1 ≤ 2 * (c.1.length + c.2 + 1) := by + simp only [sz, length_encPair, encBits_apply, encUnary_apply, List.length_replicate] + omega + calc V c ≤ k₀ * (sz c + 1) ^ d₀ := hV c + _ ≤ k₀ * (2 * (c.1.length + c.2 + 1)) ^ d₀ := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hszc _) + _ = k₀ * 2 ^ d₀ * (c.1.length + c.2 + 1) ^ d₀ := by rw [mul_pow, mul_assoc] + _ ≤ k * (c.1.length + c.2 + 1) ^ k := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + refine ⟨k, csim.computes.mono_le (fun c => ?_) fun c => (hspace c).trans (hVk c)⟩ + have hEk : E c ≤ 2 ^ (k * c.2 / Nat.sqrt (Nat.log 2 c.2)) := + Nat.pow_le_pow_right (by norm_num) + (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega))) + exact (htime c).trans (Nat.mul_le_mul (Nat.mul_le_mul_right _ (hVk c)) hEk) + +/-- **The count within time `2 ^ O(T / √(log T))` and polynomial space** (conditional on the +interfaces). Let `T` be time-constructible with `max n 2 ≤ T n`, let `c ≥ 1`, and let `rule` be a +polynomial-time function of a padded time and a count. Given a network family for `count`, with +`count x τ ≤ 2 ^ τ`, and a contraction algorithm, the function sending `x` to `rule` of the padded +clock `τ = paddedTime (c * T |x|)` and of `count x τ` is computable within time +`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d` on inputs of length `n`, for constants `C` and +`d`. -/ +theorem exists_computableInO_count (F : NetworkFamily encN value Admissible count) + (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ) + {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c) + {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β} + (hrule : ComputableInPolyTime rule (encPair encNat encNat) encβ) : + ∃ C d : ℕ, ComputableInO + (fun x : List Bool => + rule (paddedTime (c * T x.length), count x (paddedTime (c * T x.length)))) + encBits encβ + (fun x => 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length)))) + (fun x => T x.length ^ d) := by + obtain ⟨k, hsim⟩ := exists_computableInO_simulate F A + -- Preparing the context `(x, c * T |x|)`, with the clock in unary. + have hmul : ComputableInPolyTime (fun n : ℕ => c * n) encUnary encUnary := by fun_prop + have htau : ComputableInPolyTime (fun p : List Bool × ℕ => paddedTime p.2) + (encPair encBits encUnary) encNat := computableInPolyTime_paddedTime.comp (by fun_prop) + let cT : NativeCertificate (fun x : List Bool => T x.length) encBits encNat := + ⟨_, _, hT.computableInO⟩ + let cU : NativeCertificate (fun n : ℕ => n) encNat encUnary := ⟨_, _, ComputableInO.natToUnary⟩ + let cX : NativeCertificate (fun x : List Bool => x) encBits encBits := + NativeCertificate.linear (ComputableInO.of_eq fun _ => rfl) + let cpre : NativeCertificate (fun x : List Bool => (x, c * T x.length)) encBits + (encPair encBits encUnary) := + cX.prod ((NativeCertificate.ofPolyTime hmul).comp (cU.comp cT)) + let csim : NativeCertificate (simulate F) (encPair encBits encUnary) encNat := ⟨_, _, hsim⟩ + let ctotal := (NativeCertificate.ofPolyTime hrule).comp + (((NativeCertificate.ofPolyTime htau).prod csim).comp cpre) + -- Monotone polynomial bounds of the polynomial-time pieces. + obtain ⟨pm, hpm, mm, bm⟩ := exists_mono_poly_cert hmul + obtain ⟨pt, hpt, mt, bt⟩ := exists_mono_poly_cert htau + obtain ⟨pr, hpr, mr, br⟩ := exists_mono_poly_cert hrule + let W : ℕ → ℕ := fun n => 2 * n + (n + 1) ^ 2 + pm n + pt (3 * n + 1) + pr (6 * n + 3) + + k * (2 * n + 1) ^ k + (n + n + pm n) + have hW : Cslib.PolynomiallyBounded W := by fun_prop + obtain ⟨a, e, hWa⟩ := Cslib.polynomiallyBounded_iff_le.mp hW + -- The cost at an input, in terms of the clock `t = c * T |x|`. + have hcost (x : List Bool) : + ctotal.time x ≤ W (c * T x.length) * scheduleCount F.heads (c * T x.length) * + 2 ^ (k * (c * T x.length) / Nat.sqrt (Nat.log 2 (c * T x.length))) ∧ + ctotal.space x ≤ W (c * T x.length) := by + simp only [ctotal, cpre, csim, cX, cT, cU, NativeCertificate.comp_time, + NativeCertificate.comp_space, NativeCertificate.prod_time, NativeCertificate.prod_space, + NativeCertificate.linear_time, NativeCertificate.linear_space, encBits_apply, + Function.comp_apply] + set n := x.length + set t := c * T n with ht + have hnT : n ≤ T n := (le_max_left _ _).trans (hTn n) + have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n) + have hTt : T n ≤ t := Nat.le_mul_of_pos_left _ hc + have hnt : n ≤ t := hnT.trans hTt + have h2t : 2 ≤ t := h2T.trans hTt + have hτ := paddedTime_add_one_le h2t + have hcnt1 : 1 ≤ scheduleCount F.heads t := Nat.one_le_pow _ _ (by norm_num) + have hE : 1 ≤ 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) := Nat.one_le_two_pow + have hctx : (encPair encBits encUnary (x, t)).length ≤ 3 * t + 1 := by + simp only [length_encPair, encBits_apply, encUnary_apply, List.length_replicate] + omega + have hsimx : simulate F (x, t) = count x (paddedTime t) := + simulate_eq F hnt h2t (hcount x _) + have hout : (encPair encNat encNat (paddedTime t, simulate F (x, t))).length ≤ 6 * t + 3 := by + have h1 : (encNat (paddedTime t)).length ≤ paddedTime t := by + rw [length_encNat_eq_size] + exact Nat.size_le.mpr Nat.lt_two_pow_self + have h2 : (encNat (simulate F (x, t))).length ≤ paddedTime t + 1 := by + rw [hsimx] + calc _ ≤ (encNat (2 ^ paddedTime t)).length := length_encNat_mono (hcount x _) + _ = paddedTime t + 1 := by rw [length_encNat_eq_size, Nat.size_pow] + simp only [length_encPair] + omega + have hTu : (encUnary (T n)).length ≤ t := by + simp only [encUnary_apply, List.length_replicate] + exact hTt + have hmT := (bm (T n)).1.trans (mm hTu) + have hmS := (bm (T n)).2.trans (mm hTu) + have htT := (bt (x, t)).1.trans (mt hctx) + have htS := (bt (x, t)).2.trans (mt hctx) + have hrT := (br (paddedTime t, simulate F (x, t))).1.trans (mr hout) + have hrS := (br (paddedTime t, simulate F (x, t))).2.trans (mr hout) + have hpow : k * (n + t + 1) ^ k ≤ k * (2 * t + 1) ^ k := + Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _) + have hsq : (T n + 1) ^ 2 ≤ (t + 1) ^ 2 := Nat.pow_le_pow_left (by omega) _ + constructor + · have hsimT : k * (n + t + 1) ^ k * scheduleCount F.heads t * + 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) ≤ + k * (2 * t + 1) ^ k * + (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by + rw [Nat.mul_assoc] + exact Nat.mul_le_mul_right _ hpow + have hrest : 2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3) ≤ + (2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3)) * + (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := + Nat.le_mul_of_pos_right _ (Nat.mul_pos hcnt1 hE) + have hWt : W t * scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) = + W t * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by ring + rw [hWt] + have hWle : (2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3)) * + (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) + + k * (2 * t + 1) ^ k * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) ≤ + W t * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by + rw [← Nat.add_mul] + exact Nat.mul_le_mul_right _ (by simp only [W]; omega) + omega + · simp only [W] + omega + -- Absorb the cost into `2 ^ O(T / √(log T))` and `T ^ O(1)`. + obtain ⟨C, hC⟩ := Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two F.heads c e k + refine ⟨(a + 0 + 1) * (C + 1), a * c ^ e + 0 + 2 * e, + (ctotal.computes.of_enc_eq fun x => congrArg encβ ?_).mono_le (fun x => ?_) fun x => ?_⟩ + · have hnt : x.length ≤ c * T x.length := + ((le_max_left _ _).trans (hTn _)).trans (Nat.le_mul_of_pos_left _ hc) + have h2t : 2 ≤ c * T x.length := + ((le_max_right _ _).trans (hTn _)).trans (Nat.le_mul_of_pos_left _ hc) + simp only [Function.comp_apply] + rw [simulate_eq F hnt h2t (hcount x _)] + · set n := x.length + have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n) + have hcostT := (hcost x).1 + have hWt := hWa (c * T n) + have hmain : 3 ^ (F.heads * (c * T n ⌈/⌉ Nat.clog 2 (c * T n + 2))) * (c * T n + 1) ^ e * + 2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) ≤ + 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := hC (T n) h2T + have habs := Nat.mul_two_pow_div_sqrt_log_two_add_le (a := a) (b := 0) (C := C) h2T + calc ctotal.time x ≤ W (c * T n) * scheduleCount F.heads (c * T n) * + 2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) := hcostT + _ ≤ a * (c * T n + 1) ^ e * scheduleCount F.heads (c * T n) * + 2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hWt) + _ = a * (3 ^ (F.heads * (c * T n ⌈/⌉ Nat.clog 2 (c * T n + 2))) * (c * T n + 1) ^ e * + 2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n)))) := by + simp only [scheduleCount, numBlocks, blockLength] + ring + _ ≤ a * 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) + 0 := by + rw [Nat.add_zero] + exact Nat.mul_le_mul_left _ hmain + _ ≤ _ := habs + · set n := x.length + have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n) + have hspace := (hcost x).2 + have hWt := hWa (c * T n) + have hct : c * T n + 1 ≤ c * (T n + 1) := by nlinarith + calc ctotal.space x ≤ a * (c * T n + 1) ^ e := hspace.trans hWt + _ ≤ a * (c * (T n + 1)) ^ e := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hct _) + _ = a * c ^ e * (T n + 1) ^ e + 0 := by rw [mul_pow, Nat.mul_assoc, add_zero] + _ ≤ T n ^ (a * c ^ e + 0 + 2 * e) := Nat.mul_add_one_pow_add_le_pow h2T + +end Cslib.Complexity.CountingSimulation diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean new file mode 100644 index 0000000000..d00a0135c0 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean @@ -0,0 +1,165 @@ +/- +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.GenericRAM.Native.Certificate +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public import Complexity.Foundations.Data.Nat.CeilDiv +public import Mathlib.Data.Nat.Log +public import Mathlib.Data.Nat.Sqrt +import Mathlib.Tactic.Linarith + +/-! +# Interfaces of the deterministic counting simulation + +The deterministic simulation of nondeterministic and probabilistic time by blocking and tensor +contraction (#1833) has two ingredients that are formalized separately. This module states them as +interfaces, so that the assembly (`Cslib.Complexity.CountingSimulation.exists_computableInO_count`) +can be proved from them, and each can be discharged on its own. + +**Parameters.** A run of `t` steps is cut into `numBlocks t = ⌈t / b⌉` intervals of +`blockLength t = b = ⌈log₂ (t + 2)⌉` steps and padded to `paddedTime t = numBlocks t * b ≥ t` +steps. Each of `heads` blocked heads moves by at most one block per interval, so a run has one of +at most `3 ^ (heads * numBlocks t)` movement schedules. + +**Networks** (`Cslib.Complexity.CountingSimulation.NetworkFamily`). A network for each input `x`, +clock `t` and schedule `σ`, built in polynomial time from `x`, `t` in unary and `σ` in binary, +whose values sum to the count being simulated at the padded time. Each network is admissible for +the contraction algorithm at size `t`, with a constant of the family. This is the block-counting +step of #1833 (milestone H3): blocking after Hopcroft, Paul and Valiant, with a Boolean tensor +network for each schedule whose contraction counts the accepting choice strings with that +schedule. It is new mathematics, not a cited result. + +**Contraction** (`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`). One native machine +that, given a precision `P` and a network `G`, outputs `value G % 2 ^ P`, and that, on networks +admissible at a size `s ≥ 2` with `1 ≤ P ≤ D * s`, runs within time +`K * (n + 1) ^ K * 2 ^ (K * s / √⌊log₂ s⌋)` and space `K * (n + 1) ^ K`, where `n` is the encoded +length of `(P, G)` and `K` depends only on the constants. This is the form in which the +simulation uses the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1] with `ℓ = 1` +and maximum degree `O(log s)` (milestone T2 of #1833), with the exponent in the natural-number +scale of `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`. Like Theorem D.1 it is +parameterized by a size `s` bounding the number of edges and the precision, rather than by the +number of edges itself. + +Both interfaces are generic in the representation of networks: their type `N`, its encoding, the +contracted `value : N → ℕ` and the admissibility predicate `Admissible C s G` are parameters. The +intended instance takes `N` to be an explicit Boolean tensor network with its bipartition, +`value` its contraction, and `Admissible C s G` to say that `G` is bipartite with at most `C * s` +edges and maximum degree at most `C * log₂ s`. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.blockLength`, `numBlocks`, `paddedTime`, `scheduleCount`: + the blocking parameters. +* `Cslib.Complexity.CountingSimulation.ContractionAlgorithm`: the contraction interface. +* `Cslib.Complexity.CountingSimulation.NetworkFamily`: the network interface. + +## Main results + +* `Cslib.Complexity.CountingSimulation.le_paddedTime`: padding never shortens a run. +* `Cslib.Complexity.CountingSimulation.paddedTime_add_one_le`: from `t = 2` on, the padded time + and one more fit in `2 * t`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (contraction). +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing.MultiTapeTM Cslib.GenericRAM + +/-! ### Blocking parameters -/ + +/-- The length `⌈log₂ (t + 2)⌉` of a time interval for a clock `t`. -/ +@[expose] def blockLength (t : ℕ) : ℕ := Nat.clog 2 (t + 2) + +/-- The number `⌈t / blockLength t⌉` of time intervals for a clock `t`. -/ +@[expose] def numBlocks (t : ℕ) : ℕ := t ⌈/⌉ blockLength t + +/-- The padded running time `numBlocks t * blockLength t`, a whole number of intervals. -/ +@[expose] def paddedTime (t : ℕ) : ℕ := numBlocks t * blockLength t + +/-- The number `3 ^ (heads * numBlocks t)` of movement schedules of `heads` blocked heads. -/ +@[expose] def scheduleCount (heads t : ℕ) : ℕ := 3 ^ (heads * numBlocks t) + +/-- An interval has at least one step. -/ +theorem one_le_blockLength (t : ℕ) : 1 ≤ blockLength t := + Nat.succ_le_of_lt (Nat.clog_pos one_lt_two (by omega)) + +/-- **Padding never shortens a run**: `t ≤ paddedTime t`. -/ +theorem le_paddedTime (t : ℕ) : t ≤ paddedTime t := + Nat.le_ceilDiv_mul (one_le_blockLength t) + +private theorem add_two_le_two_pow {t : ℕ} (ht : 2 ≤ t) : t + 2 ≤ 2 ^ t := by + induction t, ht using Nat.le_induction with + | base => norm_num + | succ n hn ih => rw [pow_succ]; omega + +/-- An interval is no longer than the clock, from `t = 2` on. -/ +theorem blockLength_le {t : ℕ} (ht : 2 ≤ t) : blockLength t ≤ t := + Nat.clog_le_of_le_pow (add_two_le_two_pow ht) + +/-- **The padded time stays linear**: from `t = 2` on, `paddedTime t + 1 ≤ 2 * t`, since padding +adds less than one interval. -/ +theorem paddedTime_add_one_le {t : ℕ} (ht : 2 ≤ t) : paddedTime t + 1 ≤ 2 * t := by + have h := Nat.ceilDiv_mul_lt (a := t) (one_le_blockLength t) + have := blockLength_le ht + unfold paddedTime numBlocks + omega + +/-! ### The interfaces -/ + +/-- **The contraction interface** (the Boolean tensor contraction theorem, as the simulation uses +it). One native certificate computes `value G % 2 ^ P` from the precision `P` in binary and the +network `G`. For all constants `C` and `D` there is `K` such that on every network admissible at a +size `s ≥ 2` with constant `C`, and every precision `1 ≤ P ≤ D * s`, the certificate's time is at +most `K * (n + 1) ^ K * 2 ^ (K * s / √⌊log₂ s⌋)` and its space at most `K * (n + 1) ^ K`, where `n` +is the encoded length of `(P, G)`. Outside admissible inputs the certificate need only be +correct. -/ +structure ContractionAlgorithm {N : Type} (encN : N ↪ List Bool) (value : N → ℕ) + (Admissible : ℕ → ℕ → N → Prop) where + /-- The native contraction modulo `2 ^ P`. -/ + certificate : NativeCertificate (fun p : ℕ × N => value p.2 % 2 ^ p.1) (encPair encNat encN) + encNat + /-- Its time and space on admissible inputs. -/ + bound : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P : ℕ) (G : N), 2 ≤ s → 1 ≤ P → P ≤ D * s → + Admissible C s G → + certificate.time (P, G) ≤ K * ((encPair encNat encN (P, G)).length + 1) ^ K * + 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧ + certificate.space (P, G) ≤ K * ((encPair encNat encN (P, G)).length + 1) ^ K + +/-- **The network interface** (the block-counting lemma, as the simulation uses it), for a count +`count x τ` of the inputs `x` at padded time `τ`, such as the number of accepting choice strings of +length `τ` of a fair-coin machine. The family has a number of blocked heads and an admissibility +constant. Its network for the input `x`, the clock `t` and the schedule `σ` is computable in +polynomial time from `x`, `t` in unary and `σ` in binary. Whenever `|x| ≤ t` and `2 ≤ t`, the +values of the networks of the `scheduleCount heads t` schedules sum to `count x (paddedTime t)`, +and each of these networks is admissible at size `t`. -/ +structure NetworkFamily {N : Type} (encN : N ↪ List Bool) (value : N → ℕ) + (Admissible : ℕ → ℕ → N → Prop) (count : List Bool → ℕ → ℕ) where + /-- The number of blocked heads. -/ + heads : ℕ + /-- The admissibility constant. -/ + constant : ℕ + /-- The network of an input, a clock and a schedule. -/ + net : List Bool × ℕ × ℕ → N + /-- The networks are built in polynomial time, with the clock in unary. -/ + polyTime : ComputableInPolyTime net (encPair encBits (encPair encUnary encNat)) encN + /-- **The counting identity**: the values of the networks of all schedules sum to the count at + the padded time. -/ + sum_value : ∀ x t, x.length ≤ t → 2 ≤ t → + ∑ σ ∈ Finset.range (scheduleCount heads t), value (net (x, t, σ)) = count x (paddedTime t) + /-- Every network of a schedule is admissible at size `t`. -/ + admissible : ∀ x t σ, x.length ≤ t → 2 ≤ t → σ < scheduleCount heads t → + Admissible constant t (net (x, t, σ)) + +end Cslib.Complexity.CountingSimulation diff --git a/ComplexityTests/CountingSimulation.lean b/ComplexityTests/CountingSimulation.lean new file mode 100644 index 0000000000..1d8d0d9958 --- /dev/null +++ b/ComplexityTests/CountingSimulation.lean @@ -0,0 +1,140 @@ +/- +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.CountingSimulation.Assembly +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div +import Mathlib.Data.Nat.Size + +/-! Checks for the conditional assembly of the counting simulation (#1833): the streamed modular +sum on concrete terms, the blocking parameters, and toy instances of both interfaces, which show +that the hypotheses of `Cslib.Complexity.CountingSimulation.exists_computableInO_count` can be met. + +The toy instances are deliberately trivial: a "network" is a natural number that is its own value, +the contraction reduces it modulo `2 ^ P`, every network is admissible, and the counted quantity +is `2 ^ τ`, the number of all choice strings of length `τ`, carried by the first of +`scheduleCount 1 t` schedules. They exercise the algorithm and its bounds, not the tensor +networks of the intended instance. -/ + +namespace ComplexityTests.CountingSimulation + +open Turing.MultiTapeTM Cslib.GenericRAM Cslib.Complexity.CountingSimulation + +/-! ### The streamed sum -/ + +/-- `0 + 1 + 2 + 3 = 6` below the modulus `7`. -/ +example : modSum (fun p : Unit × ℕ => p.2) (fun _ => 7) (fun _ => 4) () = 6 := by + rw [modSum_eq_sum_mod] + decide + +/-- The residue wraps around: `(0 + 1 + 2 + 3 + 4) % 4 = 2`. -/ +example : modSum (fun p : Unit × ℕ => p.2) (fun _ => 4) (fun _ => 5) () = 2 := by + rw [modSum_eq_sum_mod] + decide + +/-- With no terms the sum is zero, whatever the modulus. -/ +example : modSum (fun p : Unit × ℕ => p.2 + 1) (fun _ => 5) (fun _ => 0) () = 0 := by + rw [modSum_eq_sum_mod] + rfl + +/-! ### Blocking parameters -/ + +/-- With clock `6`, intervals of `⌈log₂ 8⌉ = 3` steps, two of them, and no padding. -/ +example : blockLength 6 = 3 ∧ numBlocks 6 = 2 ∧ paddedTime 6 = 6 := by + refine ⟨?_, ?_, ?_⟩ <;> decide + +/-- With clock `7`, intervals of `⌈log₂ 9⌉ = 4` steps, and one step of padding. -/ +example : blockLength 7 = 4 ∧ numBlocks 7 = 2 ∧ paddedTime 7 = 8 := by + refine ⟨?_, ?_, ?_⟩ <;> decide + +/-- Two blocked heads over two intervals have `3 ^ 4` movement schedules. -/ +example : scheduleCount 2 6 = 81 := by decide + +example : paddedTime 7 + 1 ≤ 2 * 7 := paddedTime_add_one_le (by norm_num) + +/-! ### A toy contraction algorithm -/ + +/-- Reducing modulo `2 ^ P` only needs the low `min (size n) P` bits. -/ +theorem mod_two_pow_min_size (n P : ℕ) : n % 2 ^ min (Nat.size n) P = n % 2 ^ P := by + rcases le_total (Nat.size n) P with h | h + · rw [min_eq_left h, Nat.mod_eq_of_lt (Nat.lt_size_self n), + Nat.mod_eq_of_lt ((Nat.lt_size_self n).trans_le (Nat.pow_le_pow_right two_pos h))] + · rw [min_eq_right h] + +theorem computableInPolyTime_mod_two_pow : + ComputableInPolyTime (fun p : ℕ × ℕ => p.2 % 2 ^ p.1) (encPair encNat encNat) encNat := by + have h : ComputableInPolyTime (fun p : ℕ × ℕ => p.2 % 2 ^ min (Nat.size p.2) p.1) + (encPair encNat encNat) encNat := by fun_prop + simpa only [mod_two_pow_min_size] using h + +/-- The contraction interface for networks that are their own values, all admissible: a +polynomial-time reduction modulo `2 ^ P` meets every bound. -/ +noncomputable def toyContraction : + ContractionAlgorithm encNat (fun n : ℕ => n) (fun _ _ _ => True) where + certificate := NativeCertificate.ofPolyTime computableInPolyTime_mod_two_pow + bound C D := by + obtain ⟨p, hp, -, hb⟩ := exists_mono_poly_cert computableInPolyTime_mod_two_pow + obtain ⟨a, d, hpa⟩ := Cslib.polynomiallyBounded_iff_le.mp hp + refine ⟨a + d, fun s P G _ _ _ _ => ?_⟩ + have hpow : a * ((encPair encNat encNat (P, G)).length + 1) ^ d ≤ + (a + d) * ((encPair encNat encNat (P, G)).length + 1) ^ (a + d) := + Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)) + have hE : 1 ≤ 2 ^ ((a + d) * s / Nat.sqrt (Nat.log 2 s)) := Nat.one_le_two_pow + have hT := (hb (P, G)).1.trans (hpa _) + have hS := (hb (P, G)).2.trans (hpa _) + exact ⟨hT.trans (hpow.trans (Nat.le_mul_of_pos_right _ hE)), hS.trans hpow⟩ + +/-! ### A toy network family -/ + +theorem computableInPolyTime_toyNet : + ComputableInPolyTime (fun p : List Bool × ℕ × ℕ => 2 ^ paddedTime p.2.1 * (1 - p.2.2)) + (encPair encBits (encPair encUnary encNat)) encNat := by + simp only [paddedTime, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div] + fun_prop + +/-- The count `2 ^ τ` of all choice strings of length `τ`, carried by the network of the first of +`scheduleCount 1 t` schedules; the others have value zero. -/ +noncomputable def toyFamily : + NetworkFamily encNat (fun n : ℕ => n) (fun _ _ _ => True) (fun _ τ => 2 ^ τ) where + heads := 1 + constant := 0 + net p := 2 ^ paddedTime p.2.1 * (1 - p.2.2) + polyTime := computableInPolyTime_toyNet + sum_value x t _ _ := by + have h0 : 0 ∈ Finset.range (scheduleCount 1 t) := + Finset.mem_range.mpr (Nat.one_le_pow _ _ (by norm_num)) + rw [Finset.sum_eq_single_of_mem 0 h0 fun σ _ hσ => by + rw [Nat.sub_eq_zero_of_le (Nat.one_le_iff_ne_zero.mpr hσ), Nat.mul_zero]] + rw [Nat.sub_zero, Nat.mul_one] + admissible _ _ _ _ _ _ := trivial + +/-- The simulation computes the count on a concrete input and clock. -/ +example : simulate toyFamily ([true, false], 5) = 2 ^ paddedTime 5 := + simulate_eq toyFamily (by decide) (by norm_num) le_rfl + +/-- On an input that is too long for its clock the simulation outputs `0`. -/ +example : simulate toyFamily ([true, false, true], 2) = 0 := by + simp [simulate] + +/-! ### The conditional endpoint on the toy instances -/ + +/-- With the toy interfaces and the time-constructible `T n = 2 ^ 2 ^ n ≥ max n 2`, the count at +the padded clock is computable within time `2 ^ O(T / √(log T))` and space `T ^ O(1)`. -/ +example : ∃ C d : ℕ, ComputableInO + (fun x : List Bool => 2 ^ paddedTime (1 * 2 ^ 2 ^ x.length)) encBits encNat + (fun x => 2 ^ (C * 2 ^ 2 ^ x.length / Nat.sqrt (Nat.log 2 (2 ^ 2 ^ x.length)))) + (fun x => (2 ^ 2 ^ x.length) ^ d) := + exists_computableInO_count toyFamily toyContraction (fun _ _ => le_rfl) + Cslib.Complexity.timeConstructible_two_pow_two_pow + (fun n => max_le (Nat.lt_two_pow_self.le.trans (Nat.pow_le_pow_right (by norm_num) + Nat.lt_two_pow_self.le)) (by + calc 2 = 2 ^ 2 ^ 0 := by norm_num + _ ≤ 2 ^ 2 ^ n := Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_right + (by norm_num) (Nat.zero_le n)))) + le_rfl (rule := Prod.snd) (by fun_prop) + +end ComplexityTests.CountingSimulation From f6b09bfe62e49e97f826bccc88cf2152e3103fcb Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:42:43 -0400 Subject: [PATCH 09/10] feat(Classes/CountingSimulation): pass the padded time to the rule in unary MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A comparison such as 2^τ < 2·count is polynomial-time only with τ in unary; τ ≤ 2t keeps the rule's input polynomial in the clock. Add a test applying the endpoint with the strict-majority rule. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/CountingSimulation/Assembly.lean | 27 +++++++++---------- ComplexityTests/CountingSimulation.lean | 27 +++++++++++++++---- 2 files changed, 35 insertions(+), 19 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean index 6411651625..a0f6d3e821 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean @@ -36,8 +36,8 @@ With the clock `t = c * T n` of a time-constructible `T n ≥ max n 2`, the sche `3 ^ O(T / log T)`, so the total time is `2 ^ O(T / √(log T))` in the natural-number scale of `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`, and the space is polynomial in `T` (`Cslib.Complexity.CountingSimulation.exists_computableInO_count`). The result may be any -polynomial-time function of the padded time and the count, such as a comparison deciding -acceptance. +polynomial-time function of the padded time, in unary, and the count, such as a comparison +deciding acceptance. ## Main definitions @@ -105,7 +105,7 @@ private theorem computableInPolyTime_paddedTime_succ : fun_prop private theorem computableInPolyTime_paddedTime : - ComputableInPolyTime paddedTime encUnary encNat := by + ComputableInPolyTime paddedTime encUnary encUnary := by rw [show paddedTime = _ from funext paddedTime_eq] fun_prop @@ -311,16 +311,16 @@ theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible c /-- **The count within time `2 ^ O(T / √(log T))` and polynomial space** (conditional on the interfaces). Let `T` be time-constructible with `max n 2 ≤ T n`, let `c ≥ 1`, and let `rule` be a -polynomial-time function of a padded time and a count. Given a network family for `count`, with -`count x τ ≤ 2 ^ τ`, and a contraction algorithm, the function sending `x` to `rule` of the padded -clock `τ = paddedTime (c * T |x|)` and of `count x τ` is computable within time -`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d` on inputs of length `n`, for constants `C` and -`d`. -/ +polynomial-time function of a padded time, in unary, and a count, in binary. Given a network family +for `count`, with `count x τ ≤ 2 ^ τ`, and a contraction algorithm, the function sending `x` to +`rule` of the padded clock `τ = paddedTime (c * T |x|)` and of `count x τ` is computable within +time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d` on inputs of length `n`, for constants `C` +and `d`. -/ theorem exists_computableInO_count (F : NetworkFamily encN value Admissible count) (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ) {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c) {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β} - (hrule : ComputableInPolyTime rule (encPair encNat encNat) encβ) : + (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ) : ∃ C d : ℕ, ComputableInO (fun x : List Bool => rule (paddedTime (c * T x.length), count x (paddedTime (c * T x.length)))) @@ -331,7 +331,7 @@ theorem exists_computableInO_count (F : NetworkFamily encN value Admissible coun -- Preparing the context `(x, c * T |x|)`, with the clock in unary. have hmul : ComputableInPolyTime (fun n : ℕ => c * n) encUnary encUnary := by fun_prop have htau : ComputableInPolyTime (fun p : List Bool × ℕ => paddedTime p.2) - (encPair encBits encUnary) encNat := computableInPolyTime_paddedTime.comp (by fun_prop) + (encPair encBits encUnary) encUnary := computableInPolyTime_paddedTime.comp (by fun_prop) let cT : NativeCertificate (fun x : List Bool => T x.length) encBits encNat := ⟨_, _, hT.computableInO⟩ let cU : NativeCertificate (fun n : ℕ => n) encNat encUnary := ⟨_, _, ComputableInO.natToUnary⟩ @@ -375,10 +375,9 @@ theorem exists_computableInO_count (F : NetworkFamily encN value Admissible coun omega have hsimx : simulate F (x, t) = count x (paddedTime t) := simulate_eq F hnt h2t (hcount x _) - have hout : (encPair encNat encNat (paddedTime t, simulate F (x, t))).length ≤ 6 * t + 3 := by - have h1 : (encNat (paddedTime t)).length ≤ paddedTime t := by - rw [length_encNat_eq_size] - exact Nat.size_le.mpr Nat.lt_two_pow_self + have hout : (encPair encUnary encNat (paddedTime t, simulate F (x, t))).length ≤ 6 * t + 3 := by + have h1 : (encUnary (paddedTime t)).length = paddedTime t := by + simp only [encUnary_apply, List.length_replicate] have h2 : (encNat (simulate F (x, t))).length ≤ paddedTime t + 1 := by rw [hsimx] calc _ ≤ (encNat (2 ^ paddedTime t)).length := length_encNat_mono (hcount x _) diff --git a/ComplexityTests/CountingSimulation.lean b/ComplexityTests/CountingSimulation.lean index 1d8d0d9958..d6b681f0df 100644 --- a/ComplexityTests/CountingSimulation.lean +++ b/ComplexityTests/CountingSimulation.lean @@ -122,6 +122,14 @@ example : simulate toyFamily ([true, false, true], 2) = 0 := by /-! ### The conditional endpoint on the toy instances -/ +/-- `T n = 2 ^ 2 ^ n` meets the bound `max n 2 ≤ T n` of the endpoint. -/ +theorem max_le_two_pow_two_pow (n : ℕ) : max n 2 ≤ 2 ^ 2 ^ n := + max_le (Nat.lt_two_pow_self.le.trans (Nat.pow_le_pow_right (by norm_num) + Nat.lt_two_pow_self.le)) + (calc 2 = 2 ^ 2 ^ 0 := by norm_num + _ ≤ 2 ^ 2 ^ n := + Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_right (by norm_num) (Nat.zero_le n))) + /-- With the toy interfaces and the time-constructible `T n = 2 ^ 2 ^ n ≥ max n 2`, the count at the padded clock is computable within time `2 ^ O(T / √(log T))` and space `T ^ O(1)`. -/ example : ∃ C d : ℕ, ComputableInO @@ -130,11 +138,20 @@ example : ∃ C d : ℕ, ComputableInO (fun x => (2 ^ 2 ^ x.length) ^ d) := exists_computableInO_count toyFamily toyContraction (fun _ _ => le_rfl) Cslib.Complexity.timeConstructible_two_pow_two_pow - (fun n => max_le (Nat.lt_two_pow_self.le.trans (Nat.pow_le_pow_right (by norm_num) - Nat.lt_two_pow_self.le)) (by - calc 2 = 2 ^ 2 ^ 0 := by norm_num - _ ≤ 2 ^ 2 ^ n := Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_right - (by norm_num) (Nat.zero_le n)))) + max_le_two_pow_two_pow le_rfl (rule := Prod.snd) (by fun_prop) +/-- The strict-majority comparison `2 ^ τ < 2 * count` used for `BPTIME` and `PPTIME` is a +polynomial-time rule because the padded time is passed in unary. On the toy family every string +is accepted, so the rule accepts every input. -/ +example : ∃ C d : ℕ, ComputableInO + (fun x : List Bool => decide (2 ^ paddedTime (1 * 2 ^ 2 ^ x.length) < + 2 * 2 ^ paddedTime (1 * 2 ^ 2 ^ x.length))) encBits encBool + (fun x => 2 ^ (C * 2 ^ 2 ^ x.length / Nat.sqrt (Nat.log 2 (2 ^ 2 ^ x.length)))) + (fun x => (2 ^ 2 ^ x.length) ^ d) := + exists_computableInO_count toyFamily toyContraction (fun _ _ => le_rfl) + Cslib.Complexity.timeConstructible_two_pow_two_pow + max_le_two_pow_two_pow + le_rfl (rule := fun p => decide (2 ^ p.1 < 2 * p.2)) (by fun_prop) + end ComplexityTests.CountingSimulation From aa310eaa675a69b23f50a081049951e67e37ce9a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:47:48 -0400 Subject: [PATCH 10/10] feat(Classes/CountingSimulation): conditional NTIME/BPTIME/PPTIME simulations (#1833 E1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Under the network and contraction interfaces, every problem in NTIME[T], BPTIME[T] or PPTIME[T] (T time-constructible, max n 2 ≤ T n) is decided within time 2^(C·T/√⌊log₂ T⌋) and space T^d, hence lies in ⋃ C, DTIME(2^(C·T/√⌊log₂ T⌋)). Uses the count-to-decision rules of #1841 and #1847. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../CountingSimulation/Containments.lean | 197 ++++++++++++++++++ .../CountingSimulationContainments.lean | 61 ++++++ 3 files changed, 259 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean create mode 100644 ComplexityTests/CountingSimulationContainments.lean diff --git a/Complexity.lean b/Complexity.lean index b548b0b0a6..28de6ac2b5 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1030,6 +1030,7 @@ public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace public import Complexity.Computability.Complexity.Classes.Counting.Space public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly +public import Complexity.Computability.Complexity.Classes.CountingSimulation.Containments public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces public import Complexity.Computability.Complexity.Classes.DP public import Complexity.Computability.Complexity.Classes.EXP diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean new file mode 100644 index 0000000000..715a622e1e --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Containments.lean @@ -0,0 +1,197 @@ +/- +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.CountingSimulation.Assembly +public import Complexity.Computability.Complexity.Classes.Time.AcceptCount +public import Complexity.Computability.Complexity.Classes.PP.Time +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary + +/-! +# Nondeterministic and probabilistic time in deterministic time `2 ^ O(T / √(log T))` + +**Conditional** on the interfaces of the counting simulation (#1833): network families for the +accept counts of all finite-state fair-coin machines +(`Cslib.Complexity.CountingSimulation.NetworkFamilies`) and a contraction algorithm +(`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`). Under these hypotheses, for every +time-constructible `T` with `max n 2 ≤ T n`, every problem in `NTIME[T]`, `BPTIME[T]` or +`PPTIME[T]` is decided within time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`. + +Each class is reduced to the accept count `A_M(x)` of a fair-coin machine `M` at every padded time +`τ` past a linear clock: `x ∈ L ↔ 0 < A_M(x)` for `NTIME`, and `x ∈ L ↔ 2 ^ τ < 2 * A_M(x)` for +`BPTIME` and `PPTIME` (`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`, +`Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`, +`Turing.MultiTapePTM.decidesByMajorityInTime_iff`). The count is computed by the simulation of +`Cslib.Complexity.CountingSimulation.exists_computableInO_count`, and the comparison is a +polynomial-time function of the padded time and the count. + +## Main definitions + +* `Cslib.Complexity.CountingSimulation.NetworkFamilies`: network families for all machines. + +## Main results + +* `Cslib.Complexity.CountingSimulation.exists_decidableInTimeAndSpace_of_mem_NTIME`, + `exists_decidableInTimeAndSpace_of_mem_BPTIME`, `exists_decidableInTimeAndSpace_of_mem_PPTIME`: + time `2 ^ O(T / √(log T))` and space polynomial in `T`. +* `Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME`, `BPTIME_subset_iUnion_DTIME`, + `PPTIME_subset_iUnion_DTIME`: the containments in `⋃ C, DTIME (2 ^ (C * T / √⌊log₂ T⌋))`. +-/ + +public section + +namespace Cslib.Complexity.CountingSimulation + +open Turing Turing.MultiTapeTM + +variable {N : Type} {encN : N ↪ List Bool} {value : N → ℕ} {Admissible : ℕ → ℕ → N → Prop} + {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} + +/-- **Network families for all machines**: for every finite-state fair-coin machine, a network +family (`Cslib.Complexity.CountingSimulation.NetworkFamily`) for its accept count +`Turing.MultiTapePTM.acceptCount`. This is the hypothesis supplied by the block-counting step of +#1833. -/ +def NetworkFamilies (encN : N ↪ List Bool) (value : N → ℕ) (Admissible : ℕ → ℕ → N → Prop) : + Prop := + ∀ (k : ℕ) (State : Type) [Finite State] (M : MultiTapePTM k Bool State), + Nonempty (NetworkFamily encN value Admissible fun x τ => M.acceptCount x τ) + +/-- A problem decided by a polynomial-time comparison of the padded time with the accept count of +a finite-state fair-coin machine, at every padded time past a linear clock, is decided within time +`2 ^ O(T / √(log T))` and space polynomial in `T`. -/ +private theorem exists_decidableInTimeAndSpace_of_rule + (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) {k : ℕ} {State : Type} [Finite State] + (M : MultiTapePTM k Bool State) {c₁ c₂ : ℕ} {rule : ℕ × ℕ → Bool} + (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encBool) {L : Set α} + (hL : ∀ a τ, c₁ * T (enc a).length + c₂ ≤ τ → + (a ∈ L ↔ rule (τ, M.acceptCount (enc a) τ) = true)) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := by + obtain ⟨F⟩ := hnet k State M + obtain ⟨C, d, h⟩ := exists_computableInO_count F A + (fun x τ => Complexity.acceptCount_le_two_pow) hT hTn (c := c₁ + c₂ + 1) (by omega) hrule + obtain ⟨K, hK, -⟩ := h.of_encIn_eq enc fun a => rfl + refine ⟨(K + K + 1) * (C + 1), K + K + 2 * d, + decidableInTimeAndSpace_iff.mpr ⟨_, hK.mono (fun a => ?_) fun a => ?_, fun a => ?_⟩⟩ + · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _) + have := Nat.mul_two_pow_div_sqrt_log_two_add_le (a := K) (b := K) (C := C) h2 + simp only [Function.comp_apply, Nat.mul_add, Nat.mul_one] at this ⊢ + exact this + · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _) + have hpow : T (enc a).length ^ d ≤ (T (enc a).length + 1) ^ d := + Nat.pow_le_pow_left (Nat.le_succ _) d + have := Nat.mul_add_one_pow_add_le_pow (a := K) (b := K) (d := d) h2 + simp only [Function.comp_apply] + calc K * (T (enc a).length ^ d + 1) ≤ K * (T (enc a).length + 1) ^ d + K := by + rw [Nat.mul_add, Nat.mul_one] + exact Nat.add_le_add_right (Nat.mul_le_mul_left _ hpow) _ + _ ≤ _ := this + · have h2 : 2 ≤ T (enc a).length := (le_max_right _ _).trans (hTn _) + have hτ : c₁ * T (enc a).length + c₂ ≤ + paddedTime ((c₁ + c₂ + 1) * T (enc a).length) := by + refine le_trans ?_ (le_paddedTime _) + nlinarith + simp only [Function.comp_apply] + exact hL a _ hτ + +/-- **Nondeterministic time, deterministically** (conditional on the interfaces). For a +time-constructible `T` with `max n 2 ≤ T n`, every problem in `NTIME[T]` is decided within time +`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`, by testing whether the accept count of a +fair-coin normal form is positive. -/ +theorem exists_decidableInTimeAndSpace_of_mem_NTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ NTIME enc T) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := by + obtain ⟨k, State, _, M, c₁, c₂, hM⟩ := exists_acceptCount_of_mem_NTIME hL + exact exists_decidableInTimeAndSpace_of_rule hnet A hT hTn M + (rule := fun p => decide (0 < p.2)) (by fun_prop) fun a τ hτ => by + rw [hM a τ hτ, decide_eq_true_iff] + +/-- **Bounded-error probabilistic time, deterministically** (conditional on the interfaces). For a +time-constructible `T` with `max n 2 ≤ T n`, every problem in `BPTIME[T]` is decided within time +`2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`, by comparing the accept count with half of +the padded choice strings. -/ +theorem exists_decidableInTimeAndSpace_of_mem_BPTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ BPTIME enc T) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := by + obtain ⟨k, State, _, M, c₁, c₂, hM⟩ := exists_acceptCount_of_mem_BPTIME hL + exact exists_decidableInTimeAndSpace_of_rule hnet A hT hTn M + (rule := fun p => decide (2 ^ p.1 < 2 * p.2)) (by fun_prop) fun a τ hτ => by + rw [hM a τ hτ, decide_eq_true_iff] + +/-- **Unbounded-error probabilistic time, deterministically** (conditional on the interfaces). +For a time-constructible `T` with `max n 2 ≤ T n`, every problem in `PPTIME[T]` is decided within +time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`, by the strict-majority comparison of +the accept count. -/ +theorem exists_decidableInTimeAndSpace_of_mem_PPTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) {L : Set α} (hL : L ∈ PPTIME enc T) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d) := by + obtain ⟨c₁, c₂, k, State, _, M, hM⟩ := hL + refine exists_decidableInTimeAndSpace_of_rule hnet A hT hTn M (c₁ := c₁) (c₂ := c₂) + (rule := fun p => decide (2 ^ p.1 < 2 * p.2)) (by fun_prop) fun a τ hτ => ?_ + classical + -- Run the clock up to `τ` at `a` and leave it elsewhere. + let t' : α → ℕ := fun a' => if a' = a then τ else c₁ * T (enc a').length + c₂ + have hmono (a' : α) : c₁ * T (enc a').length + c₂ ≤ t' a' := by + by_cases h : a' = a + · subst h + simpa only [t', ite_true] using hτ + · simp only [t', h, ite_false, le_refl] + have h := (MultiTapePTM.decidesByMajorityInTime_iff.mp (hM.mono hmono) a).2 + simp only [t', ite_true] at h + rw [h] + exact decide_eq_true_iff.symm + +private theorem mem_iUnion_DTIME_of_exists {L : Set α} + (h : ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * T (enc a).length / Nat.sqrt (Nat.log 2 (T (enc a).length)))) + (fun a => T (enc a).length ^ d)) : + L ∈ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := by + obtain ⟨C, d, h⟩ := h + exact Set.mem_iUnion.mpr ⟨C, 1, 0, fun n => T n ^ d, + ComputableInTimeAndSpace.mono h (fun a => by rw [Nat.one_mul, Nat.add_zero]) fun _ => le_rfl⟩ + +/-- **`NTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C * T / √⌊log₂ T⌋)]`** (conditional on the interfaces), for a +time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem NTIME_subset_iUnion_DTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + NTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + fun _ hL => mem_iUnion_DTIME_of_exists + (exists_decidableInTimeAndSpace_of_mem_NTIME hnet A hT hTn hL) + +/-- **`BPTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C * T / √⌊log₂ T⌋)]`** (conditional on the interfaces), for a +time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem BPTIME_subset_iUnion_DTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + BPTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + fun _ hL => mem_iUnion_DTIME_of_exists + (exists_decidableInTimeAndSpace_of_mem_BPTIME hnet A hT hTn hL) + +/-- **`PPTIME[T] ⊆ ⋃ C, DTIME[2 ^ (C * T / √⌊log₂ T⌋)]`** (conditional on the interfaces), for a +time-constructible `T` with `max n 2 ≤ T n`. -/ +theorem PPTIME_subset_iUnion_DTIME (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) (hT : TimeConstructible T) + (hTn : ∀ n, max n 2 ≤ T n) : + PPTIME enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := + fun _ hL => mem_iUnion_DTIME_of_exists + (exists_decidableInTimeAndSpace_of_mem_PPTIME hnet A hT hTn hL) + +end Cslib.Complexity.CountingSimulation diff --git a/ComplexityTests/CountingSimulationContainments.lean b/ComplexityTests/CountingSimulationContainments.lean new file mode 100644 index 0000000000..73170f08a2 --- /dev/null +++ b/ComplexityTests/CountingSimulationContainments.lean @@ -0,0 +1,61 @@ +/- +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.CountingSimulation.Containments + +/-! Checks for the conditional containments of the counting simulation (#1833). + +The hypothesis `NetworkFamilies` asks for a network family for the accept count of every +finite-state fair-coin machine, with polynomial-time networks. It has no toy instance, since a +polynomial-time family with trivial networks would count accepting choice strings in polynomial +time; it is the obligation of the block-counting step. The structure `NetworkFamily` itself is +instantiated in `ComplexityTests/CountingSimulation.lean`. Here the containments are applied to a +concrete time-constructible bound, discharging `max n 2 ≤ T n`, and combined with the existing +inclusion `BPTIME ⊆ PPTIME`. -/ + +namespace ComplexityTests.CountingSimulationContainments + +open Turing.MultiTapeTM Cslib.Complexity Cslib.Complexity.CountingSimulation + +variable {N : Type} {encN : N ↪ List Bool} {value : N → ℕ} {Admissible : ℕ → ℕ → N → Prop} + {α : Type} {enc : α ↪ List Bool} + +private theorem max_le_two_pow_two_pow (n : ℕ) : max n 2 ≤ 2 ^ 2 ^ n := + max_le (Nat.lt_two_pow_self.le.trans (Nat.pow_le_pow_right (by norm_num) + Nat.lt_two_pow_self.le)) + (calc 2 = 2 ^ 2 ^ 0 := by norm_num + _ ≤ 2 ^ 2 ^ n := + Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_right (by norm_num) (Nat.zero_le n))) + +/-- With `T n = 2 ^ 2 ^ n`, nondeterministic time is in `DTIME (2 ^ (C * 2 ^ 2 ^ n / 2 ^ (n / 2)))` +for some `C`, under the interfaces: `√⌊log₂ (2 ^ 2 ^ n)⌋ = √(2 ^ n)`. -/ +example (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) : + NTIME enc (fun n => 2 ^ 2 ^ n) ⊆ + ⋃ C, DTIME enc fun n => 2 ^ (C * 2 ^ 2 ^ n / Nat.sqrt (2 ^ n)) := by + intro L hL + simpa only [Nat.log_pow (Nat.one_lt_two)] using + NTIME_subset_iUnion_DTIME hnet A timeConstructible_two_pow_two_pow max_le_two_pow_two_pow hL + +/-- Bounded-error time reaches the same bound through `PPTIME`, as well as directly. -/ +example (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) {L : Set α} + (hL : L ∈ BPTIME enc fun n => 2 ^ 2 ^ n) : + L ∈ ⋃ C, DTIME enc fun n => 2 ^ (C * 2 ^ 2 ^ n / Nat.sqrt (Nat.log 2 (2 ^ 2 ^ n))) := + PPTIME_subset_iUnion_DTIME hnet A timeConstructible_two_pow_two_pow max_le_two_pow_two_pow + (BPTIME_subset_PPTIME hL) + +/-- The strong form keeps the polynomial space bound alongside the time bound. -/ +example (hnet : NetworkFamilies encN value Admissible) + (A : ContractionAlgorithm encN value Admissible) {L : Set α} + (hL : L ∈ PPTIME enc fun n => 2 ^ 2 ^ n) : + ∃ C d : ℕ, DecidableInTimeAndSpace L enc + (fun a => 2 ^ (C * 2 ^ 2 ^ (enc a).length / Nat.sqrt (2 ^ (enc a).length))) + (fun a => (2 ^ 2 ^ (enc a).length) ^ d) := by + simpa only [Nat.log_pow Nat.one_lt_two] using exists_decidableInTimeAndSpace_of_mem_PPTIME + hnet A timeConstructible_two_pow_two_pow max_le_two_pow_two_pow hL + +end ComplexityTests.CountingSimulationContainments