From 2fca4d8e44d47d3d1fea5c3f7903628f8048da69 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 27 Oct 2026 00:05:37 -0400 Subject: [PATCH] feat(Sparsification): select sharp first-success counting thresholds --- Complexity.lean | 1 + .../Sparsification/CountingParameters.lean | 300 ++++++++++++++++++ ComplexityTests/CountingParameters.lean | 59 ++++ 3 files changed, 360 insertions(+) create mode 100644 Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean create mode 100644 ComplexityTests/CountingParameters.lean diff --git a/Complexity.lean b/Complexity.lean index 548da57346..18b0ddf5ef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2209,6 +2209,7 @@ public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingDeletion public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTree public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingUnits diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean new file mode 100644 index 0000000000..7a3ea6a09d --- /dev/null +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingParameters.lean @@ -0,0 +1,300 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.Nat.Choose.Real +public import Complexity.Foundations.Data.Nat.Log +import Mathlib.Data.Nat.Find + +/-! +# First-success geometric thresholds for counting sparsification + +For fixed width `k ≥ 2` and inverse error budget `B ≥ 1`, Appendix A.3 of [OpenAI2026ETH] +tests dyadic threshold bases `M` in increasing order. The exact test is `Γ ≤ M` and +`B * Γ * ⌈log₂ (4 * C * M)⌉ ≤ M`, where `C = 4 ∑ r < k - 1, (3 * M) ^ r` and +`Γ = 4 ∑ r < k - 1, 3 ^ r`. `countingThresholdBase` implements this first-success search. +The parameters depend only on `k` and `B`, before any input formula or variable budget. + +An explicit successful candidate proves termination and the sharp bound +`M = O_k(B log(2B))`; that candidate does not replace the first-success output. Widths zero +and one have empty coefficient sums and use the separate default `M = 2`. The same total +default is used at `B = 0`, which is outside the positive-error-budget specification. + +This module proves numerical selection and size bounds, not a native bit-cost certificate, +tree-word counting, or the complete counting sparsification theorem. + +## Main definitions + +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingDepthCoeff`: the source coefficient `C`. +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingBChoiceCoeff`: the source coefficient `Γ`. +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase`: the first successful dyadic base. + +## Main results + +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_spec`: the exact integer test. +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingThresholdBase_first`: dyadic minimality. +* `Cslib.Logic.PL.ClauseSet.Sparsification.exists_countingThresholdBase_le_mul_clog`: + the sharp size dependence on the inverse error budget. +* `Cslib.Logic.PL.ClauseSet.Sparsification.isBigO_countingThresholdBase`: + the real logarithmic bound. +* `Cslib.Logic.PL.ClauseSet.Sparsification.exists_clog_countingThresholdBase_le`: + a logarithmic bound on the number of dyadic candidates tested. +* `Cslib.Logic.PL.ClauseSet.Sparsification.sum_choose_le_countingThresholdBase`: + the all-input-size numerical binomial-tail bound for the selected parameter. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.3, pp. 46–47][OpenAI2026ETH] +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.ClauseSet.Sparsification + +open Finset + +/-- The linear path-depth coefficient `C` in Appendix A.3. -/ +def countingDepthCoeff (k M : ℕ) : ℕ := 4 * ∑ r ∈ range (k - 1), (3 * M) ^ r + +/-- The coefficient `Γ` in the weighted B-choice bound of Appendix A.3. -/ +def countingBChoiceCoeff (k : ℕ) : ℕ := 4 * ∑ r ∈ range (k - 1), 3 ^ r + +/-- The depth coefficient is at least four once width two is allowed. -/ +theorem four_le_countingDepthCoeff {k M : ℕ} (hk : 2 ≤ k) : 4 ≤ countingDepthCoeff k M := by + have h := single_le_sum (f := fun r => (3 * M) ^ r) + (fun r _ => Nat.zero_le _) (show 0 ∈ range (k - 1) by simp only [mem_range]; omega) + simp only [pow_zero] at h + exact Nat.mul_le_mul_left 4 h + +/-- The B-choice coefficient is at least four once width two is allowed. -/ +theorem four_le_countingBChoiceCoeff {k : ℕ} (hk : 2 ≤ k) : 4 ≤ countingBChoiceCoeff k := by + simpa only [countingDepthCoeff, countingBChoiceCoeff, mul_one] using + (four_le_countingDepthCoeff (M := 1) hk) + +private theorem depthCoeff_le {k M : ℕ} (hM : 1 ≤ M) : + countingDepthCoeff k M ≤ countingBChoiceCoeff k * M ^ (k - 2) := by + calc countingDepthCoeff k M + ≤ 4 * ∑ r ∈ range (k - 1), 3 ^ r * M ^ (k - 2) := by + apply Nat.mul_le_mul_left 4 + apply sum_le_sum + intro r hr + rw [Nat.mul_pow] + exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) (by + have := mem_range.mp hr + omega)) + _ = countingBChoiceCoeff k * M ^ (k - 2) := by + rw [← sum_mul] + exact (Nat.mul_assoc _ _ _).symm + +private abbrev Accepts (k B m : ℕ) : Prop := + countingBChoiceCoeff k ≤ 2 ^ m ∧ + B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤ + 2 ^ m + +private def offset (k : ℕ) : ℕ := + 2 * (countingBChoiceCoeff k * (Nat.clog 2 (4 * countingBChoiceCoeff k) + 3 * (k - 1) + 1)) + +private def candidateExponent (k B : ℕ) : ℕ := + offset k + Nat.clog 2 B + Nat.clog 2 (Nat.clog 2 B + 1) + +private theorem clog_depthCoeff_le {k : ℕ} (hk : 2 ≤ k) (m : ℕ) : + Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤ + Nat.clog 2 (4 * countingBChoiceCoeff k) + (k - 1) * m := by + apply Nat.clog_le_of_le_pow + calc 4 * countingDepthCoeff k (2 ^ m) * 2 ^ m + ≤ 4 * (countingBChoiceCoeff k * (2 ^ m) ^ (k - 2)) * 2 ^ m := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ (depthCoeff_le Nat.one_le_two_pow)) + _ = (4 * countingBChoiceCoeff k) * (2 ^ m) ^ (k - 1) := by + rw [show k - 1 = (k - 2) + 1 by omega, pow_succ] + ring + _ ≤ 2 ^ Nat.clog 2 (4 * countingBChoiceCoeff k) * (2 ^ m) ^ (k - 1) := + Nat.mul_le_mul_right _ (Nat.le_pow_clog (by decide) _) + _ = 2 ^ (Nat.clog 2 (4 * countingBChoiceCoeff k) + (k - 1) * m) := by + rw [← pow_mul, ← pow_add, Nat.mul_comm m] + +private theorem offset_budget {k : ℕ} (hk : 2 ≤ k) : + countingBChoiceCoeff k * (Nat.clog 2 (4 * countingBChoiceCoeff k) + + (k - 1) * offset k + 2 * (k - 1)) ≤ 2 ^ offset k := by + let g := countingBChoiceCoeff k + let a := Nat.clog 2 (4 * g) + let s := k - 1 + let t := g * (a + 3 * s + 1) + have hg : 1 ≤ g := (by have := four_le_countingBChoiceCoeff hk; omega) + have hga : g * a + 2 * g * s ≤ t := by dsimp only [t]; nlinarith + have hgs : g * s + 1 ≤ t := by dsimp only [t]; nlinarith + have hpoly : g * (a + s * (2 * t) + 2 * s) ≤ 2 * t ^ 2 + 1 := by + nlinarith [Nat.mul_le_mul_right (2 * t) hgs] + exact hpoly.trans (Nat.two_mul_sq_add_one_le_two_pow_two_mul t) + +private theorem gamma_le_two_pow_offset {k : ℕ} (hk : 2 ≤ k) : + countingBChoiceCoeff k ≤ 2 ^ offset k := by + have hg : 1 ≤ countingBChoiceCoeff k := (by have := four_le_countingBChoiceCoeff hk; omega) + have hgo : countingBChoiceCoeff k ≤ offset k := by unfold offset; nlinarith + exact hgo.trans Nat.lt_two_pow_self.le + +private theorem candidate_accepts {k B : ℕ} (hk : 2 ≤ k) : + Accepts k B (candidateExponent k B) := by + let L := Nat.clog 2 B + have hL : Nat.clog 2 (L + 1) ≤ L := Nat.clog_le_of_le_pow Nat.lt_two_pow_self + have hm : candidateExponent k B ≤ offset k + 2 * L := by + dsimp only [candidateExponent, L] at * + omega + have hbudget := offset_budget hk + have hcoeff : countingBChoiceCoeff k * + (Nat.clog 2 (4 * countingBChoiceCoeff k) + (k - 1) * candidateExponent k B) ≤ + 2 ^ offset k * (L + 1) := by + have h1 := Nat.mul_le_mul_left (countingBChoiceCoeff k * (k - 1)) hm + have h2 := Nat.mul_le_mul_right (L + 1) hbudget + nlinarith [Nat.zero_le (countingBChoiceCoeff k * + (Nat.clog 2 (4 * countingBChoiceCoeff k) + (k - 1) * offset k) * L)] + refine ⟨(gamma_le_two_pow_offset hk).trans (Nat.pow_le_pow_right (by decide) (by + unfold candidateExponent; omega)), ?_⟩ + calc B * countingBChoiceCoeff k * + Nat.clog 2 (4 * countingDepthCoeff k (2 ^ candidateExponent k B) * + 2 ^ candidateExponent k B) + ≤ B * (countingBChoiceCoeff k * + (Nat.clog 2 (4 * countingBChoiceCoeff k) + (k - 1) * candidateExponent k B)) := by + have := Nat.mul_le_mul_left (B * countingBChoiceCoeff k) + (clog_depthCoeff_le hk (candidateExponent k B)) + simpa only [Nat.mul_assoc] using this + _ ≤ B * (2 ^ offset k * (L + 1)) := Nat.mul_le_mul_left B hcoeff + _ ≤ 2 ^ L * (2 ^ offset k * 2 ^ Nat.clog 2 (L + 1)) := + Nat.mul_le_mul (Nat.le_pow_clog (by decide) B) + (Nat.mul_le_mul_left _ (Nat.le_pow_clog (by decide) (L + 1))) + _ = 2 ^ candidateExponent k B := by + unfold candidateExponent + rw [pow_add, pow_add] + ring + +private theorem exists_accepts {k : ℕ} (hk : 2 ≤ k) (B : ℕ) : + ∃ m, Accepts k B m := ⟨candidateExponent k B, candidate_accepts hk⟩ + +/-- The first dyadic `M ≥ Γ` passing Appendix A.3's exact test for error budget `σ = 1/B`. +Widths at most one and the out-of-domain input `B = 0` use the total default `2`. The existence +proof only bounds the search: `Nat.find` executes the decidable tests from exponent zero upward. -/ +def countingThresholdBase (k B : ℕ) : ℕ := + if h : 2 ≤ k ∧ 1 ≤ B then + 2 ^ Nat.find (p := fun m => countingBChoiceCoeff k ≤ 2 ^ m ∧ + B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤ + 2 ^ m) (by exact exists_accepts h.1 B) + else 2 + +/-- The selected dyadic base passes both exact integer tests. -/ +theorem countingThresholdBase_spec {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) : + countingBChoiceCoeff k ≤ countingThresholdBase k B ∧ + B * countingBChoiceCoeff k * + Nat.clog 2 (4 * countingDepthCoeff k (countingThresholdBase k B) * + countingThresholdBase k B) ≤ countingThresholdBase k B := by + simp only [countingThresholdBase, hk, hB, and_self, ↓reduceDIte] + exact Nat.find_spec (exists_accepts hk B) + +/-- The returned base is dyadic and every earlier power of two fails the exact test. -/ +theorem countingThresholdBase_first {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) : + ∃ m, countingThresholdBase k B = 2 ^ m ∧ ∀ j < m, + ¬ (countingBChoiceCoeff k ≤ 2 ^ j ∧ + B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ j) * 2 ^ j) ≤ + 2 ^ j) := by + refine ⟨Nat.find (exists_accepts hk B), ?_, fun j hj => Nat.find_min _ hj⟩ + simp only [countingThresholdBase, hk, hB, and_self, ↓reduceDIte] + +/-- A passing candidate with no earlier success computes the selected threshold base. This +permits finite evaluation proofs without unfolding the termination argument of `Nat.find`. -/ +theorem countingThresholdBase_eq_two_pow {k B m : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) + (hpass : countingBChoiceCoeff k ≤ 2 ^ m ∧ + B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ m) * 2 ^ m) ≤ + 2 ^ m) + (hfirst : ∀ j < m, ¬ (countingBChoiceCoeff k ≤ 2 ^ j ∧ + B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k (2 ^ j) * 2 ^ j) ≤ + 2 ^ j)) : countingThresholdBase k B = 2 ^ m := by + simp only [countingThresholdBase, hk, hB, and_self, ↓reduceDIte] + congr 1 + exact (Nat.find_eq_iff _).mpr ⟨hpass, hfirst⟩ + +/-- Widths zero and one use `M = 2` separately from the geometric search. -/ +theorem countingThresholdBase_of_lt_two {k : ℕ} (hk : k < 2) (B : ℕ) : + countingThresholdBase k B = 2 := by simp [countingThresholdBase, show ¬ 2 ≤ k by omega] + +/-- The inverse error budget zero is outside the specification and uses the total default. -/ +theorem countingThresholdBase_zero (k : ℕ) : countingThresholdBase k 0 = 2 := by + simp [countingThresholdBase] + +private theorem thresholdBase_le_candidate {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) : + countingThresholdBase k B ≤ 2 ^ candidateExponent k B := by + simp only [countingThresholdBase, hk, hB, and_self, ↓reduceDIte] + exact Nat.pow_le_pow_right (by decide) (Nat.find_min' _ (candidate_accepts hk)) + +/-- The first-success base has the sharp `B log(2B)` dependence. The constant depends only on +the fixed width; the proof supplies the explicit constant `2 ^ (offset k + 2)`. -/ +theorem exists_countingThresholdBase_le_mul_clog {k : ℕ} (hk : 2 ≤ k) : + ∃ A : ℕ, ∀ B : ℕ, 1 ≤ B → + countingThresholdBase k B ≤ A * B * (Nat.clog 2 B + 1) := by + refine ⟨2 ^ (offset k + 2), fun B hB => (thresholdBase_le_candidate hk hB).trans ?_⟩ + calc 2 ^ candidateExponent k B + = 2 ^ offset k * 2 ^ Nat.clog 2 B * 2 ^ Nat.clog 2 (Nat.clog 2 B + 1) := by + simp only [candidateExponent, pow_add] + _ ≤ 2 ^ offset k * (2 * B) * (2 * (Nat.clog 2 B + 1)) := + Nat.mul_le_mul (Nat.mul_le_mul_left _ (Nat.pow_clog_le_mul (by decide) (by omega))) + (Nat.pow_clog_le_mul (by decide) (by omega)) + _ = 2 ^ (offset k + 2) * B * (Nat.clog 2 B + 1) := by rw [pow_add]; ring + +/-- For fixed width the first-success parameter is `O(B log(2B))` as `B` tends to infinity. -/ +theorem isBigO_countingThresholdBase {k : ℕ} (hk : 2 ≤ k) : + (fun B : ℕ => (countingThresholdBase k B : ℝ)) =O[Filter.atTop] + (fun B : ℕ => (B : ℝ) * Real.log (2 * B)) := by + obtain ⟨A, hA⟩ := exists_countingThresholdBase_le_mul_clog hk + refine Asymptotics.IsBigO.of_bound (2 * A / Real.log 2) ?_ + filter_upwards [Filter.eventually_ge_atTop 1] with B hB + have hBR : (1 : ℝ) ≤ B := by exact_mod_cast hB + have hlog : 0 ≤ Real.logb 2 (B : ℝ) := Real.logb_nonneg (by norm_num) hBR + have hclog : (Nat.clog 2 B : ℝ) ≤ Real.logb 2 (B : ℝ) + 1 := by + rw [← Real.natCeil_logb_natCast] + exact (Nat.ceil_lt_add_one hlog).le + have hlogmul : Real.logb 2 (2 * (B : ℝ)) = 1 + Real.logb 2 (B : ℝ) := by + rw [Real.logb_mul (by norm_num) (by positivity), Real.logb_self_eq_one (by norm_num)] + have hclog' : (Nat.clog 2 B : ℝ) + 1 ≤ 2 * Real.logb 2 (2 * (B : ℝ)) := by + rw [hlogmul] + linarith + have hlog0 : 0 ≤ Real.log (2 * (B : ℝ)) := Real.log_nonneg (by linarith) + have hM0 : (0 : ℝ) ≤ countingThresholdBase k B := Nat.cast_nonneg _ + simp only [Real.norm_eq_abs, abs_of_nonneg hM0, + abs_of_nonneg (mul_nonneg (Nat.cast_nonneg B) hlog0)] + calc (countingThresholdBase k B : ℝ) + ≤ A * B * ((Nat.clog 2 B : ℝ) + 1) := by exact_mod_cast hA B hB + _ ≤ A * B * (2 * Real.logb 2 (2 * (B : ℝ))) := + mul_le_mul_of_nonneg_left hclog' (by positivity) + _ = (2 * A / Real.log 2) * ((B : ℝ) * Real.log (2 * B)) := by rw [Real.logb]; ring + +/-- The selected exponent is at most `D + 2 * ⌈log₂ B⌉`, for a width-dependent constant `D`. +Thus testing exponents from zero through the first success uses at most this bound plus one +tests. This is a count of candidates, not a native bit-operation bound. -/ +theorem exists_clog_countingThresholdBase_le {k : ℕ} (hk : 2 ≤ k) : + ∃ D : ℕ, ∀ B : ℕ, 1 ≤ B → + Nat.clog 2 (countingThresholdBase k B) ≤ D + 2 * Nat.clog 2 B := by + refine ⟨offset k, fun B hB => (Nat.clog_le_of_le_pow (thresholdBase_le_candidate hk hB)).trans ?_⟩ + have h : Nat.clog 2 (Nat.clog 2 B + 1) ≤ Nat.clog 2 B := + Nat.clog_le_of_le_pow Nat.lt_two_pow_self + unfold candidateExponent + omega + +/-- The selected geometric parameter gives the rounded binomial-tail bound for every variable +budget `N`, including zero. This is only a numerical bound; counting tree words is separate. -/ +theorem sum_choose_le_countingThresholdBase {k B : ℕ} (hk : 2 ≤ k) (hB : 1 ≤ B) (N : ℕ) : + ∑ j ∈ range (countingBChoiceCoeff k * N / countingThresholdBase k B + 1), + (countingDepthCoeff k (countingThresholdBase k B) * N).choose j ≤ 2 ^ (N / B + 1) := by + obtain ⟨hM, hbudget⟩ := countingThresholdBase_spec hk hB + exact Cslib.sum_choose_le_two_pow_div_add_one (four_le_countingDepthCoeff hk) + (four_le_countingBChoiceCoeff hk) hM hB hbudget N + +/-- Every selected base, including the total defaults, is at least two. -/ +theorem two_le_countingThresholdBase (k B : ℕ) : 2 ≤ countingThresholdBase k B := by + by_cases h : 2 ≤ k ∧ 1 ≤ B + · exact (by decide : 2 ≤ 4).trans + ((four_le_countingBChoiceCoeff h.1).trans (countingThresholdBase_spec h.1 h.2).1) + · simp [countingThresholdBase, h] + +end Cslib.Logic.PL.ClauseSet.Sparsification diff --git a/ComplexityTests/CountingParameters.lean b/ComplexityTests/CountingParameters.lean new file mode 100644 index 0000000000..79b424aa96 --- /dev/null +++ b/ComplexityTests/CountingParameters.lean @@ -0,0 +1,59 @@ +import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters + +/-! Actual first-success outputs, exact source coefficients, rejected candidates and boundaries. +The evaluation control runs the executable `Nat.find` selector. Equality proofs separately use +its minimum specification and decidable tests of all smaller candidates. -/ + +open Cslib.Logic.PL.ClauseSet.Sparsification Finset + +/-- info: [64, 128, 512, 1024, 2, 2, 2] -/ +#guard_msgs in +#eval [(2, 1), (2, 2), (3, 1), (3, 2), (1, 1), (0, 1), (3, 0)].map + fun (k, B) => countingThresholdBase k B + +example : countingDepthCoeff 3 2 = 28 ∧ countingBChoiceCoeff 3 = 16 := by decide + +private theorem width_two_budget_one : countingThresholdBase 2 1 = 64 := + countingThresholdBase_eq_two_pow (m := 6) (by decide) (by decide) (by decide) (by decide) + +example : countingThresholdBase 2 2 = 128 := + countingThresholdBase_eq_two_pow (m := 7) (by decide) (by decide) (by decide) (by decide) + +example : countingThresholdBase 3 1 = 512 := + countingThresholdBase_eq_two_pow (m := 9) (by decide) (by decide) (by decide) (by decide) + +example : countingThresholdBase 3 2 = 1024 := + countingThresholdBase_eq_two_pow (m := 10) (by decide) (by decide) (by decide) (by decide) + +-- M = 32 is large enough for Γ but fails the budget; the selector must continue to 64. +example : countingBChoiceCoeff 2 ≤ 32 ∧ + ¬ (1 * countingBChoiceCoeff 2 * Nat.clog 2 (4 * countingDepthCoeff 2 32 * 32) ≤ 32) := by + decide + +-- No branching remains at width zero or one. The numerical coefficients vanish, while the +-- separate total choice M = 2 remains compatible with consumers requiring a base at least two. +example : countingDepthCoeff 0 2 = 0 ∧ countingBChoiceCoeff 0 = 0 ∧ + countingThresholdBase 0 3 = 2 ∧ countingDepthCoeff 1 2 = 0 ∧ countingBChoiceCoeff 1 = 0 ∧ + countingThresholdBase 1 3 = 2 := by + norm_num [countingDepthCoeff, countingBChoiceCoeff, + countingThresholdBase_of_lt_two (k := 0) (by decide), + countingThresholdBase_of_lt_two (k := 1) (by decide)] + +example : countingThresholdBase 3 0 = 2 := countingThresholdBase_zero 3 + +-- The selected value feeds the numerical consumer, with positive radius one and tail 65. +example : + (∑ j ∈ range (countingBChoiceCoeff 2 * 16 / countingThresholdBase 2 1 + 1), + (countingDepthCoeff 2 (countingThresholdBase 2 1) * 16).choose j) = 65 ∧ + (∑ j ∈ range (countingBChoiceCoeff 2 * 16 / countingThresholdBase 2 1 + 1), + (countingDepthCoeff 2 (countingThresholdBase 2 1) * 16).choose j) ≤ 2 ^ 17 := by + constructor + · rw [width_two_budget_one] + norm_num [countingBChoiceCoeff, countingDepthCoeff, sum_range_succ] + · exact sum_choose_le_countingThresholdBase (by decide) (by decide) 16 + +-- Variable budget N = 0 is still permitted by the selected-parameter tail theorem. +example : + (∑ j ∈ range (countingBChoiceCoeff 3 * 0 / countingThresholdBase 3 2 + 1), + (countingDepthCoeff 3 (countingThresholdBase 3 2) * 0).choose j) ≤ 2 := by + exact sum_choose_le_countingThresholdBase (by decide) (by decide) 0