From 49bd81d41c598a1ffef95aabb5d9da390773d6c7 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 17:58:23 -0400 Subject: [PATCH 1/4] 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 1cd97a465..5dd44a8b2 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 000000000..11de1d9eb --- /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 000000000..d7ca69b97 --- /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 000000000..35d0e72ab --- /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 000000000..33ab6ed75 --- /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 2/4] 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 11de1d9eb..96270db11 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 4fe33981a01ea0db45e8cfbecf7da6d0725e5043 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:38:58 -0400 Subject: [PATCH 3/4] 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 508a8e566..649b3f7f5 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 000000000..a464744eb --- /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 000000000..641165162 --- /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 000000000..d00a0135c --- /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 000000000..1d8d0d995 --- /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 4/4] 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 641165162..a0f6d3e82 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 1d8d0d995..d6b681f0d 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