Round-six lemma `entry_runs`
ProvedNLogN.KFM.entry_runsAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.KFMPw):
theorem NLogN.KFM.entry_runs {M : MulSpec} {pM : Fin P} (hM : MulOK I iprog pM M)
(hdom : ∀ x y, M.dom x y) {w φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ w → zsz y ≤ w → M.Φ x y ≤ φ)
(Δ : ℕ) (s : IState HS) (z t : GI) (L0 LW LR : List Item)
(h0 : s.G 0 = .int z.1 :: .int z.2 :: L0) (hW : s.G pW = .int t.1 :: .int t.2 :: LW)
(hR : s.G pR = .int (2 ^ Δ) :: LR) (hz : zsz z.1 ≤ w ∧ zsz z.2 ≤ w)
(ht : zsz t.1 ≤ w ∧ zsz t.2 ≤ w) :
IRuns I iprog (entryB pM) s
(((s.upd 0 L0).upd pW LW).upd pO
(.int (gmulT Δ z t).2 :: .int (gmulT Δ z t).1 :: s.G pO))
(4 * φ + 100000 * (w + Δ + 1))
Context. KFM 9a: the pointwise Gaussian product pass Q_Δ(θ · f) with MulOK products
gmulP pM Δ N: stack 0 holds gflat zs ++ R0 (N Gaussian entries on top), stack pW holds
gflat ts ++ RW (the multipliers, numerators at scale 2^Δ), stack pR holds the ruler 2^Δ.
The pass replaces the entries by gmulT Δ z t = ((z·t).re.tdiv 2^Δ, (z·t).im.tdiv 2^Δ)
(four MulOK products per entry, split by the ruler for tdiv) and consumes the multipliers:
entry_runs: one entry; result pushed (imaginary part last) onpO.gmulP_runs: the pass,0 = gflat (zipWith (gmulT Δ) zs ts) ++ R0,pW = RW, at costN (4 φ + 10^5 (w + Δ + 1)) + 10^4 (N + 1)when all products cost≤ φonw-bit factors.
On numerators (RecRep) this is the twist / chirp step Q_p(θ̃ · f) of §9.4–9.5
(gmulT_eq: gmulT Δ z t = KFH.gtr Δ (gmul z t), and toC_gmul).
gmulP_kTable: the FM instance in the merged table, cost N·4·fmB(2w) + 10^6 (N+1)(w+Δ+1).
Generic per-item pass itemP body N (itemP_runs: x ↦ f x on N integer items of
stack 0) with three instances for §9.3/§9.6: shlP_runs (× 2^γ), roundP_runs
((x + h).tdiv 2^Δ, i.e. rounding when h = 2^{Δ-1}, x + h ≥ 0), smulP_runs
((S x).tdiv 2^Δ, one MulOK product per item).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFM
set_option maxRecDepth 20000
open IntMul NLogN.KFC NLogN.KFB NLogN.KFT NLogN.KIL
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
theorem NLogN.KFM.entry_runs {M : MulSpec} {pM : Fin P} (hM : MulOK I iprog pM M)
(hdom : ∀ x y, M.dom x y) {w φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ w → zsz y ≤ w → M.Φ x y ≤ φ)
(Δ : ℕ) (s : IState HS) (z t : GI) (L0 LW LR : List Item)
(h0 : s.G 0 = .int z.1 :: .int z.2 :: L0) (hW : s.G pW = .int t.1 :: .int t.2 :: LW)
(hR : s.G pR = .int (2 ^ Δ) :: LR) (hz : zsz z.1 ≤ w ∧ zsz z.2 ≤ w)
(ht : zsz t.1 ≤ w ∧ zsz t.2 ≤ w) :
IRuns I iprog (entryB pM) s
(((s.upd 0 L0).upd pW LW).upd pO
(.int (gmulT Δ z t).2 :: .int (gmulT Δ z t).1 :: s.G pO))
(4 * φ + 100000 * (w + Δ + 1)) := by sorry