Crude depth guard, guard-width form

Proved

R6.crude_guard_C1

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Under the hypotheses of the crude depth guard, if moreover $C_1 \ge 2 + m \log s$ (a real number), then every $e \le d$ satisfies

A(e) \le 2 s (E + 8)\, d^{C_1}.

This is the form in which the guard constant $C_1$ of the κ framework's CrudeAssembly enters.

In Lean:

theorem R6.crude_guard_C1 (E : ℝ) (s m : ℕ) (d β C1 : ℝ) (A : ℕ → ℝ) (hm : 2 ≤ m) (hs : 2 ≤ s)
    (hβ : 0 ≤ β ∧ β ≤ 1) (hd : 1 ≤ d) (hE : 0 ≤ E) (hC1 : 2 + m * Real.log s ≤ C1)
    (hrec : ∀ e : ℕ, d ^ β ≤ e → ∃ cs : List ℕ, cs.length ≤ s ∧
      (∀ c ∈ cs, m * c ≤ (m - 1) * e) ∧ A e ≤ E + (cs.map A).sum)
    (hleaf : ∀ e : ℕ, (e : ℝ) < d ^ β → A e ≤ 8 * d ^ β) :
    ∀ e : ℕ, (e : ℝ) ≤ d → A e ≤ 2 * s * (E + 8) * d ^ C1

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Mathlib

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open Real

Formal statement

theorem R6.crude_guard_C1 (E : ℝ) (s m : ℕ) (d β C1 : ℝ) (A : ℕ → ℝ) (hm : 2 ≤ m) (hs : 2 ≤ s)
    (hβ : 0 ≤ β ∧ β ≤ 1) (hd : 1 ≤ d) (hE : 0 ≤ E) (hC1 : 2 + m * Real.log s ≤ C1)
    (hrec : ∀ e : ℕ, d ^ β ≤ e → ∃ cs : List ℕ, cs.length ≤ s ∧
      (∀ c ∈ cs, m * c ≤ (m - 1) * e) ∧ A e ≤ E + (cs.map A).sum)
    (hleaf : ∀ e : ℕ, (e : ℝ) < d ^ β → A e ≤ 8 * d ^ β) :
    ∀ e : ℕ, (e : ℝ) ≤ d → A e ≤ 2 * s * (E + 8) * d ^ C1 := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `R6.crude_guard_C1`, Solutions/R6Guard.lean (lines 202–221) of the round-six development.

View graph