`LineBody6` from the remaining pieces (round six, `lineBody6_top`)

Proved

J6Seg.lineBody6_top

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

complexity-theoryinteger-multiplicationkappa-improvement

LineBody6 from the remaining pieces.

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

theorem J6Seg.lineBody6_top (P : Prm) (hP : P.Ok) (tab : Fin 1 → IStmt HS 1) (hA : AIL6s P tab)
    (hX : AxisU6 P tab) (hDisc : PipeDisc6 P) : LineBody6 P tab

Context. LineNeed6 top level, part 4: lineBody6_top and lineNeed6_of

One extension table holds the A-line table of AIL6s (relabelled, g4₁) and the machine's own procedures (ownL): the per-axis family U of AxisU6 and, last, the sweep swp (sgm dS dA) dS dA (idx eX) (J6SegILSweep9) on the descriptor stack dS of AIL6s.

the A clause: the relabelled run of AIL6s and aLine_math;
the B clause: sweep_run with the invariant "length ∏ t and DiscL p" (PipeDisc6), r6_machine (the sweep computes tensorGo (mapsLine6 …)) and r6_passB; the cost is (C_X + 10^12) cU6 (sweep_cost_le).

lineNeed6_of: AIL6s, AxisU6 (under the table facts of LineNeed6) and PipeDisc6 give ∀ P, P.Ok → LineNeed6 P.

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_Defs63

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open Complex
open IntMul IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf NLogN.KFM NLogN.KFY IntMul.OpenAI.RT
open NLogN NLogN.KIL NLogN.KFB AModel
open IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

Formal statement

theorem J6Seg.lineBody6_top (P : Prm) (hP : P.Ok) (tab : Fin 1 → IStmt HS 1) (hA : AIL6s P tab)
    (hX : AxisU6 P tab) (hDisc : PipeDisc6 P) : LineBody6 P 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.lineBody6_top`, Solutions/J6LineTop4.lean (lines 79–170) of the round-six development.

View graph