The layer body (round six, `bodyQH`)

Proved

IntMul.Kappa.R6.IL3H.bodyQH

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

complexity-theoryinteger-multiplicationkappa-improvement

The layer body.

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

theorem IntMul.Kappa.R6.IL3H.bodyQH {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 Zl Z Zr G Mb Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Zl Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hr : 1 ≤ r) (hD : 1 ≤ D) (hq0 : q0 ≤ D)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zl)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z) (hHZ : zsz (H : ℤ) ≤ Z)
    (hV1 : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : MbBody c K P D S G q0 (qBv c.m K D G q0) ≤ Mb)
    (pre : q0 + qBv c.m K D G q0 < D →
      MidPre c Isym tbl jL rowC CB K S r H P D ρ q0 Bp (qBv c.m K D G q0) Zl Z Zr G)
    (hEZ : zsz ((Etot c D q0 (qBv c.m K D G q0) : ℕ) : ℤ) ≤ Z)
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)) (p w : ℕ)
    (hC0 : Clean0 f) (h0 : f 0 = gflat zs ++ l) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (hb : GB w zs)
    (hH : w + (dwCL c D q0 (qBv c.m K D G q0) + 2) ≤ H)
    (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1)
    (hex : ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)) :
    ∀ σ, CoreR σ K S r H P D ρ 0 q0 Bp → σ vG = some (G : ℤ) →
      RunQ Isym tbl σ (bodyCH c jK jL) f (Function.update f 0 (gflat (Classical.choose hex) ++ l))
        (cBodyH c CB K S r H P D q0 (qBv c.m K D G q0) Bp Z Zr Bz w)

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

bodyQH: on every core assignment (CoreR at k = 0, G on vG), bodyCH c jK jL (the frames bF1 … bF4, then bodyCore) leaves gflat zs* ++ l on stack 0, where zs* is the representation of prop14Proc … (tens Cm).

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 AModel 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.bodyQH {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 Zl Z Zr G Mb Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Zl Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hr : 1 ≤ r) (hD : 1 ≤ D) (hq0 : q0 ≤ D)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zl)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z) (hHZ : zsz (H : ℤ) ≤ Z)
    (hV1 : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : MbBody c K P D S G q0 (qBv c.m K D G q0) ≤ Mb)
    (pre : q0 + qBv c.m K D G q0 < D →
      MidPre c Isym tbl jL rowC CB K S r H P D ρ q0 Bp (qBv c.m K D G q0) Zl Z Zr G)
    (hEZ : zsz ((Etot c D q0 (qBv c.m K D G q0) : ℕ) : ℤ) ≤ Z)
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)) (p w : ℕ)
    (hC0 : Clean0 f) (h0 : f 0 = gflat zs ++ l) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (hb : GB w zs)
    (hH : w + (dwCL c D q0 (qBv c.m K D G q0) + 2) ≤ H)
    (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1)
    (hex : ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)) :
    ∀ σ, CoreR σ K S r H P D ρ 0 q0 Bp → σ vG = some (G : ℤ) →
      RunQ Isym tbl σ (bodyCH c jK jL) f (Function.update f 0 (gflat (Classical.choose hex) ++ l))
        (cBodyH c CB K S r H P D q0 (qBv c.m K D G q0) Bp Z Zr Bz w) := 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.bodyQH`, Solutions/R6IL3Top8.lean (lines 42–230) of the round-six development.

View graph