The `C`-layer (round six, `clQH`)

Proved

IntMul.Kappa.R6.IL3H.clQH

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

complexity-theoryinteger-multiplicationkappa-improvement

The C-layer.

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

theorem IntMul.Kappa.R6.IL3H.clQH {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp qB Z Zf Zr G Mb Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Z Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hr : 1 ≤ r) (hqq : q0 + qB ≤ D)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hZf : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zf) (hHf : zsz (H : ℤ) ≤ Zf)
    (hV1 : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + D + S + 2 ≤ Mb)
    (pre : q0 + qB < D → MidPre c Isym tbl jL rowC CB K S r H P D ρ q0 Bp qB Z Zf Zr G)
    {σ : Fin HS → Option ℤ} (hC : CoreR σ K S r H P D ρ 0 q0 Bp) (hG : σ vG = some (G : ℤ))
    (h14 : σ 14 = some (qB : ℤ)) (h15 : σ 15 = some ((c.G (D - q0 - qB) : ℕ) : ℤ)) :
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
      (P * 2 ^ (K * D) * S) (tens Cm) (clCH jK jL) (q0 + (qB + c.G (D - q0 - qB)))
      ((c.Wr + 4) * q0 + ((c.Wr + 4) * qB + (c.Wr + 4) * c.G (D - q0 - qB)))
      (cCLH c CB K S r H P D q0 qB Bp Zf Zr Bz)

Context. Round six, item language (I3): the C-layer of the uniform Proposition 14

With the core registers, qB on 14 and Gs D'' on 15 (D'' = D - q₀ - qB), clCH jK jL runs the kernel loop on the top bits [0, q₀), the kernel loop on the bottom bits [D - qB, D), and, if D'' > 0, the middle part (midPart, the level procedure on the padded layout).

clQH: clCH implements tens Cm on the layer, scale q₀ + (qB + Gs D''), width (W'+4)(q₀ + qB + Gs D'').

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.clQH {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp qB Z Zf Zr G Mb Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Z Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hr : 1 ≤ r) (hqq : q0 + qB ≤ D)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hZf : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zf) (hHf : zsz (H : ℤ) ≤ Zf)
    (hV1 : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + D + S + 2 ≤ Mb)
    (pre : q0 + qB < D → MidPre c Isym tbl jL rowC CB K S r H P D ρ q0 Bp qB Z Zf Zr G)
    {σ : Fin HS → Option ℤ} (hC : CoreR σ K S r H P D ρ 0 q0 Bp) (hG : σ vG = some (G : ℤ))
    (h14 : σ 14 = some (qB : ℤ)) (h15 : σ 15 = some ((c.G (D - q0 - qB) : ℕ) : ℤ)) :
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
      (P * 2 ^ (K * D) * S) (tens Cm) (clCH jK jL) (q0 + (qB + c.G (D - q0 - qB)))
      ((c.Wr + 4) * q0 + ((c.Wr + 4) * qB + (c.Wr + 4) * c.G (D - q0 - qB)))
      (cCLH c CB K S r H P D q0 qB Bp Zf Zr Bz) := 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.clQH`, Solutions/R6IL3Top6.lean (lines 62–185) of the round-six development.

View graph