From bffa3cfe4e5d12e668c7cbd21458063402759c10 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:53:49 -0400 Subject: [PATCH] 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 fdd3b220c..68fc1497c 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 000000000..7d742fb6f --- /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 000000000..294c9e724 --- /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