One level body computes `levelH` (round six, `levBody_run`)

Proved

IntMul.Kappa.R6.IL.levBody_run

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

complexity-theoryinteger-multiplicationkappa-improvement

One level body computes levelH.

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

theorem IntMul.Kappa.R6.IL.levBody_run (C : Bit.QHNet (ZMod 2) W T m) {N : ℕ} [NeZero N] (hN : 1 < N)
    (P L' f : ℕ) (A B Cs : Shape) (hpos : ∀ a ∈ P :: L' :: hdShape A B Cs m N, 1 ≤ a) (Bb : ℕ)
    (hTOK : ∀ e ∈ C.edges, ∀ T' ∈ tplE e.E₁ ++ tplE e.E₂, TOK T' N Bb)
    (hcop : ∀ e ∈ C.edges, ∀ i j, Nat.Coprime (e.E₁ i j).den N ∧ Nat.Coprime (e.E₂ i j).den N)
    (hVT : zsz (((T + W) * vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb)
    (G0 : Fin HS → List Item) (hG : LevH G0 m W T N P L' f A B Cs)
    (child : ℕ × ℕ × ℕ → List (ZMod 2) → List (ZMod 2)) (cC : ℕ × ℕ × ℕ → ℕ)
    (hcall : ∀ e ∈ C.edges, ∀ ρ ∈ e.runs, ∀ (t : IState HS) (R : List Item) (ys : List (ZMod 2)),
      Inv G0 t → ys.length = vol (P :: L' :: hdShape A B Cs m N) →
      IRuns I tab (callR (0 : Fin 1) m ρ) (t.upd 0 (ints (enc2 ys) ++ R))
        (t.upd 0 (ints (enc2 (child ρ ys)) ++ R)) (cC ρ) ∧
      (child ρ ys).length = vol (P :: L' :: hdShape A B Cs m N))
    (t : IState HS) (ht : Inv G0 t) (R : List Item) (xs : List (ZMod 2))
    (hxs : xs.length = vol (P :: W * L' :: hdShape A B Cs m N)) :
    IRuns I tab (levBody C) (t.upd 0 (ints (enc2 xs) ++ R))
      (t.upd 0 (ints (enc2 (Bit.levelH C N P L' A B Cs child xs)) ++ R))
      (cLevBody C P L' (vol (hdShape A B Cs m N)) (vol (P :: L' :: hdShape A B Cs m N)) Bb cC)

Context. Round six, item language: one level of the general procedure

levBody C: row split (KFC bwdF), T · v zeros pushed in front (the temporaries), the network netH (edgeR 0 m) C.prog on the T + W streams, the routing rebuild (role w takes the stream of wire inl (ρ w)), the temporaries dropped, row merge (KFC fwdF).

levBody_run: under the level registers LevH G0 … and a run hypothesis for the child calls, the body computes Bit.levelH C N P L' A B Cs child (the denotation used by Bit.progH).

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_Defs13

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset
variable {W T m : ℕ} [NeZero W]
variable {I : List Sym} {tab : Fin 1 → IStmt HS 1}

Formal statement

theorem IntMul.Kappa.R6.IL.levBody_run (C : Bit.QHNet (ZMod 2) W T m) {N : ℕ} [NeZero N] (hN : 1 < N)
    (P L' f : ℕ) (A B Cs : Shape) (hpos : ∀ a ∈ P :: L' :: hdShape A B Cs m N, 1 ≤ a) (Bb : ℕ)
    (hTOK : ∀ e ∈ C.edges, ∀ T' ∈ tplE e.E₁ ++ tplE e.E₂, TOK T' N Bb)
    (hcop : ∀ e ∈ C.edges, ∀ i j, Nat.Coprime (e.E₁ i j).den N ∧ Nat.Coprime (e.E₂ i j).den N)
    (hVT : zsz (((T + W) * vol (P :: L' :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb)
    (G0 : Fin HS → List Item) (hG : LevH G0 m W T N P L' f A B Cs)
    (child : ℕ × ℕ × ℕ → List (ZMod 2) → List (ZMod 2)) (cC : ℕ × ℕ × ℕ → ℕ)
    (hcall : ∀ e ∈ C.edges, ∀ ρ ∈ e.runs, ∀ (t : IState HS) (R : List Item) (ys : List (ZMod 2)),
      Inv G0 t → ys.length = vol (P :: L' :: hdShape A B Cs m N) →
      IRuns I tab (callR (0 : Fin 1) m ρ) (t.upd 0 (ints (enc2 ys) ++ R))
        (t.upd 0 (ints (enc2 (child ρ ys)) ++ R)) (cC ρ) ∧
      (child ρ ys).length = vol (P :: L' :: hdShape A B Cs m N))
    (t : IState HS) (ht : Inv G0 t) (R : List Item) (xs : List (ZMod 2))
    (hxs : xs.length = vol (P :: W * L' :: hdShape A B Cs m N)) :
    IRuns I tab (levBody C) (t.upd 0 (ints (enc2 xs) ++ R))
      (t.upd 0 (ints (enc2 (Bit.levelH C N P L' A B Cs child xs)) ++ R))
      (cLevBody C P L' (vol (hdShape A B Cs m N)) (vol (P :: L' :: hdShape A B Cs m N)) Bb cC) := 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.IL.levBody_run`, Solutions/R6ILLevel.lean (lines 178–335) of the round-six development.

View graph