Round-six lemma `phiBE_runs`
ProvedNLogN.KFUU.R6Crt.phiBE_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.R6CrtPhiB):
theorem NLogN.KFUU.R6Crt.phiBE_runs {pM : Fin P} (hM : MulOK I iprog pM MS) {eSw : Fin P} {sdS : Fin HS} {K : ℝ}
(hK : SwOKτ τ 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) (hd2 : 2 ≤ d)
(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 μ) (ys : List ℤ) (h0 : f 0 = ys ++ l)
(hlen : ys.length = vol (shR d (tP d h bL))) (hb : Bnd w ys)
(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 (shR d (sP d sF)) : ℕ) : ℤ) ≤ B)
(hZ3 : 3 ≤ Z) (hZT : zsz ((vol (shR d (tP d h bL)) : ℕ) : ℤ) ≤ Z) (hwZ : zsz (w : ℤ) ≤ Z)
(hUZ : zsz ((2 ^ h : ℕ) : ℤ) ≤ Z)
(hVr : zsz ((vol (shR d (sP d sF)) : ℕ) : ℤ) ≤ Br) (hdr : zsz (d : ℤ) ≤ Br)
(hVb : zsz ((vol (shR d (sP d sF)) : ℕ) : ℤ) ≤ Bb) :
IRuns I iprog (phiBE pM eSw sdS Dsc) (encK s f)
(encK s (Function.update f 0 (PhiInvD h d bL sF μ ys ++ l))) (cBwdE τ K w h d bL sF B Z Br Bb)
Context. CRT reversal §10: Φ⁻¹ with revE (a copy of KFUU §9c, KFUUPhiB, with revU → revE)
phiBE: read the descriptor (readD onto xS, xM), build the lists (mkL, the sizes and
multipliers in forward order on oSL, oML), unpad T_r → S_r, the d backward shifts
(rotsBU), pad S_r → T_r, reverse back (revU), unpad T_k → S_k, clear.
phiBE_runs: it computes KFU.PhiInvD.
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_R6_Defs14
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFUU NLogN.KFUU.R6Crt
open IntMul NLogN.KIL NLogN.KFB NLogN.KFC NLogN.KFT NLogN.KFU AModel AModelL12 NLogN.KFUU
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P} {τ : ℝ}
theorem NLogN.KFUU.R6Crt.phiBE_runs {pM : Fin P} (hM : MulOK I iprog pM MS) {eSw : Fin P} {sdS : Fin HS} {K : ℝ}
(hK : SwOKτ τ 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) (hd2 : 2 ≤ d)
(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 μ) (ys : List ℤ) (h0 : f 0 = ys ++ l)
(hlen : ys.length = vol (shR d (tP d h bL))) (hb : Bnd w ys)
(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 (shR d (sP d sF)) : ℕ) : ℤ) ≤ B)
(hZ3 : 3 ≤ Z) (hZT : zsz ((vol (shR d (tP d h bL)) : ℕ) : ℤ) ≤ Z) (hwZ : zsz (w : ℤ) ≤ Z)
(hUZ : zsz ((2 ^ h : ℕ) : ℤ) ≤ Z)
(hVr : zsz ((vol (shR d (sP d sF)) : ℕ) : ℤ) ≤ Br) (hdr : zsz (d : ℤ) ≤ Br)
(hVb : zsz ((vol (shR d (sP d sF)) : ℕ) : ℤ) ≤ Bb) :
IRuns I iprog (phiBE pM eSw sdS Dsc) (encK s f)
(encK s (Function.update f 0 (PhiInvD h d bL sF μ ys ++ l))) (cBwdE τ K w h d bL sF B Z Br Bb) := by sorry