Round-six lemma `phiFE_runs`
ProvedNLogN.KFUU.R6Crt.phiFE_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.R6CrtPhiF):
theorem NLogN.KFUU.R6Crt.phiFE_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 μ) (xs : List ℤ) (h0 : f 0 = xs ++ l)
(hlen : xs.length = vol (shK d (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 (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 (phiFE pM eSw sdS Dsc) (encK s f)
(encK s (Function.update f 0 (PhiD h d bL sF μ xs ++ l))) (cFwdE τ K w h d bL sF B Z Br Bb)
Context. CRT reversal §9: Φ with revE (a copy of KFUU §9b, KFUUPhiF, with revU → revE)
phiFE: 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. phiFE_runs: on the managed state of a PhiNeed call it computes
KFU.PhiD.
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.phiFE_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 μ) (xs : List ℤ) (h0 : f 0 = xs ++ l)
(hlen : xs.length = vol (shK d (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 (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 (phiFE pM eSw sdS Dsc) (encK s f)
(encK s (Function.update f 0 (PhiD h d bL sF μ xs ++ l))) (cFwdE τ K w h d bL sF B Z Br Bb) := by sorry