The new block header (round six, `hdr2_sp`)

Proved

J6Seg.PreT.hdr2_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The new block header.

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

theorem J6Seg.PreT.hdr2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {K Cs : Fin HS}
    (hK : K ∉ rg) (hK5 : K.val < 56) (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56) (hKs : K ≠ Cs)
    (hcs : c Cs = []) {A n b lam : ℕ} (hA : 2 ≤ A) (hv : VB v A) (h2 : v 2 = n) (h24 : v 24 = lam)
    (h28 : v 28 = b) (hn1 : 1 ≤ n) (hnl : n ≤ lam) (h4l : 4 * lam ≤ 2 ^ A) :
    ∃ v' : Fin HS → ℤ, (∀ j, j ≠ 3 → j ≠ 4 → v' j = v j) ∧ VB v' A ∧
      Sp (hdrP2 K Cs) (encK s (J6Seg.PreT.RF v c))
        (encK s (J6Seg.PreT.RF v' (Function.update c K ((J6Seg.KR.blkHdr2 n b).reverse ++ c K))))
        (cHdr2 A lam)

Context. B-line IL, pre-tables (B5′, tabK2 layout), part 22: the new block header and one block

hdrP2 K Cs pushes blkHdr2 n b = [n, 2n, clog₂(2n), 2nb] (reading order, i.e. K gains its reverse) for n on 2, b on 28. clog₂(2n) is computed by λ rounds (counter Cs) of if p < 2n then (p := 2p; j := j + 1) with j on 3, p on 4. Everything is at width BW A (needs 4λ ≤ 2^A, since p = 2^j < 4n).
blkB2 K Cs is blkB K Cs with hdrP2 in place of hdrP; blk2_sp needs no M.

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_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.hdr2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {K Cs : Fin HS}
    (hK : K ∉ rg) (hK5 : K.val < 56) (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56) (hKs : K ≠ Cs)
    (hcs : c Cs = []) {A n b lam : ℕ} (hA : 2 ≤ A) (hv : VB v A) (h2 : v 2 = n) (h24 : v 24 = lam)
    (h28 : v 28 = b) (hn1 : 1 ≤ n) (hnl : n ≤ lam) (h4l : 4 * lam ≤ 2 ^ A) :
    ∃ v' : Fin HS → ℤ, (∀ j, j ≠ 3 → j ≠ 4 → v' j = v j) ∧ VB v' A ∧
      Sp (hdrP2 K Cs) (encK s (J6Seg.PreT.RF v c))
        (encK s (J6Seg.PreT.RF v' (Function.update c K ((J6Seg.KR.blkHdr2 n b).reverse ++ c K))))
        (cHdr2 A lam) := 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.PreT.hdr2_sp`, Solutions/J6SegILPre22.lean (lines 59–190) of the round-six development.

View graph