The tear-down (round six, `tearP_sp`)

Proved

J6Seg.PJ.tearP_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The tear-down.

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

theorem J6Seg.PJ.tearP_sp (s : IState HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
    (hlt : ∀ i, (oN i).val < 56) (hC : ∀ i, oN i ≠ cLC)
    (F : Cs) (hFo : ∀ i, F (oN i) = []) (hFC : F cLC = [])
    (V : Fin 19 → List ℤ) (T : List ℤ) (x : Fin 9 → ℤ)
    (hVs : ∀ i : Fin 9, V (Fin.castLE (by omega) i) = [x i])
    (hV9 : V 9 = [(T.length : ℤ)]) (hV10 : V 10 = T) (hVr : ∀ i : Fin 19, 11 ≤ i.val → V i = [])
    (B : ℕ) (hxB : ∀ i, zsz (x i) ≤ B) (hlB : zsz (T.length : ℤ) ≤ B) (hTB : Bnd B T) :
    Sp (tearP oN) (encK s (extend oN V F)) (encK s F) (cTear B T.length)

Context. B5 set-up, part 8: the tear-down (plain Sp)

tearP oN: pop oN 0 … oN 8, pop |T| entries of oN 10 (count on oN 9), pop oN 9: from extend oN V F back to F (tearP_sp), for any register file V of the kerRegs shape.

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.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.tearP_sp (s : IState HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
    (hlt : ∀ i, (oN i).val < 56) (hC : ∀ i, oN i ≠ cLC)
    (F : Cs) (hFo : ∀ i, F (oN i) = []) (hFC : F cLC = [])
    (V : Fin 19 → List ℤ) (T : List ℤ) (x : Fin 9 → ℤ)
    (hVs : ∀ i : Fin 9, V (Fin.castLE (by omega) i) = [x i])
    (hV9 : V 9 = [(T.length : ℤ)]) (hV10 : V 10 = T) (hVr : ∀ i : Fin 19, 11 ≤ i.val → V i = [])
    (B : ℕ) (hxB : ∀ i, zsz (x i) ≤ B) (hlB : zsz (T.length : ℤ) ≤ B) (hTB : Bnd B T) :
    Sp (tearP oN) (encK s (extend oN V F)) (encK s F) (cTear B T.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.tearP_sp`, Solutions/J6SegILPreJC8.lean (lines 25–111) of the round-six development.

View graph