Round-six lemma `eKz_ge`

Proved

J6Seg.eKz_ge

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

complexity-theoryinteger-multiplicationkappa-improvement

eKz ≥ s² |h| (|h| - 1).

The following holds (Lean statement, in the scope of module Solutions.J6SegGeom):

theorem J6Seg.eKz_ge (hs : 0 < s) (hst : s ≤ t) (l h : ℤ) :
    (s : ℤ) ^ 2 * (|h| * (|h| - 1)) ≤ eKz s t l h

Context. Segmented inverse (S2): exact structure of the resampling system (report L1, L2, L4, L8 tail)

Entries of N = I + E are eEx s t α l h = e^{-πα² X/s²}, X = eKz s t l h.

eKz_closed (L1): X = sn(sn + 2b_{l+h}) with n = q_{l+h} - q_l, and |n| ≥ |h|, so eEx_le_cf: e_{l,h} ≤ e^{-πα²|h|(|h|-1)} (cross-wrap / cut entries).
eEx_recentre (L2/L4): inside a wrap-free run starting at c, e_{c+u, v-u} = D_u T^{(b_c)}_{uv} D_v⁻¹ with b_c = bOf c / s, i.e. MF of J6SegToep.
tail_sum (truncation): Σ_{|h| > w} e_{l,h} ≤ 4 e^{-πα² w(w+1)} for α ≥ 2.
bOf_periodic, eEx_periodic.

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 Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open Finset Real
open IntMul.HvdH
variable (s t α : ℕ)

Formal statement

theorem J6Seg.eKz_ge (hs : 0 < s) (hst : s ≤ t) (l h : ℤ) :
    (s : ℤ) ^ 2 * (|h| * (|h| - 1)) ≤ eKz s t l h := 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 `J6Seg.eKz_ge`, Solutions/J6SegGeom.lean (lines 50–98) of the round-six development.

View graph