The geometry of the `A` axis steps (round six, `axA_geom`)

Proved

J6Seg.axA_geom

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

complexity-theoryinteger-multiplicationkappa-improvement

The geometry of the A axis steps (round-six regime).

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

theorem J6Seg.axA_geom (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
    SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D,
    1 ≤ HA6 P n ∧ 0 < tF6 P n k / (16 * HA6 P n) ∧
    tF6 P n k = tF6 P n k / (16 * HA6 P n) * 8 * (2 * HA6 P n) ∧
    J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ src k ∧ src k ≤ tF6 P n k ∧
    2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) * tF6 P n k ≤ 16 * HA6 P n * src k ∧
    2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ 8 * HA6 P n ∧
    2 ^ (Nat.log 2 (sWidth (pP6 P n) (αN6 P n)) + 3) = 8 * HA6 P n ∧
    0 < preT P n D k ∧ 0 < postT P n D k

Context. A lines, IL side 10: the axis geometry and the kernel row facts

axA_geom: in the round-six regime, for every axis k ≤ D (H = HA6, t = t_k, s = src k, W = WA p α H): 1 ≤ H, 0 < t/16H, t = t/16H · 8 · 2H, W ≤ s ≤ t, 2Wt ≤ 16Hs, 2W ≤ 8H, 2^(⌊log₂ m⌋+3) = 8H, 0 < preT, 0 < postT;
gK_length: the kernel keeps a row of length 8H (when 2W ≤ 8H);
aKerL_AB / gK_GB: the kernel output bound AB (Kc ((w2+bk) Kr (Ka X0 + 1) + 1) + 1), hence GB (pk + 1) under the aK_runs condition he3.

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 IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf

Formal statement

theorem J6Seg.axA_geom (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
    SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D,
    1 ≤ HA6 P n ∧ 0 < tF6 P n k / (16 * HA6 P n) ∧
    tF6 P n k = tF6 P n k / (16 * HA6 P n) * 8 * (2 * HA6 P n) ∧
    J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ src k ∧ src k ≤ tF6 P n k ∧
    2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) * tF6 P n k ≤ 16 * HA6 P n * src k ∧
    2 * J6A.WA (pP6 P n) (αN6 P n) (HA6 P n) ≤ 8 * HA6 P n ∧
    2 ^ (Nat.log 2 (sWidth (pP6 P n) (αN6 P n)) + 3) = 8 * HA6 P n ∧
    0 < preT P n D k ∧ 0 < postT P n D k := 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.axA_geom`, Solutions/J6AIL10.lean (lines 24–89) of the round-six development.

View graph