feat(circuit/frontier): the call count with a constant explicit in C

Complexity/Computability/Circuit/Frontier/TensorNetwork/ScheduleCount.lean

@@ -19,14 +19,16 @@ Under the parameter schedule of `Cslib.Circuits.Frontier.ContractionSchedule`, a
 `ContractionSchedule.ActiveBounds.card_modeBudget_le`), and there are at most
 `⌊log₂ s⌋` levels. The excess exponents sum to `O(s / √⌊log₂ s⌋)`
 (`ContractionSchedule.sum_branchExponent_le`), so the recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls
-(`ContractionSchedule.exists_recursionBound_le`): the count of Appendix D.4.7 (p. 64), in the
+(`ContractionSchedule.recursionBound_le_two_pow_div_sqrt_log_two`, with the constant
+`245760 C + 37`): the count of Appendix D.4.7 (p. 64), in the
 natural-number scale of the contraction interface. It bounds the nodes of the depth-first
 evaluation (`Nat.recursionBound`), hence the fuel of
 `Cslib.GenericRAM.StackRecursion.Scheme.certificate`.
 
 ## Main results
 
-* `Cslib.Circuits.Frontier.ContractionSchedule.exists_recursionBound_le`: the call count.
+* `Cslib.Circuits.Frontier.ContractionSchedule.recursionBound_le_two_pow_div_sqrt_log_two`: the
+  call count.
 
 ## References
 
@@ -37,16 +39,20 @@ public section
 
 namespace Cslib.Circuits.Frontier.ContractionSchedule
 
-/-- **The recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls.** For every `C` there is `K` such that,
-from `s = 2` on, a recursion of depth at most `D ≤ ⌊log₂ s⌋` whose calls at depth `d` have at
-most `2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children has at most
-`2 ^ (K s / √⌊log₂ s⌋)` nodes below its root. -/
-theorem exists_recursionBound_le (C : ℕ) : ∃ K, ∀ s D, 2 ≤ s → D ≤ Nat.log 2 s →
+/-- **The recursion has `2 ^ O(s / √⌊log₂ s⌋)` calls**, with the constant `245760 C + 37`. From
+`s = 2` on, a recursion of depth at most `D ≤ ⌊log₂ s⌋` whose calls at depth `d` have at most
+`2 ^ (2 ⌊log₂ s⌋ + branchExponent C s d)` children has at most
+`2 ^ ((245760 C + 37) s / √⌊log₂ s⌋)` nodes below its root. The constant is linear in `C`, so one
+clock serves every admissibility constant at once, as a machine that does not know `C` needs. -/
+theorem recursionBound_le_two_pow_div_sqrt_log_two (C : ℕ) {s D : ℕ} (hs : 2 ≤ s)
+    (hD : D ≤ Nat.log 2 s) :
     Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) D 0 ≤
-      2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) := by
-  obtain ⟨K, hK⟩ := Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two 2 (245760 * C + 4)
-  refine ⟨K, fun s D hs hD => (Nat.recursionBound_le _ D 0).trans ?_⟩
-  simpa only [Nat.zero_add] using hK s D (fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d))
-    (branchExponent C s) hs hD (fun _ _ => le_rfl) (sum_branchExponent_le C hs hD)
+      2 ^ ((245760 * C + 37) * s / Nat.sqrt (Nat.log 2 s)) := by
+  have h := Nat.mul_prod_le_two_pow_div_sqrt_log_two 2 (245760 * C + 4) hs hD
+    (b := fun d => 2 ^ (2 * Nat.log 2 s + branchExponent C s d)) (e := branchExponent C s)
+    (fun _ _ => le_rfl) (sum_branchExponent_le C hs hD)
+  rw [show 1 + 16 * 2 + (245760 * C + 4) = 245760 * C + 37 by ring] at h
+  refine (Nat.recursionBound_le _ D 0).trans ?_
+  simpa only [Nat.zero_add] using h
 
 end Cslib.Circuits.Frontier.ContractionSchedule

Complexity/Foundations/Data/Nat/RecursionTree.lean

@@ -25,7 +25,8 @@ most `k + 1` times the product of the branching factors (`Nat.recursionBound_le`
 **Recursion trees of size `2 ^ O(n / √(log n))`.** If a call at depth `j` has at most
 `2 ^ (c ⌊log₂ n⌋ + e j)` children, there are at most `⌊log₂ n⌋` levels, and the excess exponents
 sum to `O(n / √⌊log₂ n⌋)`, then the tree has `2 ^ O(n / √⌊log₂ n⌋)` nodes
-(`Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`), in the natural-number scale of
+(`Nat.mul_prod_le_two_pow_div_sqrt_log_two`, with the explicit constant `1 + 16 c + E`), in the
+natural-number scale of
 `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`. The polynomial factors `2 ^ (c ⌊log₂ n⌋)`
 contribute `2 ^ O(log² n)`, which the scale absorbs. Excess exponents halving with the depth sum to
 at most twice the first one (`Nat.sum_div_two_pow_le`).
@@ -42,8 +43,8 @@ a call at depth `d` has `s ^ O(1) exp(O(s / √λ · (√2 / 8) ^ d))` children
 
 * `Nat.recursionBound_le`: at most `k + 1` times the product of the branching factors.
 * `Nat.sum_div_two_pow_le`: `∑ j < D, x / 2 ^ j ≤ 2 x`.
-* `Nat.exists_recursionBound_le_two_pow_div_sqrt_log_two`: recursion trees of size
-  `2 ^ O(n / √⌊log₂ n⌋)`.
+* `Nat.mul_prod_le_two_pow_div_sqrt_log_two`: recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`,
+  with an explicit constant.
 
 ## References
 
@@ -132,17 +133,16 @@ theorem log_two_sq_le_div_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) :
   have h2 := mul_div_le_mul_div_add 8 n (sqrt L)
   omega
 
-/-- **Recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`.** For constants `c` and `E` there is `K`
-such that, from `n = 2` on: if a call at depth `j < D` has at most `2 ^ (c ⌊log₂ n⌋ + e j)`
-children, `D ≤ ⌊log₂ n⌋`, and `∑ j < D, e j ≤ E (n / √⌊log₂ n⌋)`, then
-`(D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ (K n / √⌊log₂ n⌋)`, which bounds the nodes of the recursion
-tree by `recursionBound_le`. -/
-theorem exists_recursionBound_le_two_pow_div_sqrt_log_two (c E : ℕ) :
-    ∃ K, ∀ (n D : ℕ) (b e : ℕ → ℕ), 2 ≤ n → D ≤ log 2 n →
-      (∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j)) →
-      ∑ j ∈ range D, e j ≤ E * (n / sqrt (log 2 n)) →
-      (D + 1) * ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ (K * n / sqrt (log 2 n)) := by
-  refine ⟨1 + 16 * c + E, fun n D b e hn hD hb he => ?_⟩
+/-- **Recursion trees of size `2 ^ O(n / √⌊log₂ n⌋)`**, with the constant `1 + 16 c + E`. From
+`n = 2` on: if a call at depth `j < D` has at most `2 ^ (c ⌊log₂ n⌋ + e j)` children,
+`D ≤ ⌊log₂ n⌋`, and `∑ j < D, e j ≤ E (n / √⌊log₂ n⌋)`, then
+`(D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ ((1 + 16 c + E) n / √⌊log₂ n⌋)`, which bounds the nodes of the
+recursion tree by `recursionBound_le`. The constant is linear in `E`, so a single clock serves a
+family of excess budgets growing linearly in a parameter. -/
+theorem mul_prod_le_two_pow_div_sqrt_log_two (c E : ℕ) {n D : ℕ} {b e : ℕ → ℕ} (hn : 2 ≤ n)
+    (hD : D ≤ log 2 n) (hb : ∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j))
+    (he : ∑ j ∈ range D, e j ≤ E * (n / sqrt (log 2 n))) :
+    (D + 1) * ∏ j ∈ range D, max 1 (b j) ≤ 2 ^ ((1 + 16 * c + E) * n / sqrt (log 2 n)) := by
   set L := log 2 n
   set S := n / sqrt L
   have hL : L ≤ S := log_two_le_div_sqrt_log_two n

ComplexityTests/ScheduleCount.lean

@@ -15,11 +15,14 @@ namespace ComplexityTests.ScheduleCount
 
 open Cslib.Circuits.Frontier.ContractionSchedule
 
--- At `s = 16` the depth is at most `⌊log₂ 16⌋ = 4`; one constant serves every depth and size.
-example (C : ℕ) : ∃ K, ∀ D ≤ Nat.log 2 16,
+-- At `s = 16` the depth is at most `⌊log₂ 16⌋ = 4`; the constant `245760 C + 37` serves every
+-- depth and size.
+example (C : ℕ) : ∀ D ≤ Nat.log 2 16,
     Nat.recursionBound (fun d => 2 ^ (2 * Nat.log 2 16 + branchExponent C 16 d)) D 0 ≤
-      2 ^ (K * 16 / Nat.sqrt (Nat.log 2 16)) := by
-  obtain ⟨K, hK⟩ := exists_recursionBound_le C
-  exact ⟨K, fun D hD => hK 16 D (by norm_num) hD⟩
+      2 ^ ((245760 * C + 37) * 16 / Nat.sqrt (Nat.log 2 16)) :=
+  fun _ hD => recursionBound_le_two_pow_div_sqrt_log_two C (by norm_num) hD
+
+-- The constant is linear in `C`: at `C = 1` it is `245797`.
+example : 245760 * 1 + 37 = 245797 := by norm_num
 
 end ComplexityTests.ScheduleCount