Round-six lemma `body_runsP`

An 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.R6ZFull):

theorem NLogN.KFZ.body_runsP (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0) {D p h σ K α B : ℕ} (hB : RB p h (D + 1) σ K B) (hMG : MG p h (D + 1) σ K) (Bd : ℕ)
    (hBd : ∀ x ∈ dsG p h (D + 1) σ K, zsz x ≤ Bd)
    (sv t : Fin (D + 1) → ℕ) [∀ i, NeZero (t i)] (hst : ∀ i, sv i ≤ t i) (htp : ∀ i, 0 < t i)
    (hT : ∀ i, t i ≤ 2 ^ (h + 1)) (htl : t (Fin.last D) = 2 ^ (h + 1))
    (hprod : ∏ i, t i = 2 ^ ((D + 1) * h + σ))
    (hM : 2 ^ ((D + 1) * h + σ - (h + 1)) = ∏ i : Fin D, t i.castSucc)
    (bs ss : List ℕ) (hbl : bs.length = D + 1) (hsl : ss.length = D + 1) (hb1 : ∀ b ∈ bs, b ≤ 1)
    (hstl : ∀ (i : ℕ) (hi : i < D + 1), ss[i]'(by omega) ≤ 2 ^ (h + bs[i]'(by omega)))
    (hσ : bs.sum = σ) (hsB : eS h bs (D + 1) + h + 6 ≤ B) (hdB : D + 1 + 2 ≤ B)
    (hKB : zsz (K : ℤ) ≤ B) (hpB : zsz (p : ℤ) ≤ B) (hαB : zsz (α : ℤ) ≤ B)
    (hdesc : descA 1 (axD h bs ss) ++ [(2 * 2 ^ eS h bs (D + 1) : ℤ)] = descT sv t)
    (f : Fin HS → List ℤ) (hf : EmptyEx f)
    (hc : f cS = (K : ℤ) :: (p : ℤ) :: (α : ℤ) :: (h : ℤ) :: ((D + 1 : ℕ) : ℤ) ::
      (zl bs ++ zl ss))
    (xs : List GI) (l : List ℤ) (h0 : f 0 = gflat xs ++ l) (hxs : xs.length = ∏ i, t i)
    (gx : GB (p + 2) xs) (zh : List GI) (hzh : zh.length = ∏ i, t i) (gh : GB (p + 2) zh)
    (gU : GB (p + 2) (List.zipWith (gmulT p) xs (aLz p h D sv t)))
    (gG : GB (p + 2) (zGz p h D sv t xs)) (gF : GB (p + 2) (zFz p h D sv t))
    (gV : GB (p + 2) (List.zipWith (gmulT p) zh (iLz p h D t))) (c18 : ℕ)
    (hcall : IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (.call j)
      (encK (bgS s (preM (FC f p h D σ K sv t (gflat xs ++ l)) (zFz p h D sv t)
          (zGz p h D sv t xs) l) d18 l)
        (fC d18 (gflat (zFz p h D sv t) ++ gflat (zGz p h D sv t xs) ++ [])
          (dsG p h (D + 1) σ K)))
      (encK (bgS s (preM (FC f p h D σ K sv t (gflat xs ++ l)) (zFz p h D sv t)
          (zGz p h D sv t xs) l) d18 l)
        (Function.update (fC d18 (gflat (zFz p h D sv t) ++ gflat (zGz p h D sv t xs) ++ [])
          (dsG p h (D + 1) σ K)) 0 (gflat zh ++ []))) c18) :
    IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (body j d18) (encK s f)
      (encK s (Function.update f 0 (gflat (yz p h D sv t zh) ++ l)))
      (c18 + NLogN.KFZ.cBody B Bd (p / 6) (dsG p h (D + 1) σ K).length p h D σ sv t)

Context. Round six, chirp: the chirp body for any parameters

body_runsP: the frozen KFZFull.body_runs in IL.kTableP tab ext, with the descriptor values of n replaced by MG / dsG.

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*).