Compact row additions (round six, `rowUCC_of`)

Proved

IntMul.Kappa.R6.IL2C.rowUCC_of

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

complexity-theoryinteger-multiplicationkappa-improvement

Compact row additions with factor Kc (G + 2) + 1.

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

theorem IntMul.Kappa.R6.IL2C.rowUCC_of (hm : 16 ≤ m) (hm' : m ≤ 1000000) (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) {Ksw : ℝ}
    (hKsw : 0 ≤ Ksw) (HSw : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) {Pp : ℕ}
    {tbl : Fin Pp → IStmt HS Pp} {g : Fin 1 → Fin Pp} (hprog : ∀ j, tbl (g j) = (tab j).ren id g)
    (Isym : List Sym) :
    IL3H.RowUCC m τ Isym tbl ((rowCodeC l12).ren id g) (10 ^ 31 + 100 * Ksw + 10 ^ 13)

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.rowUCC_of (hm : 16 ≤ m) (hm' : m ≤ 1000000) (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) {Ksw : ℝ}
    (hKsw : 0 ≤ Ksw) (HSw : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) {Pp : ℕ}
    {tbl : Fin Pp → IStmt HS Pp} {g : Fin 1 → Fin Pp} (hprog : ∀ j, tbl (g j) = (tab j).ren id g)
    (Isym : List Sym) :
    IL3H.RowUCC m τ Isym tbl ((rowCodeC l12).ren id g) (10 ^ 31 + 100 * Ksw + 10 ^ 13) := 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.rowUCC_of`, Solutions/R6IL2CRow.lean (lines 532–662) of the round-six development.

View graph