Round-six lemma `PP_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.R6ZCall):

theorem NLogN.KFZ.PP_runsP (j : Fin (7 + E)) (d18 : Fin HS) (hd0 : d18 ≠ 0) {p h d σ K B : ℕ} (hB : RB p h d σ K B) (hM : MG p h d σ K)
    (Bd : ℕ) (hBd : ∀ x ∈ dsG p h d σ K, zsz x ≤ Bd)
    (w : ℕ) (N : ℕ) (xs bL aL tL iL zh : List GI) (l : List ℤ)
    (hxs : xs.length = N) (hbL : bL.length = N) (haL : aL.length = N) (htL : tL.length = N)
    (hiL : iL.length = N) (hzh : zh.length = N)
    (gx : GB w xs) (gb : GB w bL) (ga : GB w aL) (gt : GB w tL) (gi : GB w iL) (gh : GB w zh)
    (gU : GB w (List.zipWith (gmulT p) xs aL))
    (gG : GB w (List.zipWith (gmulT p) (List.zipWith (gmulT p) xs aL) tL))
    (gF : GB w (List.zipWith (gmulT p) bL tL))
    (gV : GB w (List.zipWith (gmulT p) zh iL))
    (F : Fin HS → List ℤ) (hR : Regs F p h d σ K) (LR LX LX2 L1 L2 : List ℤ)
    (h0 : F 0 = gflat xs ++ l) (hqB : F qB = gflat bL) (hqA : F NLogN.KFZ.qA = gflat aL)
    (hqT : F NLogN.KFZ.qT = gflat tL) (hqI : F qI = gflat iL)
    (hpR : F pR = (2 ^ p : ℤ) :: LR) (hnX : F nX = (N : ℤ) :: LX)
    (hnX2 : F nX2 = ((2 * N : ℕ) : ℤ) :: LX2) (hN1 : F KFM.rN = 1 :: L1)
    (hN2 : F rN2 = ((2 * N : ℕ) : ℤ) :: L2) (hX : F (X18 d18) = []) (c18 : ℕ)
    (hcall : IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (.call j)
      (encK (bgS s (preM F (List.zipWith (gmulT p) bL tL)
          (List.zipWith (gmulT p) (List.zipWith (gmulT p) xs aL) tL) l) d18 l)
        (fC d18 (gflat (List.zipWith (gmulT p) bL tL) ++
          gflat (List.zipWith (gmulT p) (List.zipWith (gmulT p) xs aL) tL) ++ [])
          (dsG p h d σ K)))
      (encK (bgS s (preM F (List.zipWith (gmulT p) bL tL)
          (List.zipWith (gmulT p) (List.zipWith (gmulT p) xs aL) tL) l) d18 l)
        (Function.update (fC d18 (gflat (List.zipWith (gmulT p) bL tL) ++
          gflat (List.zipWith (gmulT p) (List.zipWith (gmulT p) xs aL) tL) ++ [])
          (dsG p h d σ K)) 0 (gflat zh ++ []))) c18) :
    IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (PP j d18) (encK s F)
      (encK s (Function.update (Function.update (Function.update (Function.update
        (Function.update F 0 (gflat (List.zipWith (gmulT p)
          (List.zipWith (gmulT p) zh iL) aL) ++ l)) qB []) NLogN.KFZ.qA []) NLogN.KFZ.qT []) qI []))
      (cCmul w p N + (cCmul w p N + (cRepl 1 (2 * N) w + (cCmul w p N +
        ((c18 + cM B Bd (p / 6) (dsG p h d σ K).length) +
        (cCmul w p N + (cCmul w p N + 4 * cMvX (2 * N) w)))))))

Context. Round six, chirp: the Prop 18 call and the product phase for any parameters

• MG, dsG: the side conditions and the Prop 18 descriptor for free p h d σ K (the frozen KFZCall.M_runs reads them through n).
• M_runsG: the frozen M_runs without n.
• PP_runsP: the frozen PP_runs in IL.kTableP tab ext, without n.

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