Round-six lemma `combC_runs`
ProvedNLogN.KFM.combC_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.combC_runs (sub : Bool) (s : IState HS) (u v : ℤ) (Δ : ℕ) (L1 L2 LR : List Item)
(h1 : s.G pP1 = .int u :: L1) (h2 : s.G pP2 = .int v :: L2)
(hR : s.G pR = .int (2 ^ Δ) :: LR) :
IRuns I iprog (combC sub) s
(((s.upd pP1 L1).upd pP2 L2).upd pO
(.int ((u + if sub then -v else v).tdiv (2 ^ Δ)) :: s.G pO))
(1000 * (zsz u + zsz v + Δ + 3))
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.combC_runs (sub : Bool) (s : IState HS) (u v : ℤ) (Δ : ℕ) (L1 L2 LR : List Item)
(h1 : s.G pP1 = .int u :: L1) (h2 : s.G pP2 = .int v :: L2)
(hR : s.G pR = .int (2 ^ Δ) :: LR) :
IRuns I iprog (combC sub) s
(((s.upd pP1 L1).upd pP2 L2).upd pO
(.int ((u + if sub then -v else v).tdiv (2 ^ Δ)) :: s.G pO))
(1000 * (zsz u + zsz v + Δ + 3)) := by sorry