The A-lines call

Proved

NLogN.KFM.lineA_phase

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

complexity-theoryinteger-multiplicationkappa-improvement

The A-lines call.

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

theorem NLogN.KFM.lineA_phase [instS : ∀ i, NeZero (sBD n D i)] [instT : ∀ i, NeZero (tBD n D i)]
    {eA eB : Fin (7 + P')} {dS : Fin HS} {C₀ : ℝ} {A : ℕ} (hd0 : dS ≠ 0)
    (hL : lineG Isym ext eA eB dS C₀ A n (D + 1)) (Bd : ℕ) (hBd : ∀ x ∈ descLineN n, zsz x ≤ Bd)
    (t : IState HS) (hR : BaseOK t n) (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (sBD n D i)) → ℂ)
    (R0 : List Item) (h0 : t.G 0 = ints (gflat zs) ++ R0)
    (hu : RepPad (pP n) (sBD n D) (tBD n D) zs u) (hu1 : ‖u‖ ≤ 1 / 2) :
    ∃ (zs' : List GI) (w : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) (c : ℕ),
      IRuns Isym iprog (callW (descLineP (bX dS)) (bX dS) (bY dS) dS (g eA)) t
        (t.upd 0 (ints (gflat zs') ++ R0)) c ∧
      RepFull (pP n) (tBD n D) zs' w ∧ NLogN.KFB.GB (pP n + 2) zs' ∧
      (∀ M : AxisMaps (d := D + 1) (pP n) (αP n) (sBD n D) (tBD n D),
        ‖w - tensCLM (kerA M.A) u‖ ≤ epsA (pP n) (αP n) (D + 1) * hp (pP n)) ∧
      (c : ℝ) ≤ kLine n Bd C₀ A

Context. The lemma belongs to the part KFM Big2: the interface calls of bigE: Every interface call is callW bld X Y dS e (KFMCall) with the descriptor builder bld (KFMSB, KFMSF) on the builder stack X = bX dS and the scratch Y = bY dS (both differ from the interface's descriptor stack dS). A run of the interface in its own table kTable ext is a run in the merged table (IRuns.relabel).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$ : the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.

Preamble

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
open NLogN
open NLogN.KFM
open AModel AModelL12 IntMul KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue
  IntMul.OpenAI.RCost
variable {P P' : ℕ} {Isym : List Sym} {iprog : Fin P → IStmt HS P}
  {ext : Fin P' → IStmt HS (7 + P')} {g : Fin (7 + P') → Fin P}
  (hprog : ∀ j, iprog (g j) = (kTable ext j).ren id g)
  {n D : ℕ} (hn : n0 ≤ n) (hD : dP n = D + 1)
include hprog hn

Formal statement

theorem NLogN.KFM.lineA_phase [instS : ∀ i, NeZero (sBD n D i)] [instT : ∀ i, NeZero (tBD n D i)]
    {eA eB : Fin (7 + P')} {dS : Fin HS} {C₀ : ℝ} {A : ℕ} (hd0 : dS ≠ 0)
    (hL : lineG Isym ext eA eB dS C₀ A n (D + 1)) (Bd : ℕ) (hBd : ∀ x ∈ descLineN n, zsz x ≤ Bd)
    (t : IState HS) (hR : BaseOK t n) (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (sBD n D i)) → ℂ)
    (R0 : List Item) (h0 : t.G 0 = ints (gflat zs) ++ R0)
    (hu : RepPad (pP n) (sBD n D) (tBD n D) zs u) (hu1 : ‖u‖ ≤ 1 / 2) :
    ∃ (zs' : List GI) (w : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) (c : ℕ),
      IRuns Isym iprog (callW (descLineP (bX dS)) (bX dS) (bY dS) dS (g eA)) t
        (t.upd 0 (ints (gflat zs') ++ R0)) c ∧
      RepFull (pP n) (tBD n D) zs' w ∧ NLogN.KFB.GB (pP n + 2) zs' ∧
      (∀ M : AxisMaps (d := D + 1) (pP n) (αP n) (sBD n D) (tBD n D),
        ‖w - tensCLM (kerA M.A) u‖ ≤ epsA (pP n) (αP n) (D + 1) * hp (pP n)) ∧
      (c : ℝ) ≤ kLine n Bd C₀ A := by sorry

Source

OpenAI, Integer multiplication below n log n (preprint, 23 Sep 2026), https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026. Lemma `NLogN.KFM.lineA_phase` of the Lean development Solutions/KFMBig2.lean (lines 106–133), integer-multiplication-kappa campaign.

View graph