The core stage (round six, `coreQH`)

Proved

IntMul.Kappa.R6.IL3H.coreQH

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

complexity-theoryinteger-multiplicationkappa-improvement

The core stage.

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

theorem IntMul.Kappa.R6.IL3H.coreQH (c : IntMul.Kappa.R6.IL3H.Cfg) (hc : CfgOK c) (cW : ℕ) (hWc : c.W ≤ 2 ^ cW) {body : IStmt HS Pp}
    {σ : Fin HS → Option ℤ} {P K D S ρ r w G Z Mb Bz : ℕ}
    (hd : DescR σ P K D S ρ r w) (hG : σ vG = some (G : ℤ))
    (h12 : σ 12 = some (dep c.m D : ℤ)) (h13 : σ 13 = some ((c.W ^ dep c.m D : ℕ) : ℤ))
    (hD : 1 ≤ D) (hK : 1 ≤ K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r)
    (hKW : cW * dep c.m D + 2 * (D / c.m * G) ≤ K * D)
    (hGm : G + c.m ≤ P * 2 ^ (K * D) * S * r)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : w + EwH c D + c.Aw * (D + 1) ^ c.p + (D + 1) ^ c.p + 2 * c.m +
      (cW + 4) * (K * D + K) + G + 100 ≤ Mb)
    {f g : Fin HS → List ℤ} (hf : Clean0 f) (hg : Clean0 g) {cc : ℕ}
    (Cont : ∀ σ', CoreR σ' K S r (w + EwH c D) P D ρ 0 (q0v c.m cW K D (dep c.m D) G)
        (BpV c.W c.m K P D (dep c.m D) G (q0v c.m cW K D (dep c.m D) G)) →
      σ' vG = some (G : ℤ) → RunQ Isym tbl σ' body f g cc) :
    RunQ Isym tbl σ (coreCH c cW body) f g (cCoreH cc Z Bz (szC c))

Context. Round six, item language (I3): the core registers of the uniform Proposition 14

After the field-width loop (G on vG = 24) and the depth loop (d = dep m D on 12, W^d on 13), coreCH c cW body pushes

27 0, 32 1, 19 1 (a frozen CoreR at level k = 0), 28 q₀ = min(D, ⌈(cW d + 2 ⌊D/m⌋ G) / K⌉), 5 H = w + EwH D (natural frame coreF1),
29 D - q₀, 20 B' = padB (P 2^{K q₀}) (W^d 2^{2 ⌊D/m⌋ G}) (expression frame core2H),

and runs body. coreQH: body runs on a CoreR assignment that keeps G on vG.

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.IL3H
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW Complex P8Lift Butterfly IntMul.Kappa.R6.Cx
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

Formal statement

theorem IntMul.Kappa.R6.IL3H.coreQH (c : IntMul.Kappa.R6.IL3H.Cfg) (hc : CfgOK c) (cW : ℕ) (hWc : c.W ≤ 2 ^ cW) {body : IStmt HS Pp}
    {σ : Fin HS → Option ℤ} {P K D S ρ r w G Z Mb Bz : ℕ}
    (hd : DescR σ P K D S ρ r w) (hG : σ vG = some (G : ℤ))
    (h12 : σ 12 = some (dep c.m D : ℤ)) (h13 : σ 13 = some ((c.W ^ dep c.m D : ℕ) : ℤ))
    (hD : 1 ≤ D) (hK : 1 ≤ K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r)
    (hKW : cW * dep c.m D + 2 * (D / c.m * G) ≤ K * D)
    (hGm : G + c.m ≤ P * 2 ^ (K * D) * S * r)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : w + EwH c D + c.Aw * (D + 1) ^ c.p + (D + 1) ^ c.p + 2 * c.m +
      (cW + 4) * (K * D + K) + G + 100 ≤ Mb)
    {f g : Fin HS → List ℤ} (hf : Clean0 f) (hg : Clean0 g) {cc : ℕ}
    (Cont : ∀ σ', CoreR σ' K S r (w + EwH c D) P D ρ 0 (q0v c.m cW K D (dep c.m D) G)
        (BpV c.W c.m K P D (dep c.m D) G (q0v c.m cW K D (dep c.m D) G)) →
      σ' vG = some (G : ℤ) → RunQ Isym tbl σ' body f g cc) :
    RunQ Isym tbl σ (coreCH c cW body) f g (cCoreH cc Z Bz (szC c)) := 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.IL3H.coreQH`, Solutions/R6IL3Top3.lean (lines 110–416) of the round-six development.

View graph