Round-six lemma `sp_par`

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.R6SPar):

theorem IntMul.Kappa.R6.sp_par (P : Prm) (hP : P.Ok) (n : ℕ) (G : Good P n) (a c : ℕ) (hc : 0 < c)
    (hε : P.ε = (a : ℝ) / c) (s : IState HS) (f : Fin HS → List ℤ) (Aa Bb D : ℕ)
    (l23 l24 : List ℤ) (h23 : f 23 = (n : ℤ) :: l23) (h24 : f 24 = (bP6 n : ℤ) :: l24)
    (h47 : f 47 = []) (hAa : 64 ≤ Aa) (hpA : 2 ^ pP6 P n ≤ Aa) (hbA : 2 ^ bP6 n ≤ Aa)
    (hnA : 4 * n ≤ Aa) (hD6 : 6 ≤ D) (hDa : a + c + 4 ≤ D) (hDx : P.x + 2 ≤ D)
    (hB : Aa ^ D < 2 ^ Bb) :
    Sp (parP a c P.x) (encK s f)
      (encK s (update (update (update (update (update (update (update (update (update
        (update f 25 ((dP6 P n : ℤ) :: f 25)) 29 ((b'P6 P n : ℤ) :: f 29))
        30 ((pP6 P n : ℤ) :: f 30)) 31 ((LP6 P n : ℤ) :: f 31)) 32 ((ℓP6 P n : ℤ) :: f 32))
        33 ((hN6 P n : ℤ) :: f 33)) 34 ((dpN6 P n : ℤ) :: f 34)) 52 ((α2P6 P n : ℤ) :: f 52))
        35 ((αN6 P n : ℤ) :: f 35)) 36 (1 :: f 36)))
      (IntMul.Kappa.R6.cPar a c P.x (bP6 n) (b'P6 P n) * kU Bb)

Context. Round-six setup, part 5: the parameter phase

From n (register 23) and b = lg n (register 24) the program parP computes d (25, a count of x ∈ [1, b] with x^c ≤ b^a, ε = a/c), b' (29), p (30), L (31, a count), ℓ (32), h (33), d' (34), α² = ⌊p/(48d)⌋ (52), α (35, a count over [1, b']) and the start value 1 of the product (36).

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