The seven-pass machine computes the `B` line pass (round six, `r6_machine`)

Proved

J6Seg.r6_machine

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

complexity-theoryinteger-multiplicationkappa-improvement

The seven-pass machine computes the B line pass (round-six regime).

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

theorem J6Seg.r6_machine (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
    SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
    ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
    ∀ ys : List GI, ys.length = (List.ofFn (tD6 P n D)).prod →
      pipeSweep (pipe6 P n src D) (D + 1) ys =
        tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys

Context. B-line machine, sweep 4: the machine computes tensorGo mapsLine6

pipeSweep: the machine applies an axis program Fp k for k = 0, 1, … in place;
pipeSweep_eq: if every Fp k is the in-place axis map of F k, the machine is sweepL;
sweepL_tensorGo': sweepL of line maps of slice form is tensorGo;
r6_maps_eq: in the round-six regime mapsLine6 = mapsBs and λ ∣ t_i, s_i < t_i;
r6_machine: in the round-six regime, the seven-pass machine (pipe6, axes 0..d-1) computes tensorGo (mapsLine6 P n src D) on every array of the right length.

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_Defs62

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open IntMul IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

Formal statement

theorem J6Seg.r6_machine (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
    SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
    ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
    ∀ ys : List GI, ys.length = (List.ofFn (tD6 P n D)).prod →
      pipeSweep (pipe6 P n src D) (D + 1) ys =
        tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys := 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.r6_machine`, Solutions/J6SegSw4.lean (lines 189–271) of the round-six development.

View graph