The uniform phase pass (round six, `cPhU_Y`)
ProvedNLogN.KFW.cPhU_YThe uniform phase pass at a width in the window.
The following holds (Lean statement, in the scope of module Solutions.KFWCost1):
theorem NLogN.KFW.cPhU_Y {Bn t S0 r Z H x sz : ℕ} (hS : 1 ≤ S0) (hBn : 1 ≤ Bn) (hx : x ≤ 2 * H + 16)
(εE : Ex HS) (hsz : εE.size ≤ sz) :
cPhU x (Bn * (S0 * r * 2 ^ t)) t Bn Z (S0 * r) (xPh εE Z Z) ≤
1000000000 * (sz + 2) * nN Bn t S0 * Yu r Z H
Context. KFW: cost units of the uniform level procedure
All costs of the level procedure are evaluated at widths in the window [0, H] (plus small
offsets and the scale ES k ≤ H), so they are bounded by multiples of the cost unit
Yu r Z H = r (2H + 21) + (Z + 2)³
(per record). This file bounds the elementary cost pieces (cAtom, cPhU, push and move
overheads, pow2Cost) by multiples of n · Yu.
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.KFW open IntMul NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN Complex Butterfly
theorem NLogN.KFW.cPhU_Y {Bn t S0 r Z H x sz : ℕ} (hS : 1 ≤ S0) (hBn : 1 ≤ Bn) (hx : x ≤ 2 * H + 16)
(εE : Ex HS) (hsz : εE.size ≤ sz) :
cPhU x (Bn * (S0 * r * 2 ^ t)) t Bn Z (S0 * r) (xPh εE Z Z) ≤
1000000000 * (sz + 2) * nN Bn t S0 * Yu r Z H := by sorry