`PreU6` holds (round six, `preU6_holds`)

Proved

J6Seg.PJ.preU6_holds

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

complexity-theoryinteger-multiplicationkappa-improvement

PreU6 holds.

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

theorem J6Seg.PJ.preU6_holds (P : Prm) (hP : P.Ok) (pl : Plan6) (tab : Fin 1 → IStmt HS 1) :
    PreU6 P pl tab

Context. B5: the contract PreU6

preU6_holds: for every plan and every table, PreU6 P pl tab holds. The family U has four procedures, the native pairs eCn / tearP (chunk pass) and eJn / tearP (J pass), relocated by the permutation of nativeLayout; Cp = 2, A = 0. Hence PreNeed6 P pl (preNeed6_holds).

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

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

Formal statement

theorem J6Seg.PJ.preU6_holds (P : Prm) (hP : P.Ok) (pl : Plan6) (tab : Fin 1 → IStmt HS 1) :
    PreU6 P pl tab := 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.preU6_holds`, Solutions/J6SegILPreJK34.lean (lines 41–111) of the round-six development.

View graph