The block body (round six, `blockB`)

Proved

J6Seg.ATab.Rn.blockB

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

complexity-theoryinteger-multiplicationkappa-improvement

The block body.

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

theorem J6Seg.ATab.Rn.blockB {W p s t α pk b q : ℕ} {v : Vr} {c : Cs} (hB : ABnd W p s t α)
    (hq : q < ncA p t α) (hL : LV p s t α pk b v) (h24 : v 24 = q) (hv : BV W v)
    (hcI : c cI = []) :
    Rn J6Seg.ATab.blockB v c (fun v' => (∀ j, j ∉ TB' → v' j = v j) ∧ BV W v')
      (update c sS ((segT (aTab6 p s t α pk b) q).reverse ++ c sS)) (cBlock W p α)

Context. A lines, table set-up, part 5: the block body

blockB = 25 := A0(q); push |tab| :: header; 10 := 2W; loopA; 10 := 2W + 2H; loopR; 10 := 2H; loopC (block index q on 24). Rn.blockB: it pushes segT (aTab6 …) q onto sS (reversed: sS gains (segT … q).reverse).

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_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.ATab
open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH Function

Formal statement

theorem J6Seg.ATab.Rn.blockB {W p s t α pk b q : ℕ} {v : Vr} {c : Cs} (hB : ABnd W p s t α)
    (hq : q < ncA p t α) (hL : LV p s t α pk b v) (h24 : v 24 = q) (hv : BV W v)
    (hcI : c cI = []) :
    Rn J6Seg.ATab.blockB v c (fun v' => (∀ j, j ∉ TB' → v' j = v j) ∧ BV W v')
      (update c sS ((segT (aTab6 p s t α pk b) q).reverse ++ c sS)) (cBlock W p α) := 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 `J6Seg.ATab.Rn.blockB`, Solutions/J6AILTab5.lean (lines 122–220) of the round-six development.

View graph