phiFU_runs (KFUU §9b: the uniform `Φ`)

Proved

NLogN.KFUU.phiFU_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

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

theorem NLogN.KFUU.phiFU_runs {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {eSw : Fin P} {sdS : Fin HS} {K : ℝ}
    (hK : SwOKU I iprog eSw sdS K) (hdS : sdS ≠ 0) {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19)
    (hDd : Dsc ≠ sdS) (w h d : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ) (hh : 1 ≤ h)
    (hs : ∀ j < d, 1 ≤ sF j) (hst : ∀ j < d, sF j ≤ 2 ^ (h + if bL j then 1 else 0))
    (hμ : ∀ j < d, μ j < sF j)
    (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ) (hf : ∀ j, j ≠ 0 → j ≠ dP → f j = [])
    (hfd : f dP = KFM.descPhi w h d bL sF μ) (xs : List ℤ) (h0 : f 0 = xs ++ l)
    (hlen : xs.length = vol (shK d (NLogN.KFU.sP d sF))) (hb : Bnd w xs)
    (B Z Br Bb : ℕ) (hwB : zsz (w : ℤ) ≤ B) (hhB : h + 1 ≤ B) (h2B : zsz ((2 ^ h * 2 : ℕ) : ℤ) ≤ B)
    (h3B : zsz ((3 + 3 * d : ℕ) : ℤ) ≤ B) (hVB : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ B)
    (hZ3 : 3 ≤ Z) (hZT : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.tP d h bL)) : ℕ) : ℤ) ≤ Z) (hwZ : zsz (w : ℤ) ≤ Z)
    (hUZ : zsz ((2 ^ h : ℕ) : ℤ) ≤ Z)
    (hVr : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ Br) (hdr : zsz (d : ℤ) ≤ Br)
    (hVb : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ Bb) :
    IRuns I iprog (phiFU pM eSw sdS Dsc) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update f 0 (PhiD h d bL sF μ xs ++ l))) (NLogN.KFUU.cFwd K w h d bL sF B Z Br Bb)

Context. The lemma belongs to the part KFUU §9b: the uniform Φ: phiFU: read the descriptor (readD), build the shape lists (mkL), pad S_k → T_k, reverse (revU, the SwapNeed entry), unpad T_r → S_r, the d forward shifts (rotsFU), pad S_r → T_r, clear. phiFU_runs: on the managed state of a PhiNeed call it computes KFU.PhiD.

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
set_option linter.unnecessarySeqFocus false
open NLogN
open NLogN.KFUU
open IntMul KIL KFB KFC KFT KFU AModel AModelL12
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
set_option maxHeartbeats 64000000

Formal statement

theorem NLogN.KFUU.phiFU_runs {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {eSw : Fin P} {sdS : Fin HS} {K : ℝ}
    (hK : SwOKU I iprog eSw sdS K) (hdS : sdS ≠ 0) {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19)
    (hDd : Dsc ≠ sdS) (w h d : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ) (hh : 1 ≤ h)
    (hs : ∀ j < d, 1 ≤ sF j) (hst : ∀ j < d, sF j ≤ 2 ^ (h + if bL j then 1 else 0))
    (hμ : ∀ j < d, μ j < sF j)
    (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ) (hf : ∀ j, j ≠ 0 → j ≠ dP → f j = [])
    (hfd : f dP = KFM.descPhi w h d bL sF μ) (xs : List ℤ) (h0 : f 0 = xs ++ l)
    (hlen : xs.length = vol (shK d (NLogN.KFU.sP d sF))) (hb : Bnd w xs)
    (B Z Br Bb : ℕ) (hwB : zsz (w : ℤ) ≤ B) (hhB : h + 1 ≤ B) (h2B : zsz ((2 ^ h * 2 : ℕ) : ℤ) ≤ B)
    (h3B : zsz ((3 + 3 * d : ℕ) : ℤ) ≤ B) (hVB : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ B)
    (hZ3 : 3 ≤ Z) (hZT : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.tP d h bL)) : ℕ) : ℤ) ≤ Z) (hwZ : zsz (w : ℤ) ≤ Z)
    (hUZ : zsz ((2 ^ h : ℕ) : ℤ) ≤ Z)
    (hVr : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ Br) (hdr : zsz (d : ℤ) ≤ Br)
    (hVb : zsz ((vol (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) : ℕ) : ℤ) ≤ Bb) :
    IRuns I iprog (phiFU pM eSw sdS Dsc) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update f 0 (PhiD h d bL sF μ xs ++ l))) (NLogN.KFUU.cFwd K w h d bL sF B Z Br Bb) := 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.KFUU.phiFU_runs` of the Lean development Solutions/KFUUPhiF.lean (lines 53–297), integer-multiplication-kappa campaign.

View graph