The head (round six, `jHead`)

Proved

J6Seg.PJ.Rn.jHead

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

complexity-theoryinteger-multiplicationkappa-improvement

The head.

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

theorem J6Seg.PJ.Rn.jHead {kA kC wA wC k pre post s t p α d W N : ℕ} {Z : Fin HS}
    (hZ : Z ∉ rg) (hZ5 : Z.val < 56) (hZT : Z ≠ sTmp) (hZC : Z ≠ cRdC)
    {c : Cs} (hcZ : c Z = dsc k pre post s t p α d) (hZv : Z.val = 49 ∨ Z.val = 55)
    (hc : ∀ j, j ≠ Z → c j = [])
    (hW : parBig kA kC wA wC k pre post s t p α d < 2 ^ W)
    (hNW : N < 2 ^ W) (hW2 : 2 ≤ W) (hN1 : 1 ≤ N)
    (hs : 0 < s) (hws : wF d ≤ s) (hQW : segPF p d s ≤ W)
    (hsN : s ≤ N) (hlN : lamP d ≤ N) (hNMN : lamP d * (2 * wF d + 1) ≤ N)
    (hmm : (Jlist (mkBlocks s t (lamP d) (wF d))).length *
      (Jlist (mkBlocks s t (lamP d) (wF d))).length ≤ N)
    (hmc : (Jlist (mkBlocks s t (lamP d) (wF d))).length * (2 * wF d + 2) ≤ N)
    (bss : s * s ≤ 2 ^ W)
    (hJB : JB (segPF p d s) (p / 7) W s t α (lamP d) (wF d)) :
    Rn (J6Seg.PJ.jHead kA kC wA wC Z) (fun _ => 0) c
      (fun v => BV W v ∧ v 9 = ((2 ^ segPF p d s : ℕ) : ℤ) ∧
        v 10 = ((2 ^ (segPF p d s + 1) : ℕ) : ℤ) ∧ v 22 = s ∧ v 24 = lamP d ∧ v 26 = wF d ∧
        v 28 = (Jlist (mkBlocks s t (lamP d) (wF d))).length)
      (headSt (segPF p d s) (p / 7) s t (lamP d) (wF d) α pre post
        ((wA * segPF p d s + wC : ℕ) : ℤ) ((kA * segPF p d s + kC : ℕ) : ℤ)
        ((2 ^ (kA * segPF p d s + kC) : ℕ) : ℤ) c)
      (cJHead kA kC wA wC W N d s p (Jlist (mkBlocks s t (lamP d) (wF d))).length)

Context. B5 J side, part K23: the head parP; jS1; jS2; jK

From the descriptor on Z (49 or 55, everything else empty): parameters, stash, line, tables, capacitance matrix, coupling rows; then the block and table stacks are cleared (Rn.jHead).

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_Defs71

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

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

Formal statement

theorem J6Seg.PJ.Rn.jHead {kA kC wA wC k pre post s t p α d W N : ℕ} {Z : Fin HS}
    (hZ : Z ∉ rg) (hZ5 : Z.val < 56) (hZT : Z ≠ sTmp) (hZC : Z ≠ cRdC)
    {c : Cs} (hcZ : c Z = dsc k pre post s t p α d) (hZv : Z.val = 49 ∨ Z.val = 55)
    (hc : ∀ j, j ≠ Z → c j = [])
    (hW : parBig kA kC wA wC k pre post s t p α d < 2 ^ W)
    (hNW : N < 2 ^ W) (hW2 : 2 ≤ W) (hN1 : 1 ≤ N)
    (hs : 0 < s) (hws : wF d ≤ s) (hQW : segPF p d s ≤ W)
    (hsN : s ≤ N) (hlN : lamP d ≤ N) (hNMN : lamP d * (2 * wF d + 1) ≤ N)
    (hmm : (Jlist (mkBlocks s t (lamP d) (wF d))).length *
      (Jlist (mkBlocks s t (lamP d) (wF d))).length ≤ N)
    (hmc : (Jlist (mkBlocks s t (lamP d) (wF d))).length * (2 * wF d + 2) ≤ N)
    (bss : s * s ≤ 2 ^ W)
    (hJB : JB (segPF p d s) (p / 7) W s t α (lamP d) (wF d)) :
    Rn (J6Seg.PJ.jHead kA kC wA wC Z) (fun _ => 0) c
      (fun v => BV W v ∧ v 9 = ((2 ^ segPF p d s : ℕ) : ℤ) ∧
        v 10 = ((2 ^ (segPF p d s + 1) : ℕ) : ℤ) ∧ v 22 = s ∧ v 24 = lamP d ∧ v 26 = wF d ∧
        v 28 = (Jlist (mkBlocks s t (lamP d) (wF d))).length)
      (headSt (segPF p d s) (p / 7) s t (lamP d) (wF d) α pre post
        ((wA * segPF p d s + wC : ℕ) : ℤ) ((kA * segPF p d s + kC : ℕ) : ℤ)
        ((2 ^ (kA * segPF p d s + kC) : ℕ) : ℤ) c)
      (cJHead kA kC wA wC W N d s p (Jlist (mkBlocks s t (lamP d) (wF d))).length) := 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.PJ.Rn.jHead`, Solutions/J6SegILPreJK23.lean (lines 48–183) of the round-six development.

View graph