The A-line math (round six, `aLine_math`)

Proved

J6Seg.aLine_math

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

complexity-theoryinteger-multiplicationkappa-improvement

The A-line math (the body of ALineHyp6_of_AIL6).

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

theorem J6Seg.aLine_math (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)],
    ∀ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D), FitSpec6 P n src D M →
    ∀ (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (sD6 src D i)) → ℂ),
      RepPad (pP6 P n) (sD6 src D) (tD6 P n D) zs u → ‖u‖ ≤ 1 / 2 →
      zs.length = (List.ofFn (tD6 P n D)).prod ∧ GB (pP6 P n + 2) zs ∧
      RepFull (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs)
        (NLogN.KFY.wOf (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs)) ∧
      GB (pP6 P n + 2) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs) ∧
      ‖NLogN.KFY.wOf (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs) -
        tensCLM (kerA M.A) u‖ ≤ errW6 P n * hp (pP6 P n)

Context. LineNeed6 top level, part 3: the A-line math with the descriptor stack kept

aLine_math: the mathematical part of ALineHyp6_of_AIL6 (J6AMath6, same proof), stated without the IL run, so the top level can keep the descriptor stack of AIL6s (shared with the B sweep): for M with FitSpec6 and a padded representation zs of u (‖u‖ ≤ 1/2), tensorGo (mapsA6 …) zs represents wOf … within errW6 · 2^{-p} of (⊗ A_i) u.

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 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.aLine_math (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)],
    ∀ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D), FitSpec6 P n src D M →
    ∀ (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (sD6 src D i)) → ℂ),
      RepPad (pP6 P n) (sD6 src D) (tD6 P n D) zs u → ‖u‖ ≤ 1 / 2 →
      zs.length = (List.ofFn (tD6 P n D)).prod ∧ GB (pP6 P n + 2) zs ∧
      RepFull (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs)
        (NLogN.KFY.wOf (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs)) ∧
      GB (pP6 P n + 2) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs) ∧
      ‖NLogN.KFY.wOf (pP6 P n) (tD6 P n D) (tensorGo (mapsA6 P n src D) (List.ofFn (tD6 P n D)) zs) -
        tensCLM (kerA M.A) u‖ ≤ errW6 P n * hp (pP6 P n) := 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.aLine_math`, Solutions/J6LineTop3.lean (lines 23–118) of the round-six development.

View graph