From bffa3cfe4e5d12e668c7cbd21458063402759c10 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:53:49 -0400 Subject: [PATCH 1/3] feat(foundations): count tuples of bounded weight by the partition generating function The number of tuples beta : iota -> N of total weight sum w_i beta_i < p, with at most m coordinates of each positive weight, is at most exp(theta p + m pi^2/(6 theta)) for every theta > 0, hence at most 2^(4 floor(sqrt(m p)) + 4). This is the mode count (D.15) of the Boolean tensor contraction theorem of [OpenAI2026ETH] (#1538). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Combinatorics/WeightBudget.lean | 245 ++++++++++++++++++ .../Combinatorics/WeightBudget.lean | 59 +++++ 3 files changed, 305 insertions(+) create mode 100644 Complexity/Foundations/Combinatorics/WeightBudget.lean create mode 100644 ComplexityTests/Foundations/Combinatorics/WeightBudget.lean diff --git a/Complexity.lean b/Complexity.lean index fdd3b220c6..68fc1497cf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2594,6 +2594,7 @@ public import Complexity.Foundations.Combinatorics.Sunflower public import Complexity.Foundations.Combinatorics.Sunflower.LowerBound public import Complexity.Foundations.Combinatorics.Sunflower.Pluck public import Complexity.Foundations.Combinatorics.UniformSchedules +public import Complexity.Foundations.Combinatorics.WeightBudget public import Complexity.Foundations.Control.Monad.IsMonadHom.StateT public import Complexity.Foundations.Control.Monad.Memoize public import Complexity.Foundations.Data.BiTape diff --git a/Complexity/Foundations/Combinatorics/WeightBudget.lean b/Complexity/Foundations/Combinatorics/WeightBudget.lean new file mode 100644 index 0000000000..7d742fb6f2 --- /dev/null +++ b/Complexity/Foundations/Combinatorics/WeightBudget.lean @@ -0,0 +1,245 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Analysis.Complex.ExponentialBounds +import Mathlib.Analysis.Real.Pi.Bounds +import Mathlib.Analysis.SpecialFunctions.Log.Deriv +import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.SpecificLimits.Basic +import Mathlib.Data.Fintype.Pi +import Mathlib.NumberTheory.ZetaValues +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Counting tuples of bounded weight + +Give each coordinate `i` of a tuple `β : ι → ℕ` a positive weight `w i`, with at most `m` +coordinates of each weight. This file bounds the number of tuples of total weight +`∑ i, w i * β i < p` by the partition generating function: + +* for every `θ > 0` there are at most `exp (θ p + m π² / (6 θ))` of them + (`Cslib.card_le_exp_of_sum_mul_lt`); +* taking `θ = √(m / p)`, there are at most `2 ^ (4 ⌊√(m p)⌋ + 4)` + (`Cslib.card_le_two_pow_of_sum_mul_lt`). + +This is the count (D.15) of the exponent tuples of the modes in the proof of the Boolean tensor +contraction theorem of [OpenAI2026ETH] (§D.4.5, pp. 62–63), where the modes play the coordinates +and their weights are their divisibility exponents. + +**The proof.** Put `x = e^{-θ}`. Every tuple of weight below `p` has `x ^ (weight) ≥ x ^ p`, and the +sum of `x ^ (weight)` over all tuples is at most the generating product `∏ i, (1 - x ^ w i)⁻¹`. +Its logarithm is `∑ i, -log (1 - x ^ w i)`, which is at most `m` times the sum of +`-log (1 - e^{-θ j})` over the distinct weights `j`. Expanding the logarithm and summing the +geometric series bounds that sum (`Cslib.sum_neg_log_one_sub_exp_le`): + + `∑_{j ≥ 1} -log (1 - e^{-θ j}) = ∑_{h ≥ 1} 1 / (h (e^{θ h} - 1)) ≤ (1 / θ) ∑_{h ≥ 1} 1 / h² + = π² / (6 θ)`, + +using `e^y - 1 ≥ y` and `∑ 1 / h² = π² / 6` (`hasSum_zeta_two`). + +## Main results + +* `Cslib.sum_neg_log_one_sub_exp_le`: `∑_{j ∈ s} -log (1 - e^{-θ j}) ≤ π² / (6 θ)` for a finite + set `s` of positive integers. +* `Cslib.card_le_exp_of_sum_mul_lt`: the generating-function bound on the number of tuples. +* `Cslib.card_le_two_pow_of_sum_mul_lt`: its natural-number form `2 ^ (4 ⌊√(m p)⌋ + 4)`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.5, the count (D.15) + and the estimate following it (pp. 62–63). +-/ + +public section + +namespace Cslib + +open Finset Real + +/-- **The logarithm of the partition generating function.** For `θ > 0` and every finite set +`s` of positive integers, `∑_{j ∈ s} -log (1 - e^{-θ j}) ≤ π² / (6 θ)`. -/ +theorem sum_neg_log_one_sub_exp_le {θ : ℝ} (hθ : 0 < θ) (s : Finset ℕ) (hs : 0 ∉ s) : + ∑ j ∈ s, -log (1 - exp (-(θ * j))) ≤ π ^ 2 / (6 * θ) := by + have hterm : ∀ j ∈ s, HasSum (fun h : ℕ => exp (-(θ * j)) ^ (h + 1) / (h + 1)) + (-log (1 - exp (-(θ * j)))) := by + intro j hj + have hj0 : (0 : ℝ) < j := Nat.cast_pos.2 (Nat.pos_of_ne_zero fun h => hs (h ▸ hj)) + apply Real.hasSum_pow_div_log_of_abs_lt_one + rw [abs_of_pos (exp_pos _), exp_lt_one_iff] + have := mul_pos hθ hj0 + linarith + have hzeta : HasSum (fun h : ℕ => 1 / θ * (1 / ((h : ℝ) + 1) ^ 2)) (1 / θ * (π ^ 2 / 6)) := by + have h := (hasSum_nat_add_iff' 1).mpr hasSum_zeta_two + simp only [range_one, sum_singleton, Nat.cast_zero, ne_eq, OfNat.ofNat_ne_zero, + not_false_eq_true, zero_pow, div_zero, sub_zero, Nat.cast_add, Nat.cast_one] at h + exact h.mul_left _ + have hle := hasSum_le (fun h => ?_) (hasSum_sum hterm) hzeta + · calc _ ≤ 1 / θ * (π ^ 2 / 6) := hle + _ = π ^ 2 / (6 * θ) := by field_simp + -- For fixed `h`, the terms form a geometric series in `q = e^{-θ (h + 1)}`. + set y : ℝ := θ * (h + 1) with hy + have hy0 : 0 < y := by positivity + set q : ℝ := exp (-y) with hq + have hq0 : 0 ≤ q := (exp_pos _).le + have hq1 : q < 1 := exp_lt_one_iff.2 (neg_lt_zero.2 hy0) + have hpow : ∀ j : ℕ, exp (-(θ * j)) ^ (h + 1) = q ^ j := fun j => by + rw [hq, ← exp_nat_mul, ← exp_nat_mul, hy] + push_cast + ring_nf + have hgeo : ∑ j ∈ s, q ^ j ≤ (1 - q)⁻¹ - 1 := by + have := sum_le_hasSum (insert 0 s) (fun j _ => pow_nonneg hq0 j) + (hasSum_geometric_of_lt_one hq0 hq1) + rw [sum_insert hs, pow_zero] at this + linarith + have hkey : q * (1 + y) ≤ 1 := by + calc q * (1 + y) ≤ q * exp y := mul_le_mul_of_nonneg_left (by linarith [add_one_le_exp y]) hq0 + _ = 1 := by rw [hq, ← exp_add, neg_add_cancel, exp_zero] + have hq' : (1 - q)⁻¹ - 1 ≤ 1 / y := by + have h1q : 0 < 1 - q := by linarith + rw [show (1 - q)⁻¹ - 1 = q / (1 - q) by field_simp; ring, div_le_div_iff₀ h1q hy0] + linarith + have hh : (0 : ℝ) < h + 1 := by positivity + calc ∑ j ∈ s, exp (-(θ * j)) ^ (h + 1) / (h + 1) = (∑ j ∈ s, q ^ j) / (h + 1) := by + rw [sum_div] + exact sum_congr rfl fun j _ => by rw [hpow] + _ ≤ (1 / y) / (h + 1) := div_le_div_of_nonneg_right (hgeo.trans hq') hh.le + _ = 1 / θ * (1 / ((h : ℝ) + 1) ^ 2) := by rw [hy]; field_simp + +/-- **Counting tuples of bounded weight by the generating function.** Let every coordinate have a +positive weight, with at most `m` coordinates of each weight. Then for every `θ > 0` there are at +most `exp (θ p + m π² / (6 θ))` tuples of total weight below `p`. -/ +theorem card_le_exp_of_sum_mul_lt {ι : Type*} [Fintype ι] {w : ι → ℕ} (hw : ∀ i, 0 < w i) + {m : ℕ} (hm : ∀ j, #{i | w i = j} ≤ m) {p : ℕ} {S : Finset (ι → ℕ)} + (hS : ∀ β ∈ S, ∑ i, w i * β i < p) {θ : ℝ} (hθ : 0 < θ) : + (#S : ℝ) ≤ exp (θ * p + m * (π ^ 2 / (6 * θ))) := by + classical + set x : ℝ := exp (-θ) with hx + have hx0 : 0 < x := exp_pos _ + have hx1 : x < 1 := exp_lt_one_iff.2 (neg_lt_zero.2 hθ) + -- Every tuple contributes at least `x ^ p` to the generating sum. + have h1 : (#S : ℝ) * x ^ p ≤ ∑ β ∈ S, x ^ (∑ i, w i * β i) := by + calc (#S : ℝ) * x ^ p = ∑ _β ∈ S, x ^ p := by rw [sum_const, nsmul_eq_mul] + _ ≤ _ := sum_le_sum fun β hβ => pow_le_pow_of_le_one hx0.le hx1.le (hS β hβ).le + -- The tuples lie in a box, over which the generating sum factors. + have hsub : S ⊆ Fintype.piFinset fun _ => range p := by + intro β hβ + rw [Fintype.mem_piFinset] + intro i + rw [mem_range] + calc β i ≤ w i * β i := Nat.le_mul_of_pos_left _ (hw i) + _ ≤ ∑ i, w i * β i := single_le_sum (fun i _ => Nat.zero_le (w i * β i)) (mem_univ i) + _ < p := hS β hβ + have h2 : ∑ β ∈ S, x ^ (∑ i, w i * β i) ≤ ∏ i, ∑ b ∈ range p, (x ^ w i) ^ b := by + rw [prod_univ_sum] + calc ∑ β ∈ S, x ^ (∑ i, w i * β i) = ∑ β ∈ S, ∏ i, (x ^ w i) ^ β i := by + refine sum_congr rfl fun β _ => ?_ + rw [← prod_pow_eq_pow_sum] + exact prod_congr rfl fun i _ => pow_mul x (w i) (β i) + _ ≤ ∑ β ∈ Fintype.piFinset fun _ => range p, ∏ i, (x ^ w i) ^ β i := + sum_le_sum_of_subset_of_nonneg hsub fun _ _ _ => prod_nonneg fun _ _ => by positivity + -- Each factor is a truncated geometric series. + have h3 : ∏ i, ∑ b ∈ range p, (x ^ w i) ^ b ≤ exp (∑ i, -log (1 - x ^ w i)) := by + rw [exp_sum] + refine prod_le_prod₀ (fun i _ => sum_nonneg fun _ _ => by positivity) fun i _ => ?_ + have hy0 : 0 ≤ x ^ w i := by positivity + have hy1 : x ^ w i < 1 := pow_lt_one₀ hx0.le hx1 (hw i).ne' + rw [exp_neg, exp_log (by linarith)] + exact sum_le_hasSum _ (fun _ _ => by positivity) (hasSum_geometric_of_lt_one hy0 hy1) + -- Group the coordinates by weight. + have h4 : ∑ i, -log (1 - x ^ w i) ≤ m * (π ^ 2 / (6 * θ)) := by + have hxj : ∀ j : ℕ, x ^ j = exp (-(θ * j)) := fun j => by + rw [hx, ← exp_nat_mul] + ring_nf + have hnn : ∀ j ∈ univ.image w, 0 ≤ -log (1 - x ^ j) := by + intro j hj + obtain ⟨i, -, rfl⟩ := mem_image.1 hj + have : 0 < 1 - x ^ w i := by linarith [pow_lt_one₀ hx0.le hx1 (hw i).ne'] + have : 1 - x ^ w i ≤ 1 := by linarith [pow_pos hx0 (w i)] + linarith [log_nonpos (by linarith) this] + have h0 : 0 ∉ univ.image w := by + simp only [mem_image, mem_univ, true_and, not_exists] + exact fun i h => (hw i).ne' h + rw [sum_comp (fun j => -log (1 - x ^ j)) w] + calc ∑ j ∈ univ.image w, #{i ∈ univ | w i = j} • -log (1 - x ^ j) + ≤ ∑ j ∈ univ.image w, m • -log (1 - x ^ j) := + sum_le_sum fun j hj => nsmul_le_nsmul_left (hnn j hj) (hm j) + _ = m * ∑ j ∈ univ.image w, -log (1 - exp (-(θ * j))) := by + rw [← smul_sum, nsmul_eq_mul] + simp only [hxj] + _ ≤ m * (π ^ 2 / (6 * θ)) := + mul_le_mul_of_nonneg_left (sum_neg_log_one_sub_exp_le hθ _ h0) (Nat.cast_nonneg m) + have hxp : x ^ p * exp (θ * p) = 1 := by + rw [hx, ← exp_nat_mul, ← exp_add] + ring_nf + exact exp_zero + calc (#S : ℝ) = #S * x ^ p * exp (θ * p) := by rw [mul_assoc, hxp, mul_one] + _ ≤ exp (m * (π ^ 2 / (6 * θ))) * exp (θ * p) := + mul_le_mul_of_nonneg_right ((h1.trans h2).trans (h3.trans (exp_le_exp.2 h4))) + (exp_pos _).le + _ = exp (θ * p + m * (π ^ 2 / (6 * θ))) := by rw [← exp_add, add_comm] + +/-- `1 + π² / 6 ≤ 4 log 2`, so `exp ((1 + π² / 6) y) ≤ 16 ^ y`. -/ +private theorem one_add_pi_sq_div_six_le : 1 + π ^ 2 / 6 ≤ 4 * log 2 := by + nlinarith [pi_lt_d2, pi_pos, log_two_gt_d9] + +/-- **Counting tuples of bounded weight, natural-number form.** Let every coordinate have a +positive weight, with at most `m` coordinates of each weight. Then there are at most +`2 ^ (4 ⌊√(m p)⌋ + 4)` tuples of total weight below `p`: the generating-function bound at +`θ = √(m / p)`. -/ +theorem card_le_two_pow_of_sum_mul_lt {ι : Type*} [Fintype ι] {w : ι → ℕ} (hw : ∀ i, 0 < w i) + {m : ℕ} (hm : ∀ j, #{i | w i = j} ≤ m) {p : ℕ} {S : Finset (ι → ℕ)} + (hS : ∀ β ∈ S, ∑ i, w i * β i < p) : #S ≤ 2 ^ (4 * Nat.sqrt (m * p) + 4) := by + classical + rcases Nat.eq_zero_or_pos p with rfl | hp + · have : S = ∅ := eq_empty_of_forall_notMem fun β hβ => Nat.not_lt_zero _ (hS β hβ) + simp [this] + rcases Nat.eq_zero_or_pos m with rfl | hm0 + · have : IsEmpty ι := ⟨fun i => by + have hpos : 0 < #{i' | w i' = w i} := card_pos.2 ⟨i, by simp⟩ + have := hm (w i) + omega⟩ + exact (card_le_one_of_subsingleton S).trans Nat.one_le_two_pow + set n := Nat.sqrt (m * p) + set a : ℝ := √(m : ℝ) with ha + set b : ℝ := √(p : ℝ) with hb + have ha0 : 0 < a := Real.sqrt_pos.2 (Nat.cast_pos.2 hm0) + have hb0 : 0 < b := Real.sqrt_pos.2 (Nat.cast_pos.2 hp) + have ha2 : (m : ℝ) = a ^ 2 := (Real.sq_sqrt (Nat.cast_nonneg m)).symm + have hb2 : (p : ℝ) = b ^ 2 := (Real.sq_sqrt (Nat.cast_nonneg p)).symm + have hexp : a / b * p + m * (π ^ 2 / (6 * (a / b))) = a * b * (1 + π ^ 2 / 6) := by + rw [ha2, hb2] + field_simp + have hab : a * b ≤ n + 1 := by + have hlt : ((m * p : ℕ) : ℝ) < ((n + 1 : ℕ) : ℝ) ^ 2 := by + exact_mod_cast Nat.lt_succ_sqrt' (m * p) + have hsq : (a * b) ^ 2 < ((n : ℝ) + 1) ^ 2 := by + rw [mul_pow, ← ha2, ← hb2] + push_cast at hlt + exact hlt + exact (lt_of_pow_lt_pow_left₀ 2 (by positivity) hsq).le + have hreal : (#S : ℝ) ≤ 2 ^ (4 * n + 4) := by + calc (#S : ℝ) ≤ exp (a / b * p + m * (π ^ 2 / (6 * (a / b)))) := + card_le_exp_of_sum_mul_lt hw hm hS (div_pos ha0 hb0) + _ = exp (a * b * (1 + π ^ 2 / 6)) := by rw [hexp] + _ ≤ exp (((4 * n + 4 : ℕ) : ℝ) * log 2) := by + refine exp_le_exp.2 ?_ + have h1 : (0 : ℝ) ≤ 1 + π ^ 2 / 6 := by positivity + calc a * b * (1 + π ^ 2 / 6) ≤ (n + 1) * (4 * log 2) := + mul_le_mul hab one_add_pi_sq_div_six_le h1 (by positivity) + _ = ((4 * n + 4 : ℕ) : ℝ) * log 2 := by push_cast; ring + _ = 2 ^ (4 * n + 4) := by rw [exp_nat_mul, exp_log two_pos] + exact_mod_cast hreal + +end Cslib diff --git a/ComplexityTests/Foundations/Combinatorics/WeightBudget.lean b/ComplexityTests/Foundations/Combinatorics/WeightBudget.lean new file mode 100644 index 0000000000..294c9e7249 --- /dev/null +++ b/ComplexityTests/Foundations/Combinatorics/WeightBudget.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 + +public import Complexity.Foundations.Combinatorics.WeightBudget + +public section + +open Finset Real + +namespace Cslib.Tests.WeightBudget + +/-! ### A concrete budget + +Two coordinates of weights `1` and `2` and budget `p = 5`: the tuples with `β₀ + 2 β₁ < 5` are +the five with `β₁ = 0`, the three with `β₁ = 1` and the one with `β₁ = 2`. -/ + +/-- The weights `1, 2`. -/ +def w (i : Fin 2) : ℕ := i.val + 1 + +/-- The tuples of weight below `5`. -/ +def budget : Finset (Fin 2 → ℕ) := + {β ∈ Fintype.piFinset fun _ => range 5 | ∑ i, w i * β i < 5} + +example : #budget = 9 := by decide + +/-- Each weight occurs once, so `m = 1`: the bound is `2 ^ (4 ⌊√5⌋ + 4) = 2 ^ 12`. -/ +example : #budget ≤ 2 ^ 12 := by + have h := card_le_two_pow_of_sum_mul_lt (w := w) (m := 1) (p := 5) (S := budget) + (fun i => Nat.succ_pos _) (fun j => by + rw [card_le_one] + intro a ha b hb + rw [mem_filter] at ha hb + exact Fin.ext (by simp only [w] at ha hb; omega)) + (fun β hβ => (mem_filter.1 hβ).2) + simpa [(Nat.eq_sqrt.2 ⟨by norm_num, by norm_num⟩ : 2 = Nat.sqrt 5).symm] using h + +/-- The real form at `θ = 1`. -/ +example : (#budget : ℝ) ≤ exp (5 + π ^ 2 / 6) := by + have h := card_le_exp_of_sum_mul_lt (w := w) (m := 1) (p := 5) (S := budget) + (fun i => Nat.succ_pos _) (fun j => by + rw [card_le_one] + intro a ha b hb + rw [mem_filter] at ha hb + exact Fin.ext (by simp only [w] at ha hb; omega)) + (fun β hβ => (mem_filter.1 hβ).2) one_pos + simpa using h + +/-! ### The logarithmic sum -/ + +example : -log (1 - exp (-(1 * ((1 : ℕ) : ℝ)))) + -log (1 - exp (-(1 * ((2 : ℕ) : ℝ)))) ≤ + π ^ 2 / (6 * 1) := by + have h := sum_neg_log_one_sub_exp_le one_pos {1, 2} (by decide) + rwa [sum_pair (by decide)] at h + +end Cslib.Tests.WeightBudget From bafb62e4272d58d0e9795ad624a3a42a8cc6f085 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:00:47 -0400 Subject: [PATCH 2/3] feat(circuit/frontier): parameter schedule of the contraction recursion, (D.11) and (D.15) The schedule (D.4)-(D.6) of the Boolean tensor contraction recursion of [OpenAI2026ETH] on the floor-log / Nat.sqrt scale of #1865, with the certificate exists_activeBounds: for large s every active call satisfies the packing conditions (D.6), the precision bound (D.11) p_t u <= 34 M D_t, polynomial precisions and depth <= log s - 2. The mode count (D.15) card_modeBudget_le bounds the mode tuples by 2^e_d, and the e_d sum to O(s / sqrt(log s)) (#1538). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Frontier/TensorNetwork/Schedule.lean | 724 ++++++++++++++++++ .../Frontier/TensorNetworkSchedule.lean | 90 +++ 3 files changed, 815 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean create mode 100644 ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean diff --git a/Complexity.lean b/Complexity.lean index 68fc1497cf..6c584d06fd 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -874,6 +874,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Explicit public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ModeExpansion +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional public import Complexity.Computability.Circuit.Frontier.Witness diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean new file mode 100644 index 0000000000..6fa306e299 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean @@ -0,0 +1,724 @@ +/- +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.Circuit.Frontier.TensorNetwork.ModeExpansion +public import Complexity.Foundations.Data.Nat.SqrtLog +import Complexity.Foundations.Combinatorics.WeightBudget +import Complexity.Foundations.Data.Nat.Asymptotics +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# The parameter schedule of the tensor contraction recursion + +This file fixes the parameters of the recursion in the proof of the Boolean tensor contraction +theorem (Theorem D.1) of [OpenAI2026ETH] (§D.4.2, (D.4)–(D.6), p. 58) and proves the inequalities +its running time rests on: the conditions of the packing lemma, the precision bound (D.11) +(p. 61) and the count (D.15) of the mode tuples (pp. 62–63). Correctness of the recursion does not +depend on these choices; they bound the number of its calls by `2 ^ O(s / √⌊log₂ s⌋)` (§D.4.7, +p. 64). + +**The schedule.** Fix the size `s` and write `λ = ⌊log₂ s⌋`. + +* A call with at most `H = ⌊s / ⌊√λ⌋⌋` edges is a leaf (`leafSize`). +* At depth `d` the taper is `u_d = ⌊λ / 2 ^ (17 + d)⌋` (`taper`), the manuscript's + `⌊ε λ / 2 ^ d⌋` with `ε = 1 / (128 · 1024) = 2 ^ (-17)`. +* Labels have `a_d = 2 ∑_{j ≤ d} u_j` coordinates (`slotBits`), packets `L = 2 ^ a_d` slots, and + there are `D_arr = 64 ^ (2 a_d)` pairs of labels (`r = 64`). +* The degree bound is `Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` (`degreeBound`), a power of two that is at least + `s ^ (9/10)` (`pow_nine_le_degreeBound_pow_ten`) and at most `2 ^ 20 s ^ 9` in tenth power. +* The node `t` of valuation `i` is recovered from its children at precision + `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` (`nodePrecision`), as in Lemma D.5, where + `D_t = L / 2 ^ i`. +* Precisions stay below `precisionBound C s d`, which starts at `C s` and grows by + `8 C s (4 · 2 ^ a_d + a_d + 1)` per level. + +**Active calls.** `Active C s d M p` says that a call at depth `d` has `M` edges, with +`16 ^ d M ≤ C s` and `H < M`, and precision `p ≤ precisionBound C s d`. The root is active when +it has more than `H` edges and edges and precision are at most `C s` (`Active.root`), and an +active call's children are active when they have more than `H` edges (`Active.child`): Lemma D.3 +gives them at most `M / 16` edges. + +**The certificate.** For every `C` there is `s₀` such that for all `s ≥ s₀` +(`exists_activeBounds`): + +* precisions up to depth `λ` are at most `s ^ 2`; +* every active call satisfies `ActiveBounds`: its depth is at most `λ - 2`; `1 ≤ u_d ≤ M`; the + conditions (D.6) of the packing lemma, `2 Δ D_arr² ≤ M`, `L D_arr ≤ M` and `2 L ≤ Δ`, in the form + `Cslib.PacketPacking.exists_packing` takes them; `M (2 L - 1) + 1 ≤ 2 ^ (4 λ)` interpolation + points; and, for each node `t` with `q_t > 0` and `h = ⌈3 M / u⌉`, the precision bound (D.11) + `p_t u_d ≤ 34 M D_t` together with `p_t ≤ precisionBound C s (d + 1)`. + +From (D.11), the mode count (D.15) gives at most `2 ^ e_d` mode tuples with +`e_d = 4 ⌊15360 C s / (⌊√λ⌋ 8 ^ d)⌋ + 4` (`card_modeBudget_le`, `branchExponent`), and the +exponents sum to `O(s / √⌊log₂ s⌋)` over the levels (`sum_branchExponent_le`). With the factor +`2 ^ (2 λ)` for the nodes, interpolation points and groups (`ActiveBounds.branching_le`), a call at +depth `d` has at most `2 ^ (2 λ + e_d)` children. These are the hypotheses of a recursion tree with +`2 ^ O(s / √⌊log₂ s⌋)` nodes. + +**Differences from the source.** We use `λ = ⌊log₂ s⌋` and `H = ⌊s / ⌊√λ⌋⌋`, the scale of the +consumer interface of #1833, where the manuscript has `⌈log₂ s⌉` and `⌈s / ⌊√λ⌋⌉`; we take +`Δ = 2 ^ (⌊9 λ / 10⌋ + 2)` instead of `⌈s ^ (9/10)⌉`; and we prove the weaker lower bound +`u_d ≥ ⌊√λ⌋ / (2 ^ 17 C)` instead of `u_d ≥ λ ^ (4/5)`, which suffices for (D.11). The manuscript's +precision bound `p ≤ s λ^{O(1)} 2 ^ (a_{d-1})` is `precisionBound_le`. + +## Main definitions + +* `leafSize`, `taper`, `prefixBits`, `slotBits`, `degreeBound`, `nodePrecision`, + `precisionBound`, `branchExponent`: the schedule. +* `Active`: an active call within the schedule. +* `ActiveBounds`: the inequalities that hold at an active call for large `s`. + +## Main results + +* `exists_activeBounds`: the parameter certificate. +* `card_modeBudget_le`: the mode count (D.15) at an active call. +* `sum_branchExponent_le`: the excess exponents sum to `O(s / √⌊log₂ s⌋)`. +* `precisionBound_le`: the precision bound `p ≤ C s 2 ^ (a_{d-1}) (1 + d (8 λ + 40))`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.2 (D.4)–(D.6) + (p. 58), Lemma D.5 and (D.11) (pp. 60–61), (D.13)–(D.15) (pp. 62–63) and §D.4.7 (p. 64). +-/ + +public section + +namespace Cslib.Circuits.Frontier.ContractionSchedule + +open Finset Filter + +/-! ### The schedule -/ + +/-- The leaf size `H = ⌊s / ⌊√⌊log₂ s⌋⌋⌋`: calls with at most `H` edges are evaluated by direct +summation. -/ +@[expose] def leafSize (s : ℕ) : ℕ := s / Nat.sqrt (Nat.log 2 s) + +/-- The taper `u_d = ⌊⌊log₂ s⌋ / 2 ^ (17 + d)⌋` at depth `d`, the manuscript's `⌊ε λ / 2 ^ d⌋` +with `ε = 2 ^ (-17)`. -/ +@[expose] def taper (s d : ℕ) : ℕ := Nat.log 2 s / 2 ^ (17 + d) + +/-- `2 ∑_{j < d} u_j`, the manuscript's `a_{d - 1}`. -/ +@[expose] def prefixBits (s d : ℕ) : ℕ := 2 * ∑ j ∈ range d, taper s j + +/-- The number `a_d = 2 ∑_{j ≤ d} u_j` of label coordinates at depth `d`: packets have `2 ^ a_d` +slots. -/ +@[expose] def slotBits (s d : ℕ) : ℕ := prefixBits s (d + 1) + +/-- The degree bound `Δ = 2 ^ (⌊9 ⌊log₂ s⌋ / 10⌋ + 2)`, a power of two at least `s ^ (9/10)`. -/ +@[expose] def degreeBound (s : ℕ) : ℕ := 2 ^ (9 * Nat.log 2 s / 10 + 2) + +/-- The precision `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` at which a node `t` of valuation `i` +is recovered by Lemma D.5, for input precision `p`, `h = ⌈3 M / u⌉` and `2 ^ a` slots. -/ +@[expose] def nodePrecision (p h a M i : ℕ) : ℕ := p + 8 * h * 2 ^ (a - i) + 8 * M * (a + 1) + +/-- The precision schedule: `C s` at the root, growing by `8 C s (4 · 2 ^ a_d + a_d + 1)` from +depth `d` to `d + 1`. -/ +@[expose] def precisionBound (C s : ℕ) : ℕ → ℕ + | 0 => C * s + | d + 1 => precisionBound C s d + 8 * C * s * (4 * 2 ^ slotBits s d + slotBits s d + 1) + +/-- The excess exponent `e_d = 4 ⌊15360 C s / (⌊√⌊log₂ s⌋⌋ 8 ^ d)⌋ + 4` of the mode count at +depth `d`. -/ +@[expose] def branchExponent (C s d : ℕ) : ℕ := + 4 * (15360 * C * s / (Nat.sqrt (Nat.log 2 s) * 8 ^ d)) + 4 + +/-- An *active* call at depth `d` of the recursion for size `s` and constant `C`: it has `M` +edges, at most `C s / 16 ^ d` and more than the leaf size, and precision `p` within the +schedule. -/ +structure Active (C s d M p : ℕ) : Prop where + /-- Each level divides the number of edges by at least `16`. -/ + edges_le : 16 ^ d * M ≤ C * s + /-- The call is not a leaf. -/ + leafSize_lt : leafSize s < M + /-- The precision is within the schedule. -/ + precision_le : p ≤ precisionBound C s d + +/-- The root is active when it is not a leaf and its edges and precision are at most `C s`. -/ +theorem Active.root {C s M p : ℕ} (hM : M ≤ C * s) (hH : leafSize s < M) (hp : p ≤ C * s) : + Active C s 0 M p := + ⟨by simpa using hM, hH, hp⟩ + +/-- A child of an active call at depth `d` with at most a sixteenth of its edges, precision +within the schedule and more than the leaf size is an active call at depth `d + 1`. -/ +theorem Active.child {C s d M p M' p' : ℕ} (h : Active C s d M p) (hM : 16 * M' ≤ M) + (hH : leafSize s < M') (hp : p' ≤ precisionBound C s (d + 1)) : Active C s (d + 1) M' p' := + ⟨by rw [pow_succ, mul_assoc]; exact (Nat.mul_le_mul_left _ hM).trans h.edges_le, hH, hp⟩ + +/-! ### Arithmetic of the schedule -/ + +theorem slotBits_eq (s d : ℕ) : slotBits s d = prefixBits s d + 2 * taper s d := by + simp only [slotBits, prefixBits, sum_range_succ, mul_add] + +theorem prefixBits_le_slotBits (s d : ℕ) : prefixBits s d ≤ slotBits s d := by + rw [slotBits_eq] + exact Nat.le_add_right _ _ + +/-- `∑_{j < d} ⌊y / 2 ^ (j + 1)⌋ ≤ y`. -/ +private theorem sum_div_two_pow_succ_le (y d : ℕ) : ∑ j ∈ range d, y / 2 ^ (j + 1) ≤ y := by + induction d generalizing y with + | zero => simp + | succ d ih => + rw [sum_range_succ'] + have h : ∑ j ∈ range d, y / 2 ^ (j + 1 + 1) = ∑ j ∈ range d, y / 2 / 2 ^ (j + 1) := + sum_congr rfl fun j _ => by rw [Nat.div_div_eq_div_mul, ← pow_succ'] + rw [h] + have := ih (y / 2) + simp only [zero_add, pow_one] + omega + +/-- **`a ≤ 4 ε λ`**: `2 ∑_{j < d} u_j ≤ ⌊λ / 2 ^ 15⌋`. -/ +theorem prefixBits_le (s d : ℕ) : prefixBits s d ≤ Nat.log 2 s / 32768 := by + have h : ∑ j ∈ range d, taper s j ≤ Nat.log 2 s / 65536 := by + have : ∀ j, taper s j = Nat.log 2 s / 65536 / 2 ^ (j + 1) := fun j => by + rw [taper, Nat.div_div_eq_div_mul, show 17 + j = 16 + (j + 1) by omega, pow_add] + rfl + simp only [this] + exact sum_div_two_pow_succ_le _ d + unfold prefixBits + omega + +theorem slotBits_le (s d : ℕ) : slotBits s d ≤ Nat.log 2 s / 32768 := + prefixBits_le s (d + 1) + +/-- **The degree bound is at least `s ^ (9/10)`**: `s ^ 9 ≤ Δ ^ 10`. -/ +theorem pow_nine_le_degreeBound_pow_ten (s : ℕ) : s ^ 9 ≤ degreeBound s ^ 10 := by + have hs : s < 2 ^ (Nat.log 2 s + 1) := Nat.lt_pow_succ_log_self one_lt_two s + calc s ^ 9 ≤ (2 ^ (Nat.log 2 s + 1)) ^ 9 := Nat.pow_le_pow_left hs.le 9 + _ = 2 ^ (9 * Nat.log 2 s + 9) := by rw [← pow_mul]; ring_nf + _ ≤ 2 ^ (10 * (9 * Nat.log 2 s / 10 + 2)) := Nat.pow_le_pow_right two_pos (by omega) + _ = degreeBound s ^ 10 := by rw [degreeBound, ← pow_mul, mul_comm] + +/-- A degree `x` with `x ^ 10 ≤ s ^ 9` is at most the degree bound. -/ +theorem le_degreeBound_of_pow_ten_le {x s : ℕ} (h : x ^ 10 ≤ s ^ 9) : x ≤ degreeBound s := + (Nat.pow_le_pow_iff_left (by norm_num)).1 (h.trans (pow_nine_le_degreeBound_pow_ten s)) + +/-- **The degree bound is at most `2 ^ 2 s ^ (9/10)`**: `Δ ^ 10 ≤ 2 ^ 20 s ^ 9`. -/ +theorem degreeBound_pow_ten_le {s : ℕ} (hs : s ≠ 0) : degreeBound s ^ 10 ≤ 2 ^ 20 * s ^ 9 := by + have h2 : 2 ^ Nat.log 2 s ≤ s := Nat.pow_log_le_self 2 hs + calc degreeBound s ^ 10 = 2 ^ (10 * (9 * Nat.log 2 s / 10) + 20) := by + rw [degreeBound, ← pow_mul]; ring_nf + _ ≤ 2 ^ (9 * Nat.log 2 s + 20) := Nat.pow_le_pow_right two_pos (by omega) + _ = 2 ^ 20 * (2 ^ Nat.log 2 s) ^ 9 := by rw [← pow_mul, ← pow_add]; ring_nf + _ ≤ 2 ^ 20 * s ^ 9 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h2 9) + +/-- **The precision bound** of (D.11), `p ≤ s λ^{O(1)} 2 ^ (a_{d - 1})`: +`precisionBound C s d ≤ C s 2 ^ (a_{d - 1}) (1 + d (8 λ + 40))`. -/ +theorem precisionBound_le (C s d : ℕ) : + precisionBound C s d ≤ C * s * 2 ^ prefixBits s d * (1 + d * (8 * Nat.log 2 s + 40)) := by + induction d with + | zero => simp [precisionBound, prefixBits] + | succ d ih => + set n := Nat.log 2 s + set a := slotBits s d + have ha : a ≤ n := (slotBits_le s d).trans (Nat.div_le_self _ _) + have hpow : 2 ^ prefixBits s d ≤ 2 ^ a := + Nat.pow_le_pow_right two_pos (prefixBits_le_slotBits s d) + have h1 : 1 ≤ 2 ^ a := Nat.one_le_two_pow + have hstep : 8 * (4 * 2 ^ a + a + 1) ≤ 2 ^ a * (8 * n + 40) := by + have : a + 1 ≤ 2 ^ a * (n + 1) := by nlinarith + nlinarith + have hP : precisionBound C s d ≤ C * s * 2 ^ a * (1 + d * (8 * n + 40)) := + ih.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hpow)) + calc precisionBound C s (d + 1) + = precisionBound C s d + C * s * (8 * (4 * 2 ^ a + a + 1)) := by + rw [precisionBound]; ring + _ ≤ C * s * 2 ^ a * (1 + d * (8 * n + 40)) + C * s * (2 ^ a * (8 * n + 40)) := + Nat.add_le_add hP (Nat.mul_le_mul_left _ hstep) + _ = C * s * 2 ^ prefixBits s (d + 1) * (1 + (d + 1) * (8 * n + 40)) := by + rw [show prefixBits s (d + 1) = a from rfl]; ring + +/-! ### Active calls -/ + +section Active + +variable {C s d M p : ℕ} + +theorem Active.one_le_edges (h : Active C s d M p) : 1 ≤ M := + Nat.one_le_iff_ne_zero.2 fun h0 => by have := h.leafSize_lt; omega + +theorem Active.edges_le_mul (h : Active C s d M p) : M ≤ C * s := + (Nat.le_mul_of_pos_left M (Nat.pow_pos (by norm_num))).trans h.edges_le + +theorem Active.one_le_const (h : Active C s d M p) : 1 ≤ C := by + have := h.one_le_edges.trans h.edges_le_mul + rcases Nat.eq_zero_or_pos C with rfl | hC + · simp at this + · exact hC + +/-- At an active call `s < M ⌊√λ⌋`, since `⌊s / ⌊√λ⌋⌋ < M`. -/ +theorem Active.lt_mul_sqrt (h : Active C s d M p) (hs : 2 ≤ s) : + s < M * Nat.sqrt (Nat.log 2 s) := + (Nat.div_lt_iff_lt_mul (Nat.one_le_sqrt_log_two hs)).1 h.leafSize_lt + +/-- **The depth bound**: `16 ^ d < C ⌊√λ⌋` at an active call. -/ +theorem Active.sixteen_pow_lt (h : Active C s d M p) (hs : 2 ≤ s) : + 16 ^ d < C * Nat.sqrt (Nat.log 2 s) := by + have h1 := h.lt_mul_sqrt hs + have h2 : 16 ^ d * s < C * Nat.sqrt (Nat.log 2 s) * s := + calc 16 ^ d * s < 16 ^ d * (M * Nat.sqrt (Nat.log 2 s)) := + Nat.mul_lt_mul_of_pos_left h1 (Nat.pow_pos (by norm_num)) + _ = 16 ^ d * M * Nat.sqrt (Nat.log 2 s) := by ring + _ ≤ C * s * Nat.sqrt (Nat.log 2 s) := Nat.mul_le_mul_right _ h.edges_le + _ = C * Nat.sqrt (Nat.log 2 s) * s := by ring + exact Nat.lt_of_mul_lt_mul_right h2 + +/-- **The taper stays large**: `u_d ≥ ⌊√λ⌋ / (2 ^ 17 C)` at an active call. -/ +theorem Active.le_taper (h : Active C s d M p) (hs : 2 ≤ s) : + Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C) ≤ taper s d := by + set n := Nat.log 2 s + set σ := Nat.sqrt n + have hσ : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hC := h.one_le_const + have h2d : 2 ^ d ≤ C * σ := + (Nat.pow_le_pow_left (by norm_num : 2 ≤ 16) d).trans (h.sixteen_pow_lt hs).le + calc σ / (2 ^ 17 * C) = σ * σ / (2 ^ 17 * C * σ) := (Nat.mul_div_mul_right _ _ hσ).symm + _ ≤ n / (2 ^ 17 * C * σ) := Nat.div_le_div_right (Nat.sqrt_le n) + _ ≤ n / (2 ^ 17 * 2 ^ d) := by + refine Nat.div_le_div_left ?_ (by positivity) + rw [mul_assoc] + exact Nat.mul_le_mul_left _ h2d + _ = taper s d := by rw [taper, pow_add] + +end Active + +/-- `⌊√λ⌋ ≤ 2 ^ (10 + d) ⌊√u_d⌋` once `u_d ≥ 1`: the taper loses at most a factor `2 ^ (17 + d)` +against `λ`. -/ +theorem sqrt_log_two_le_mul_sqrt_taper {s d : ℕ} (hu : 1 ≤ taper s d) : + Nat.sqrt (Nat.log 2 s) ≤ 2 ^ (10 + d) * Nat.sqrt (taper s d) := by + set n := Nat.log 2 s + set u := taper s d + set y := Nat.sqrt u + have hy : 1 ≤ y := Nat.sqrt_pos.2 hu + have hn : n < (u + 1) * 2 ^ (17 + d) := by + have := Nat.lt_div_mul_add (a := n) (b := 2 ^ (17 + d)) (by positivity) + simpa only [u, taper, add_mul, one_mul] using this + have hu1 : u + 1 ≤ 4 * y ^ 2 := by + have := Nat.lt_succ_sqrt' u + nlinarith + have hsq : Nat.sqrt n ^ 2 < (2 ^ (10 + d) * y) ^ 2 := by + calc Nat.sqrt n ^ 2 ≤ n := Nat.sqrt_le' n + _ < (u + 1) * 2 ^ (17 + d) := hn + _ ≤ 4 * y ^ 2 * 2 ^ (17 + d) := Nat.mul_le_mul_right _ hu1 + _ = 2 ^ (19 + d) * y ^ 2 := by rw [show 19 + d = 2 + (17 + d) by omega, pow_add]; ring + _ ≤ 2 ^ (20 + 2 * d) * y ^ 2 := Nat.mul_le_mul_right _ (Nat.pow_le_pow_right two_pos + (by omega)) + _ = (2 ^ (10 + d) * y) ^ 2 := by rw [mul_pow, ← pow_mul]; ring_nf + exact ((Nat.pow_lt_pow_iff_left (by norm_num)).1 hsq).le + +/-! ### The certificate -/ + +/-- The inequalities that hold at an active call at depth `d` with `M` edges and precision `p`, for +`s` large enough. Write `u = taper s d`, `a = slotBits s d`, `L = 2 ^ a`, `Δ = degreeBound s` and +`λ = ⌊log₂ s⌋`. -/ +structure ActiveBounds (C s d M p : ℕ) : Prop where + /-- The call and its children lie in the first `λ` levels. -/ + depth_add_two_le : d + 2 ≤ Nat.log 2 s + /-- `1 ≤ u`, as Lemma D.5 requires. -/ + one_le_taper : 1 ≤ taper s d + /-- `u ≤ M`, as Lemma D.5 requires. -/ + taper_le_edges : taper s d ≤ M + /-- (D.6): `2 Δ D_arr² ≤ M`. -/ + degree_mul_pairs_sq_le : 2 * degreeBound s * (64 ^ (2 * slotBits s d)) ^ 2 ≤ M + /-- (D.6): `L D_arr ≤ M`. -/ + slots_mul_pairs_le : 2 ^ slotBits s d * 64 ^ (2 * slotBits s d) ≤ M + /-- (D.6): `2 L ≤ Δ`, so packet vertices respect the degree bound. -/ + two_mul_slots_le : 2 * 2 ^ slotBits s d ≤ degreeBound s + /-- There are `2 ^ (4 λ)` residue-field lifts for the `M (2 L - 1) + 1` interpolation points. -/ + points_le : M * (2 * 2 ^ slotBits s d - 1) + 1 ≤ 2 ^ (4 * Nat.log 2 s) + /-- The nodes, interpolation points and `64` groups contribute a factor `2 ^ (2 λ)` to the + branching. -/ + branching_le : + 2 * 2 ^ slotBits s d * (M * (2 * 2 ^ slotBits s d - 1) + 1) * 64 ≤ 2 ^ (2 * Nat.log 2 s) + /-- The children's precisions are within the schedule. -/ + nodePrecision_le : ∀ i h, i < taper s d → h * taper s d ≤ 3 * M + taper s d → + nodePrecision p h (slotBits s d) M i ≤ precisionBound C s (d + 1) + /-- **(D.11)**: `p_t u ≤ 34 M D_t`. -/ + nodePrecision_mul_taper_le : ∀ i h, i < taper s d → h * taper s d ≤ 3 * M + taper s d → + nodePrecision p h (slotBits s d) M i * taper s d ≤ 34 * M * 2 ^ (slotBits s d - i) + +/-! #### Arithmetic lemmas -/ + +private theorem one_add_mul_le_sq (n : ℕ) : 1 + n * (8 * n + 40) ≤ 49 * (n + 1) ^ 2 := by + nlinarith + +private theorem one_add_mul_le_sq' {n : ℕ} (hn : 1 ≤ n) : 1 + n * (8 * n + 40) ≤ 49 * n ^ 2 := by + nlinarith + +/-- The children's precisions are within the schedule. -/ +private theorem nodePrecision_le_of {p P h u M C s a i : ℕ} (hp : p ≤ P) + (hh : h * u ≤ 3 * M + u) (hu : 1 ≤ u) (huM : u ≤ M) (hM : M ≤ C * s) : + nodePrecision p h a M i ≤ P + 8 * C * s * (4 * 2 ^ a + a + 1) := by + have hh4 : h ≤ 4 * M := by + have : h ≤ h * u := Nat.le_mul_of_pos_right h hu + omega + have hDt : 2 ^ (a - i) ≤ 2 ^ a := Nat.pow_le_pow_right two_pos (Nat.sub_le a i) + calc nodePrecision p h a M i = p + 8 * h * 2 ^ (a - i) + 8 * M * (a + 1) := rfl + _ ≤ P + 8 * (4 * (C * s)) * 2 ^ a + 8 * (C * s) * (a + 1) := + Nat.add_le_add (Nat.add_le_add hp (Nat.mul_le_mul + (Nat.mul_le_mul_left 8 (hh4.trans (Nat.mul_le_mul_left 4 hM))) hDt)) + (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left 8 hM)) + _ = P + 8 * C * s * (4 * 2 ^ a + a + 1) := by ring + +/-- The inherited precision is absorbed by the taper: `p u ≤ M 2 ^ (a_{d-1} + u)`. -/ +private theorem mul_taper_le_of {p C s A d n σ u M : ℕ} + (hp : p ≤ C * s * 2 ^ A * (1 + d * (8 * n + 40))) (hsM : s ≤ M * σ) (hσ : σ ≤ n) + (hd : d ≤ n) (hu : u ≤ n) (hn : 1 ≤ n) (hpow : 49 * C * n ^ 4 ≤ 2 ^ u) : + p * u ≤ M * 2 ^ (A + u) := by + have h0 : d * (8 * n + 40) ≤ n * (8 * n + 40) := Nat.mul_le_mul_right _ hd + have h1 : 1 + d * (8 * n + 40) ≤ 49 * n ^ 2 := (Nat.add_le_add_left h0 1).trans + (one_add_mul_le_sq' hn) + have h2 : σ * u ≤ n ^ 2 := by rw [sq]; exact Nat.mul_le_mul hσ hu + have hfac : C * σ * (1 + d * (8 * n + 40)) * u ≤ 49 * C * n ^ 4 := + calc C * σ * (1 + d * (8 * n + 40)) * u = C * (σ * u) * (1 + d * (8 * n + 40)) := by ring + _ ≤ C * n ^ 2 * (49 * n ^ 2) := Nat.mul_le_mul (Nat.mul_le_mul_left _ h2) h1 + _ = 49 * C * n ^ 4 := by ring + calc p * u ≤ C * s * 2 ^ A * (1 + d * (8 * n + 40)) * u := Nat.mul_le_mul_right _ hp + _ ≤ C * (M * σ) * 2 ^ A * (1 + d * (8 * n + 40)) * u := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ + (Nat.mul_le_mul_left C hsM))) + _ = M * 2 ^ A * (C * σ * (1 + d * (8 * n + 40)) * u) := by ring + _ ≤ M * 2 ^ A * 2 ^ u := Nat.mul_le_mul_left _ (hfac.trans hpow) + _ = M * 2 ^ (A + u) := by rw [mul_assoc, ← pow_add] + +/-- The evaluation loss is absorbed by the taper: `8 (a + 1) u ≤ 2 ^ u`. -/ +private theorem eight_mul_le_two_pow {a u n C : ℕ} (hC : 1 ≤ C) (hn : 1 ≤ n) (ha : a ≤ n) + (hu : u ≤ n) (hpow : 49 * C * n ^ 4 ≤ 2 ^ u) : 8 * (a + 1) * u ≤ 2 ^ u := by + have h1 : 8 * (a + 1) * u ≤ 16 * n ^ 2 := by + calc 8 * (a + 1) * u ≤ 8 * (n + n) * n := + Nat.mul_le_mul (Nat.mul_le_mul_left 8 (Nat.add_le_add ha hn)) hu + _ = 16 * n ^ 2 := by ring + have h2 : n ^ 2 ≤ n ^ 4 := Nat.pow_le_pow_right hn (by norm_num) + have h3 : 16 * n ^ 4 ≤ 49 * C * n ^ 4 := + Nat.mul_le_mul_right _ (by omega) + omega + +/-- **(D.11)** from its ingredients: `p_t u ≤ 34 M D_t`. -/ +private theorem nodePrecision_mul_le_of {p h a M i u A : ℕ} (hpu : p * u ≤ M * 2 ^ (A + u)) + (ha : a = A + 2 * u) (hi : i < u) (hh : h * u ≤ 3 * M + u) (huM : u ≤ M) + (h8 : 8 * (a + 1) * u ≤ 2 ^ u) : + nodePrecision p h a M i * u ≤ 34 * M * 2 ^ (a - i) := by + have hDt : 2 ^ (A + u) ≤ 2 ^ (a - i) := Nat.pow_le_pow_right two_pos (by omega) + have hu2 : 2 ^ u ≤ 2 ^ (a - i) := Nat.pow_le_pow_right two_pos (by omega) + have hhu : h * u ≤ 4 * M := by omega + calc nodePrecision p h a M i * u + = p * u + 8 * (h * u) * 2 ^ (a - i) + M * (8 * (a + 1) * u) := by + rw [nodePrecision]; ring + _ ≤ M * 2 ^ (a - i) + 8 * (4 * M) * 2 ^ (a - i) + M * 2 ^ (a - i) := + Nat.add_le_add (Nat.add_le_add (hpu.trans (Nat.mul_le_mul_left _ hDt)) + (Nat.mul_le_mul_right _ (Nat.mul_le_mul_left 8 hhu))) + (Nat.mul_le_mul_left _ (h8.trans hu2)) + _ = 34 * M * 2 ^ (a - i) := by ring + +/-- `64 ^ (2 a) = 2 ^ (12 a)`. -/ +private theorem sixtyFour_pow (a : ℕ) : 64 ^ (2 * a) = 2 ^ (12 * a) := by + rw [show (64 : ℕ) = 2 ^ 6 by norm_num, ← pow_mul]; ring_nf + +/-- A power of two is below `M` when it is below `s / 2 ^ (n / 20)`, since `s < M σ` and +`σ ≤ 2 ^ (n / 20)`. -/ +private theorem two_pow_lt_of {k n s M σ : ℕ} (hk : k + n / 20 ≤ n) (hσ : σ ≤ 2 ^ (n / 20)) + (h2n : 2 ^ n ≤ s) (hsM : s < M * σ) : 2 ^ k < M := by + have : 2 ^ k * σ < M * σ := + calc 2 ^ k * σ ≤ 2 ^ k * 2 ^ (n / 20) := Nat.mul_le_mul_left _ hσ + _ = 2 ^ (k + n / 20) := (pow_add _ _ _).symm + _ ≤ 2 ^ n := Nat.pow_le_pow_right two_pos hk + _ ≤ s := h2n + _ < M * σ := hsM + exact Nat.lt_of_mul_lt_mul_right this + +/-- The interpolation points: `M (2 L - 1) + 1 ≤ 2 ^ (n / 8 + n + a + 2)`. -/ +private theorem points_le_of {M a C s n : ℕ} (hM1 : 1 ≤ M) (hM : M ≤ C * s) + (hC : C ≤ 2 ^ (n / 8)) (hs : s < 2 ^ (n + 1)) : + M * (2 * 2 ^ a - 1) + 1 ≤ 2 ^ (n / 8 + n + a + 2) := by + have h1 : M * (2 * 2 ^ a - 1) + 1 ≤ M * (2 * 2 ^ a) := by + have h2a : 1 ≤ 2 * 2 ^ a := by have := Nat.one_le_two_pow (n := a); omega + rw [Nat.mul_sub, mul_one] + have : M ≤ M * (2 * 2 ^ a) := Nat.le_mul_of_pos_right M (by omega) + omega + calc M * (2 * 2 ^ a - 1) + 1 ≤ M * (2 * 2 ^ a) := h1 + _ ≤ C * s * (2 * 2 ^ a) := Nat.mul_le_mul_right _ hM + _ ≤ 2 ^ (n / 8) * 2 ^ (n + 1) * (2 * 2 ^ a) := + Nat.mul_le_mul_right _ (Nat.mul_le_mul hC hs.le) + _ = 2 ^ (n / 8 + n + a + 2) := by + rw [← pow_succ', ← pow_add, ← pow_add]; ring_nf + +/-- The asymptotic inequalities behind the certificate, in `n = ⌊log₂ s⌋`. -/ +private theorem eventually_large (C : ℕ) (hC : 1 ≤ C) : ∀ᶠ n : ℕ in atTop, + 200 ≤ n ∧ 49 * C * (Nat.sqrt n + 1) ^ 8 ≤ 2 ^ (Nat.sqrt n / (2 ^ 17 * C)) ∧ + C * (n + 1) ^ 1 ≤ 2 ^ (n / 8) ∧ 8 * (n + 1) ^ 1 ≤ 2 ^ (n / 20) ∧ + 49 * C * (n + 1) ^ 2 ≤ 2 ^ (n / 2) := by + have hsqrt : Tendsto Nat.sqrt atTop atTop := + tendsto_atTop_atTop.2 fun b => ⟨b * b, fun n hn => Nat.le_sqrt.2 hn⟩ + filter_upwards [eventually_ge_atTop 200, + hsqrt.eventually (Nat.eventually_mul_add_one_pow_le_pow_div (49 * C) 8 (2 ^ 17 * C) + one_lt_two (by positivity)), + Nat.eventually_mul_add_one_pow_le_pow_div C 1 8 one_lt_two (by norm_num), + Nat.eventually_mul_add_one_pow_le_pow_div 8 1 20 one_lt_two (by norm_num), + Nat.eventually_mul_add_one_pow_le_pow_div (49 * C) 2 2 one_lt_two (by norm_num)] + with n h1 h2 h3 h4 h5 + exact ⟨h1, h2, h3, h4, h5⟩ + +/-! #### The certificate -/ + +/-- Precisions up to depth `⌊log₂ s⌋` are at most `s ^ 2` once `49 C (λ + 1)² ≤ 2 ^ (λ / 2)`. -/ +private theorem precisionBound_le_sq_of {C s d : ℕ} (hd : d ≤ Nat.log 2 s) (hs : s ≠ 0) + (h : 49 * C * (Nat.log 2 s + 1) ^ 2 ≤ 2 ^ (Nat.log 2 s / 2)) : + precisionBound C s d ≤ s ^ 2 := by + set n := Nat.log 2 s + have h2n : 2 ^ n ≤ s := Nat.pow_log_le_self 2 hs + have hpow : 2 ^ prefixBits s d ≤ 2 ^ (n / 32768) := + Nat.pow_le_pow_right two_pos (prefixBits_le s d) + have hfac : C * (1 + d * (8 * n + 40)) ≤ 49 * C * (n + 1) ^ 2 := by + have h1 : d * (8 * n + 40) ≤ n * (8 * n + 40) := Nat.mul_le_mul_right _ hd + have h2 := one_add_mul_le_sq n + calc C * (1 + d * (8 * n + 40)) ≤ C * (49 * (n + 1) ^ 2) := + Nat.mul_le_mul_left _ (by omega) + _ = 49 * C * (n + 1) ^ 2 := by ring + calc precisionBound C s d ≤ C * s * 2 ^ prefixBits s d * (1 + d * (8 * n + 40)) := + precisionBound_le C s d + _ = s * (C * (1 + d * (8 * n + 40))) * 2 ^ prefixBits s d := by ring + _ ≤ s * 2 ^ (n / 2) * 2 ^ (n / 32768) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ (hfac.trans h)) hpow + _ = s * 2 ^ (n / 2 + n / 32768) := by rw [mul_assoc, ← pow_add] + _ ≤ s * 2 ^ n := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right two_pos (by omega)) + _ ≤ s * s := Nat.mul_le_mul_left _ h2n + _ = s ^ 2 := (sq s).symm + +/-- The certificate at one active call, from the asymptotic inequalities at `λ = ⌊log₂ s⌋`. -/ +private theorem activeBounds_of {C s d M p : ℕ} (hA : Active C s d M p) + (h200 : 200 ≤ Nat.log 2 s) + (hA1 : 49 * C * (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 ≤ + 2 ^ (Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C))) + (hA2 : C * (Nat.log 2 s + 1) ≤ 2 ^ (Nat.log 2 s / 8)) + (hA3 : 8 * (Nat.log 2 s + 1) ≤ 2 ^ (Nat.log 2 s / 20)) : + ActiveBounds C s d M p := by + have hs0 : s ≠ 0 := by + rintro rfl + simp at h200 + have hC := hA.one_le_const + have hM1 := hA.one_le_edges + have hMCs := hA.edges_le_mul + have h2n : 2 ^ Nat.log 2 s ≤ s := Nat.pow_log_le_self 2 hs0 + have hsn : s < 2 ^ (Nat.log 2 s + 1) := Nat.lt_pow_succ_log_self one_lt_two s + have hs2 : 2 ≤ s := (Nat.pow_le_pow_right two_pos (by omega : 1 ≤ Nat.log 2 s)).trans h2n + have hsM := hA.lt_mul_sqrt hs2 + have h16 := hA.sixteen_pow_lt hs2 + have hσn : Nat.sqrt (Nat.log 2 s) ≤ Nat.log 2 s := Nat.sqrt_le_self _ + have hnσ : Nat.log 2 s < (Nat.sqrt (Nat.log 2 s) + 1) ^ 2 := Nat.lt_succ_sqrt' _ + have hσpow : Nat.sqrt (Nat.log 2 s) ≤ 2 ^ (Nat.log 2 s / 20) := by omega + have hCpow : C ≤ 2 ^ (Nat.log 2 s / 8) := (Nat.le_mul_of_pos_right C (by omega)).trans hA2 + have haA : slotBits s d = prefixBits s d + 2 * taper s d := slotBits_eq s d + have ha : slotBits s d ≤ Nat.log 2 s / 32768 := slotBits_le s d + have han : slotBits s d ≤ Nat.log 2 s := ha.trans (Nat.div_le_self _ _) + -- The depth. + have hdepth : d + 2 ≤ Nat.log 2 s := by + have h1 : 2 ^ (4 * d) < 2 ^ (Nat.log 2 s / 8) := by + calc 2 ^ (4 * d) = 16 ^ d := by rw [pow_mul]; norm_num + _ < C * Nat.sqrt (Nat.log 2 s) := h16 + _ ≤ C * (Nat.log 2 s + 1) := Nat.mul_le_mul_left _ (by omega) + _ ≤ 2 ^ (Nat.log 2 s / 8) := hA2 + have := (Nat.pow_lt_pow_iff_right one_lt_two).1 h1 + omega + -- The taper. + have hpowu : 49 * C * Nat.log 2 s ^ 4 ≤ 2 ^ taper s d := by + have hn4 : Nat.log 2 s ^ 4 ≤ (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := by + calc Nat.log 2 s ^ 4 ≤ ((Nat.sqrt (Nat.log 2 s) + 1) ^ 2) ^ 4 := + Nat.pow_le_pow_left hnσ.le 4 + _ = (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := by rw [← pow_mul] + calc 49 * C * Nat.log 2 s ^ 4 ≤ 49 * C * (Nat.sqrt (Nat.log 2 s) + 1) ^ 8 := + Nat.mul_le_mul_left _ hn4 + _ ≤ 2 ^ (Nat.sqrt (Nat.log 2 s) / (2 ^ 17 * C)) := hA1 + _ ≤ 2 ^ taper s d := Nat.pow_le_pow_right two_pos (hA.le_taper hs2) + have hu1 : 1 ≤ taper s d := by + by_contra hu0 + have h0 : taper s d = 0 := by omega + rw [h0, pow_zero] at hpowu + have : 1 ≤ Nat.log 2 s ^ 4 := Nat.one_le_pow _ _ (by omega) + have : 49 ≤ 49 * C * Nat.log 2 s ^ 4 := + calc 49 = 49 * 1 * 1 := rfl + _ ≤ 49 * C * Nat.log 2 s ^ 4 := Nat.mul_le_mul (Nat.mul_le_mul_left _ hC) this + omega + have hun : taper s d ≤ Nat.log 2 s := Nat.div_le_self _ _ + have huM : taper s d ≤ M := by + have := Nat.log_two_le_div_sqrt_log_two s + have := hA.leafSize_lt + simp only [leafSize] at this + omega + have hpu : p * taper s d ≤ M * 2 ^ (prefixBits s d + taper s d) := + mul_taper_le_of (hA.precision_le.trans (precisionBound_le C s d)) hsM.le hσn + (by omega) hun (by omega) hpowu + have h8 : 8 * (slotBits s d + 1) * taper s d ≤ 2 ^ taper s d := + eight_mul_le_two_pow hC (by omega) han hun hpowu + have hpoints := points_le_of (a := slotBits s d) hM1 hMCs hCpow hsn + refine ⟨hdepth, hu1, huM, ?_, ?_, ?_, ?_, ?_, fun i h _ hh => ?_, fun i h hi hh => ?_⟩ + · -- `2 Δ D_arr² ≤ M`. + have := two_pow_lt_of (k := 3 + 9 * Nat.log 2 s / 10 + 24 * slotBits s d) (by omega) + hσpow h2n hsM + rw [degreeBound, sixtyFour_pow] + calc 2 * 2 ^ (9 * Nat.log 2 s / 10 + 2) * (2 ^ (12 * slotBits s d)) ^ 2 + = 2 ^ (3 + 9 * Nat.log 2 s / 10 + 24 * slotBits s d) := by + rw [← pow_mul, ← pow_succ', ← pow_add]; ring_nf + _ ≤ M := this.le + · -- `L D_arr ≤ M`. + have := two_pow_lt_of (k := 13 * slotBits s d) (by omega) hσpow h2n hsM + rw [sixtyFour_pow, ← pow_add] + calc 2 ^ (slotBits s d + 12 * slotBits s d) = 2 ^ (13 * slotBits s d) := by ring_nf + _ ≤ M := this.le + · -- `2 L ≤ Δ`. + rw [degreeBound, ← pow_succ'] + exact Nat.pow_le_pow_right two_pos (by omega) + · -- Interpolation points. + exact hpoints.trans (Nat.pow_le_pow_right two_pos (by omega)) + · -- The polynomial branching factor. + calc 2 * 2 ^ slotBits s d * (M * (2 * 2 ^ slotBits s d - 1) + 1) * 64 + ≤ 2 * 2 ^ slotBits s d * 2 ^ (Nat.log 2 s / 8 + Nat.log 2 s + slotBits s d + 2) * 64 := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hpoints) + _ = 2 ^ (Nat.log 2 s / 8 + Nat.log 2 s + 2 * slotBits s d + 9) := by + rw [show (64 : ℕ) = 2 ^ 6 by norm_num, ← pow_succ', ← pow_add, ← pow_add]; ring_nf + _ ≤ 2 ^ (2 * Nat.log 2 s) := Nat.pow_le_pow_right two_pos (by omega) + · -- Children's precisions. + exact nodePrecision_le_of hA.precision_le hh hu1 huM hMCs + · -- (D.11). + exact nodePrecision_mul_le_of hpu haA hi hh huM h8 + +/-- **The parameter certificate.** For every `C` there is `s₀` such that for all `s ≥ s₀` the +precisions up to depth `⌊log₂ s⌋` are at most `s ^ 2`, and every active call satisfies +`ActiveBounds`. -/ +theorem exists_activeBounds (C : ℕ) : ∃ s₀, ∀ s, s₀ ≤ s → + (∀ d ≤ Nat.log 2 s, precisionBound C s d ≤ s ^ 2) ∧ + ∀ d M p, Active C s d M p → ActiveBounds C s d M p := by + rcases Nat.eq_zero_or_pos C with rfl | hC + · refine ⟨0, fun s _ => ⟨fun d _ => ?_, fun d M p h => absurd h.one_le_const (by norm_num)⟩⟩ + have := precisionBound_le 0 s d + simp only [zero_mul] at this + exact this.trans (Nat.zero_le _) + obtain ⟨n₀, hn₀⟩ := eventually_atTop.1 (eventually_large C hC) + refine ⟨2 ^ n₀, fun s hs => ?_⟩ + have hs0 : s ≠ 0 := by + rintro rfl + have := Nat.one_le_two_pow (n := n₀) + omega + obtain ⟨h200, hA1, hA2, hA3, hA5⟩ := hn₀ (Nat.log 2 s) (Nat.le_log_of_pow_le one_lt_two hs) + simp only [pow_one] at hA2 hA3 + exact ⟨fun d hd => precisionBound_le_sq_of hd hs0 hA5, + fun d M p hA => activeBounds_of hA h200 hA1 hA2 hA3⟩ + +/-! ### The mode count -/ + +/-- **The mode count (D.15)** at an active call: if the node `t` of valuation `i ≤ a` satisfies +the precision bound (D.11) `p_t u ≤ 34 M D_t` with `u ≥ 1`, and the packing has `#P 2 ^ a ≤ 3 M` +packets (Lemma D.3 (1)), then there are at most `2 ^ e_d` tuples of exponents of the modes +`P × Fin (2 ^ (i + 1)) × Fin p_t` (packet, tile, `b`) of weight `b + 1` below `p_t`. There are +`#P 2 ^ (i + 1) ≤ 6 M / D_t` modes of each weight (D.13). -/ +theorem card_modeBudget_le {C s d M p : ℕ} (hA : Active C s d M p) (hs : 2 ≤ s) + (hu : 1 ≤ taper s d) {i h : ℕ} (hi : i ≤ slotBits s d) + (hpt : nodePrecision p h (slotBits s d) M i * taper s d ≤ + 34 * M * 2 ^ (slotBits s d - i)) + {P : Type*} [Fintype P] [DecidableEq P] + (hP : Fintype.card P * 2 ^ slotBits s d ≤ 3 * M) : + #(TensorNetwork.modeBudget + (fun Z : P × Fin (2 ^ (i + 1)) × Fin (nodePrecision p h (slotBits s d) M i) => + (Z.2.2 : ℕ) + 1) + (nodePrecision p h (slotBits s d) M i)) ≤ 2 ^ branchExponent C s d := by + set a := slotBits s d + set pt := nodePrecision p h a M i + set u := taper s d + set m := Fintype.card P * 2 ^ (i + 1) + set σ := Nat.sqrt (Nat.log 2 s) + -- At most `m` modes of each weight. + have hfib : ∀ j, #{Z : P × Fin (2 ^ (i + 1)) × Fin pt | (Z.2.2 : ℕ) + 1 = j} ≤ m := by + intro j + calc #{Z : P × Fin (2 ^ (i + 1)) × Fin pt | (Z.2.2 : ℕ) + 1 = j} + ≤ #(univ : Finset (P × Fin (2 ^ (i + 1)))) := by + refine card_le_card_of_injOn (fun Z => (Z.1, Z.2.1)) (fun _ _ => mem_univ _) ?_ + intro Z hZ Z' hZ' hZZ + have hZ := (mem_filter.1 (mem_coe.1 hZ)).2 + have hZ' := (mem_filter.1 (mem_coe.1 hZ')).2 + simp only [Prod.mk.injEq] at hZZ + exact Prod.ext hZZ.1 (Prod.ext hZZ.2 (Fin.ext (by omega))) + _ = m := by simp [m] + have hcard := card_le_two_pow_of_sum_mul_lt (fun _ => Nat.succ_pos _) hfib + (S := TensorNetwork.modeBudget _ pt) fun β hβ => + (TensorNetwork.mem_modeBudget (fun _ => Nat.succ_pos _)).1 hβ + refine hcard.trans (Nat.pow_le_pow_right two_pos ?_) + -- `⌊√(m p_t)⌋ ⌊√u⌋ ≤ 15 M`. + set x := Nat.sqrt (m * pt) + set y := Nat.sqrt u + have hmD : m * 2 ^ (a - i) ≤ 6 * M := by + have : m * 2 ^ (a - i) = 2 * (Fintype.card P * 2 ^ a) := by + rw [show a = i + (a - i) by omega, Nat.add_sub_cancel_left] + simp only [m, pow_succ, pow_add] + ring + omega + have hxy : x * y ≤ 15 * M := by + have h1 : (x * y) ^ 2 ≤ m * pt * u := by + rw [mul_pow] + exact Nat.mul_le_mul (Nat.sqrt_le' _) (Nat.sqrt_le' _) + have h2 : m * pt * u ≤ 204 * M ^ 2 := + calc m * pt * u = m * (pt * u) := by ring + _ ≤ m * (34 * M * 2 ^ (a - i)) := Nat.mul_le_mul_left _ hpt + _ = 34 * M * (m * 2 ^ (a - i)) := by ring + _ ≤ 34 * M * (6 * M) := Nat.mul_le_mul_left _ hmD + _ = 204 * M ^ 2 := by ring + have h3 : (x * y) ^ 2 ≤ (15 * M) ^ 2 := by + rw [mul_pow (15 : ℕ)] + omega + exact (Nat.pow_le_pow_iff_left (by norm_num)).1 h3 + have hσ : σ ≤ 2 ^ (10 + d) * y := sqrt_log_two_le_mul_sqrt_taper hu + have hσ1 : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hx : x ≤ 15360 * C * s / (σ * 8 ^ d) := by + rw [Nat.le_div_iff_mul_le (by positivity)] + calc x * (σ * 8 ^ d) ≤ x * (2 ^ (10 + d) * y * 8 ^ d) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_right _ hσ) + _ = x * y * 2 ^ 10 * (2 ^ d * 8 ^ d) := by rw [pow_add]; ring + _ ≤ 15 * M * 2 ^ 10 * 16 ^ d := by + rw [← mul_pow] + exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hxy) + _ = 15360 * (16 ^ d * M) := by ring + _ ≤ 15360 * (C * s) := Nat.mul_le_mul_left _ hA.edges_le + _ = 15360 * C * s := by ring + change 4 * x + 4 ≤ 4 * (15360 * C * s / (σ * 8 ^ d)) + 4 + omega + +/-- **The excess exponents sum to `O(s / √⌊log₂ s⌋)`**: over at most `⌊log₂ s⌋` levels, +`∑_d e_d ≤ (245760 C + 4) ⌊s / ⌊√⌊log₂ s⌋⌋⌋`. The terms decrease geometrically, as in the +manuscript's `(√2 / 8) ^ d` (§D.4.7, p. 64). -/ +theorem sum_branchExponent_le (C : ℕ) {s D : ℕ} (hs : 2 ≤ s) (hD : D ≤ Nat.log 2 s) : + ∑ d ∈ range D, branchExponent C s d ≤ + (245760 * C + 4) * (s / Nat.sqrt (Nat.log 2 s)) := by + set σ := Nat.sqrt (Nat.log 2 s) + set S := s / σ + set X := 15360 * C * s / σ + have hσ1 : 1 ≤ σ := Nat.one_le_sqrt_log_two hs + have hS1 : 1 ≤ S := Nat.one_le_div_sqrt_log_two hs + have hDS : D ≤ S := hD.trans (Nat.log_two_le_div_sqrt_log_two s) + have hX : X ≤ 15360 * C * S + 15360 * C := Nat.mul_div_le_mul_div_add _ _ _ + have hterm : ∀ d, 15360 * C * s / (σ * 8 ^ d) ≤ X / 2 ^ d := fun d => by + rw [← Nat.div_div_eq_div_mul] + exact Nat.div_le_div_left (Nat.pow_le_pow_left (by norm_num) d) (by positivity) + have hgeo : ∑ d ∈ range D, X / 2 ^ d ≤ 2 * X := by + have h := sum_div_two_pow_succ_le (2 * X) D + have heq : ∀ d, 2 * X / 2 ^ (d + 1) = X / 2 ^ d := fun d => by + rw [pow_succ', Nat.mul_div_mul_left X (2 ^ d) two_pos] + simpa only [heq] using h + calc ∑ d ∈ range D, branchExponent C s d + = 4 * ∑ d ∈ range D, 15360 * C * s / (σ * 8 ^ d) + 4 * D := by + simp only [branchExponent, sum_add_distrib, ← mul_sum, sum_const, card_range, + smul_eq_mul] + ring + _ ≤ 4 * (2 * X) + 4 * S := + Nat.add_le_add (Nat.mul_le_mul_left _ ((sum_le_sum fun d _ => hterm d).trans hgeo)) + (Nat.mul_le_mul_left _ hDS) + _ ≤ (245760 * C + 4) * S := by + have hCS : C ≤ C * S := Nat.le_mul_of_pos_right C hS1 + have h1 : 15360 * C * S = 15360 * (C * S) := by ring + have h2 : (245760 * C + 4) * S = 245760 * (C * S) + 4 * S := by ring + omega + +end Cslib.Circuits.Frontier.ContractionSchedule diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean new file mode 100644 index 0000000000..ef6a4eedd9 --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkSchedule.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Schedule + +/-! +# Tests for the parameter schedule of the contraction recursion + +Concrete values of the schedule at `s = 2 ^ 10`, an active call there, and a nonvacuity check of +the certificate: some root call satisfies `ActiveBounds`. +-/ + +@[expose] public section + +namespace ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Schedule + +open Cslib.Circuits.Frontier.ContractionSchedule + +/-! ### Values at `s = 2 ^ 10`, where `⌊log₂ s⌋ = 10` and `⌊√10⌋ = 3` -/ + +theorem log_two_1024 : Nat.log 2 1024 = 10 := by + rw [show (1024 : ℕ) = 2 ^ 10 by norm_num, Nat.log_pow one_lt_two] + +theorem sqrt_10 : Nat.sqrt 10 = 3 := + (Nat.eq_sqrt.2 ⟨by norm_num, by norm_num⟩).symm + +example : leafSize 1024 = 341 := by + rw [leafSize, log_two_1024, sqrt_10] + +/-- `ε λ` is far below one at this size, so the taper and the labels are trivial. -/ +example (d : ℕ) : taper 1024 d = 0 := by + rw [taper, log_two_1024] + exact Nat.div_eq_of_lt (lt_of_lt_of_le (by norm_num) (Nat.pow_le_pow_right two_pos + (Nat.le_add_right 17 d))) + +example : degreeBound 1024 = 2 ^ 11 := by + rw [degreeBound, log_two_1024] + +example : precisionBound 3 1024 0 = 3072 := rfl + +/-- One level adds `8 C s (4 · 2 ^ a_0 + a_0 + 1)` with `a_0 = 0`. -/ +example : precisionBound 3 1024 1 = 3072 + 8 * 3 * 1024 * 5 := by + have h : slotBits 1024 0 = 0 := by + simp [slotBits, prefixBits, taper, log_two_1024] + simp [precisionBound, h] + +example : nodePrecision 5 2 3 7 1 = 5 + 8 * 2 * 4 + 8 * 7 * 4 := rfl + +/-- `Δ ^ 10 ≥ s ^ 9` and `Δ ^ 10 ≤ 2 ^ 20 s ^ 9`. -/ +example : 1024 ^ 9 ≤ degreeBound 1024 ^ 10 ∧ degreeBound 1024 ^ 10 ≤ 2 ^ 20 * 1024 ^ 9 := + ⟨pow_nine_le_degreeBound_pow_ten 1024, degreeBound_pow_ten_le (by norm_num)⟩ + +/-! ### Active calls -/ + +/-- A root call with `1000` edges and precision `5` at `s = 1024`, `C = 1`. -/ +example : Active 1 1024 0 1000 5 := + Active.root (by norm_num) (by rw [show leafSize 1024 = 341 by + rw [leafSize, log_two_1024, sqrt_10]]; norm_num) (by norm_num) + +/-- A child with `62` edges is not active at `s = 1024`: it is a leaf. -/ +example : ¬ Active 1 1024 1 62 5 := fun h => by + have := h.leafSize_lt + rw [show leafSize 1024 = 341 by rw [leafSize, log_two_1024, sqrt_10]] at this + omega + +/-- **The certificate is not vacuous**: for each `C ≥ 1` some root call satisfies +`ActiveBounds`. -/ +example (C : ℕ) (hC : 1 ≤ C) : ∃ s M p, ActiveBounds C s 0 M p := by + obtain ⟨s₀, h⟩ := exists_activeBounds C + set s := max s₀ 16 + have hs : 16 ≤ s := le_max_right _ _ + have hlog : 4 ≤ Nat.log 2 s := Nat.le_log_of_pow_le one_lt_two (by simpa using hs) + have hσ : 2 ≤ Nat.sqrt (Nat.log 2 s) := Nat.le_sqrt.2 (by omega) + refine ⟨s, s, 0, (h s (le_max_left _ _)).2 0 s 0 (Active.root ?_ ?_ (Nat.zero_le _))⟩ + · exact Nat.le_mul_of_pos_left s hC + · exact Nat.div_lt_self (by omega) (by omega) + +/-- The excess exponents at `s = 1024` and `C = 1` over two levels. -/ +example : ∑ d ∈ Finset.range 2, branchExponent 1 1024 d ≤ 245764 * (1024 / Nat.sqrt 10) := by + have := sum_branchExponent_le 1 (s := 1024) (D := 2) (by norm_num) + (by rw [log_two_1024]; norm_num) + rwa [log_two_1024] at this + +end ComplexityTests.Computability.Circuit.Frontier.TensorNetwork.Schedule From d9a734324a1bf53b70ff5ca89acdb2166b57587b Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 23:02:48 -0400 Subject: [PATCH 3/3] feat(circuit/frontier): mode count at a certified active call ActiveBounds.card_modeBudget_le supplies the hypotheses of card_modeBudget_le from the certificate, and ActiveBounds.two_le. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/Schedule.lean | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean index 6fa306e299..66eafea95a 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/Schedule.lean @@ -78,7 +78,8 @@ precision bound `p ≤ s λ^{O(1)} 2 ^ (a_{d-1})` is `precisionBound_le`. ## Main results * `exists_activeBounds`: the parameter certificate. -* `card_modeBudget_le`: the mode count (D.15) at an active call. +* `card_modeBudget_le`, `ActiveBounds.card_modeBudget_le`: the mode count (D.15) at an active + call. * `sum_branchExponent_le`: the excess exponents sum to `O(s / √⌊log₂ s⌋)`. * `precisionBound_le`: the precision bound `p ≤ C s 2 ^ (a_{d-1}) (1 + d (8 λ + 40))`. @@ -686,6 +687,28 @@ theorem card_modeBudget_le {C s d M p : ℕ} (hA : Active C s d M p) (hs : 2 ≤ change 4 * x + 4 ≤ 4 * (15360 * C * s / (σ * 8 ^ d)) + 4 omega +/-- At an active call satisfying the certificate, `s ≥ 2`. -/ +theorem ActiveBounds.two_le {C s d M p : ℕ} (hB : ActiveBounds C s d M p) : 2 ≤ s := by + have h := hB.depth_add_two_le + rcases Nat.lt_or_ge s 2 with hs | hs + · rw [Nat.log_of_lt hs] at h + omega + · exact hs + +/-- **The mode count (D.15) at a certified active call**: for a node of valuation `i < u` and +`h = ⌈3 M / u⌉`, and a packing with `#P 2 ^ a ≤ 3 M` (Lemma D.3 (1)), there are at most `2 ^ e_d` +mode tuples. This is `card_modeBudget_le` with its hypotheses supplied by `ActiveBounds`. -/ +theorem ActiveBounds.card_modeBudget_le {C s d M p : ℕ} (hB : ActiveBounds C s d M p) + (hA : Active C s d M p) {i h : ℕ} (hi : i < taper s d) + (hh : h * taper s d ≤ 3 * M + taper s d) {P : Type*} [Fintype P] [DecidableEq P] + (hP : Fintype.card P * 2 ^ slotBits s d ≤ 3 * M) : + #(TensorNetwork.modeBudget + (fun Z : P × Fin (2 ^ (i + 1)) × Fin (nodePrecision p h (slotBits s d) M i) => + (Z.2.2 : ℕ) + 1) + (nodePrecision p h (slotBits s d) M i)) ≤ 2 ^ branchExponent C s d := + ContractionSchedule.card_modeBudget_le hA hB.two_le hB.one_le_taper + (by have := slotBits_eq s d; omega) (hB.nodePrecision_mul_taper_le i h hi hh) hP + /-- **The excess exponents sum to `O(s / √⌊log₂ s⌋)`**: over at most `⌊log₂ s⌋` levels, `∑_d e_d ≤ (245760 C + 4) ⌊s / ⌊√⌊log₂ s⌋⌋⌋`. The terms decrease geometrically, as in the manuscript's `(√2 / 8) ^ d` (§D.4.7, p. 64). -/