Round-six lemma `outP_spec`

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

theorem J6Seg.JK.outP_spec {a b : List ℤ} {l lm : List ℤ} {B : ℕ} (h0 : F 0 = l) (hCR : F CR = [])
    (hM : F HM = (a.length : ℤ) :: lm) (hab : a.length = b.length) (hWR : F WR = a.reverse)
    (hWI : F WI = b.reverse) (haB : Bnd B a) (hbB : Bnd B b) (hzB : zsz (a.length : ℤ) ≤ B) :
    Sp outP (encK s F) (encK s (update (update (update F 0 (gflat (a.zip b) ++ l)) WR []) WI []))
      (a.length * 10 ^ 5 * (B + 2) + 10 ^ 5 * (B + 2))

Context. B-line IL, the J kernel (B4), part 12: the Gaussian row in and out

• unzP: the row gflat x on stack 0 is split into its real and imaginary parts (RE = (x.map fst).reverse, IM = (x.map snd).reverse);
• zerP: G - m zero pairs onto stack 0;
• outP: the outputs WR = a.reverse, WI = b.reverse (|a| = |b| = m) interleaved onto stack 0: gflat (a.zip b).

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