Round-six lemma `repS`

Proved

J6Seg.JK.MSp.repS

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.JK.MSp.repS {M : MulSpec} {C : Fin HS} {n : Ex HS} {b : RM} {s : IState HS}
    {F : ℕ → Fin HS → List ℤ} {N B : ℕ} {c : ℕ → ℕ} (hC5 : C.val < 56) (hC : ∀ k, F k C = [])
    (hw : C ∉ b.writes) (hnc : n.Clean) (hno : n.ok (encK s (F 0)))
    (hnb : n.Bnd (encK s (F 0)) B) (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, MSp M b (encK s (update (F k) C [(N : ℤ) - k]))
      (encK s (update (F (k + 1)) C [(N : ℤ) - k])) (c k)) :
    MSp M (.rep C n b) (encK s (F 0)) (encK s (F N))
      ((n.size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
        ∑ k ∈ range N, (c k + 4 * 10 ^ 7 * (B + 2) ^ 2 + 30) + 32)

Context. B-line IL, the J kernel (B4), part 4: the dot loop as a whole, loops with varying bodies

MSp.repS: the counted loop through managed states with an iteration-dependent body cost (∑ k < N, c k);
dotP_spec: dotP X adds dotF P cs acc to SUM, consumes |cs| table entries onto TT and restores X, at cost (|cs| + 1) · uC;
the a-priori bounds of the fixed-point dot products (fmul_abs_lt, dotF_take_abs_le).

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_R6_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL Function Finset

Formal statement

theorem J6Seg.JK.MSp.repS {M : MulSpec} {C : Fin HS} {n : Ex HS} {b : RM} {s : IState HS}
    {F : ℕ → Fin HS → List ℤ} {N B : ℕ} {c : ℕ → ℕ} (hC5 : C.val < 56) (hC : ∀ k, F k C = [])
    (hw : C ∉ b.writes) (hnc : n.Clean) (hno : n.ok (encK s (F 0)))
    (hnb : n.Bnd (encK s (F 0)) B) (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, MSp M b (encK s (update (F k) C [(N : ℤ) - k]))
      (encK s (update (F (k + 1)) C [(N : ℤ) - k])) (c k)) :
    MSp M (.rep C n b) (encK s (F 0)) (encK s (F N))
      ((n.size + 1) * 10 ^ 7 * (B + 2) ^ 2 +
        ∑ k ∈ range N, (c k + 4 * 10 ^ 7 * (B + 2) ^ 2 + 30) + 32) := 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.JK.MSp.repS`, Solutions/J6SegILJKer4.lean (lines 23–85) of the round-six development.

View graph