`AxisU6` from the B-line components (round six, `axisU6_of`)

Proved

J6Seg.Ax.axisU6_of

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

complexity-theoryinteger-multiplicationkappa-improvement

AxisU6 from the B-line components.

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

theorem J6Seg.Ax.axisU6_of (P : Prm) (hP : P.Ok) (ap : AxPlan6) (hVC : Val.ValCond6 ap) (hCP : AxCh.ChunkPlan6 ap)
    (hPre : PreNeed6 P ap.pl) (hBud : AxBudget6 P ap) (hSlab : SlabNeed6 P)
    (tab : Fin 1 → IStmt HS 1) (hSw : IL.SwapNeedτ tab P.τ) (hRow : IL2.RowUCP 576 P.τ tab)
    (hFU : FineU6 tab) : AxisU6 P tab

Context. B-line axis program (AxisU6), part 11: axisU6_of

AxisU6 P tab for every table with the facts of LineNeed6 (SwapNeedτ, RowUCP, FineU6), from

PreNeed6 P ap.pl (B5: the kernel-pass set-ups),
SlabNeed6 P (B1: the slab set-ups — source-table producers and ctlB),
AxBudget6 P ap (S2: plan constants and the closed-form cost),
the plan conditions ValCond6 ap (value bounds, valNeed6_all') and ChunkPlan6 ap (chunk output, chunkOut6_all); the chunk table bound is chunkTabBnd6_all.

The family: FineU6's, PreU6's and SlabNeed6's procedures, then the chunk kernel chunkI pMul, the J kernel jKprog, and the axis body axBody (descriptor stack 8, kernel registers ρK dF).

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_Defs67

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Ax
set_option maxHeartbeats 4000000
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab (passP drP rdP itO bkP)

Formal statement

theorem J6Seg.Ax.axisU6_of (P : Prm) (hP : P.Ok) (ap : AxPlan6) (hVC : Val.ValCond6 ap) (hCP : AxCh.ChunkPlan6 ap)
    (hPre : PreNeed6 P ap.pl) (hBud : AxBudget6 P ap) (hSlab : SlabNeed6 P)
    (tab : Fin 1 → IStmt HS 1) (hSw : IL.SwapNeedτ tab P.τ) (hRow : IL2.RowUCP 576 P.τ tab)
    (hFU : FineU6 tab) : AxisU6 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.Ax.axisU6_of`, Solutions/J6SegAxis11.lean (lines 84–175) of the round-six development.

View graph