Round-six lemma `rowCodeC_runs`

Proved

IntMul.Kappa.R6.IL2C.rowCodeC_runs

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.R6IL2CRow):

theorem IntMul.Kappa.R6.IL2C.rowCodeC_runs {Ksw : ℝ} (hKsw : 0 ≤ Ksw) (HSw : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) {I : List Sym}
    {F K e T S0 B r H G : ℕ} {i j : Fin m} (hij : (i : ℕ) ≠ j) (hK : 6 ≤ K)
    (hp : IL3F.PF m F K e T S0 B r) (hG : 1 ≤ G) (hGK : G < K)
    (hdB : 2 ^ (2 * ((F - 1) * G)) ∣ B) (hdS : 2 ^ ((F - 1) * G) ∣ S0)
    {u : IState HS} (hAC : Agree (IL3H.rowσC m F K e T S0 B r H G i j) u)
    (zs : List GI) (R0 : List Item) (hg0 : u.G 0 = ints (gflat zs) ++ R0)
    (hl : zs.length = B * 2 ^ T * S0 * r) (hGB : GB H zs) :
    ∃ c, IRuns I tab (rowCodeC l12) u
        (u.upd 0 (ints (gflat (permRecs (rect (IL3F.N0R m F K e T B i j) (IL3F.N1R m F K e i j)
          (IL3F.N2R m F K e i j) (IL3F.N3R m F K e S0 i j) (F * K))
          (rowAddAddr K (e % K) F (pxR i j) (pyR i j)) r zs)) ++ R0)) c ∧
      (c : ℝ) ≤ cL13 Ksw τ (IL3F.N0R m F K e T B i j) (IL3F.N1R m F K e i j)
          (IL3F.N2R m F K e i j) (IL3F.N3R m F K e S0 i j) K F (e % K) G r H (pxR i j) (pyR i j) +
        3 * (cHd (zsz ((VbR T S0 B r H : ℕ) : ℤ)) : ℝ)

Context. Round six, compact controls (I2C): the compact row code and RowUCP′

hdrG (on the row background rowσC: the field width G in register 46) and hdrC (after the frozen header hdrL and the bit-length loop): the registers of CEnv.
rowCodeC l12 = withPushI hdrG (withPushI hdrL (zB (withPushI hdrC (l13C l12)))); rowCodeC_runs: the row addition permRecs … at cost cL13 + 3 cHd.
rowUCC_of: IL3H.RowUCC m τ Isym tbl ((rowCodeC l12).ren id g) Kc (factor Kc (G+2) + 1, no factor K).
RowUCP' (IL3F.RowUCPF with IL3H.RowUCC in place of RowUCF) and rowUCP'_of.

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_Defs22

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH NLogN.KFX NLogN.KFN P8Lift AModel Butterfly IntMul.Kappa.R6.IL
variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ} {m : ℕ}

Formal statement

theorem IntMul.Kappa.R6.IL2C.rowCodeC_runs {Ksw : ℝ} (hKsw : 0 ≤ Ksw) (HSw : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) {I : List Sym}
    {F K e T S0 B r H G : ℕ} {i j : Fin m} (hij : (i : ℕ) ≠ j) (hK : 6 ≤ K)
    (hp : IL3F.PF m F K e T S0 B r) (hG : 1 ≤ G) (hGK : G < K)
    (hdB : 2 ^ (2 * ((F - 1) * G)) ∣ B) (hdS : 2 ^ ((F - 1) * G) ∣ S0)
    {u : IState HS} (hAC : Agree (IL3H.rowσC m F K e T S0 B r H G i j) u)
    (zs : List GI) (R0 : List Item) (hg0 : u.G 0 = ints (gflat zs) ++ R0)
    (hl : zs.length = B * 2 ^ T * S0 * r) (hGB : GB H zs) :
    ∃ c, IRuns I tab (rowCodeC l12) u
        (u.upd 0 (ints (gflat (permRecs (rect (IL3F.N0R m F K e T B i j) (IL3F.N1R m F K e i j)
          (IL3F.N2R m F K e i j) (IL3F.N3R m F K e S0 i j) (F * K))
          (rowAddAddr K (e % K) F (pxR i j) (pyR i j)) r zs)) ++ R0)) c ∧
      (c : ℝ) ≤ cL13 Ksw τ (IL3F.N0R m F K e T B i j) (IL3F.N1R m F K e i j)
          (IL3F.N2R m F K e i j) (IL3F.N3R m F K e S0 i j) K F (e % K) G r H (pxR i j) (pyR i j) +
        3 * (cHd (zsz ((VbR T S0 B r 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 `IntMul.Kappa.R6.IL2C.rowCodeC_runs`, Solutions/R6IL2CRow.lean (lines 171–520) of the round-six development.

View graph