Round-six lemma `gathS`

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

theorem J6A.LF.gathS {dA : Fin HS} (h30 : 30 ≤ dA.val) (h31 : dA.val ≤ 31) {ju jd : Fin Pp}
    (hju : iprog ju = J6A.SL.slUp (J6A.SL.gP1 dA) 7 12) (hjd : iprog jd = J6A.SL.slDn.code)
    {k pre post sr t p α d W M : ℕ} (hL : ∀ x ∈ J6A.PA.dL k pre post sr t p α d, |x| < 2 ^ W)
    (hp : 1 ≤ p) (hα : 1 ≤ α) (hmW : sWidth p α + 4 ≤ W)
    (hMd : M = t / (16 * J6A.PA.HH p α)) (hM : 0 < M) (htM : t = M * 8 * (2 * J6A.PA.HH p α))
    (hWs : J6A.WA p α (J6A.PA.HH p α) ≤ sr) (hst : sr ≤ t)
    (hsep : 2 * J6A.WA p α (J6A.PA.HH p α) * t ≤ 16 * J6A.PA.HH p α * sr)
    (hWw : 2 * J6A.WA p α (J6A.PA.HH p α) ≤ 8 * J6A.PA.HH p α)
    (hpre : 0 < pre) (hpost : 0 < post) (hB : 64 * (pre * (t * post)) < 2 ^ W) {C : ℝ}
    (hC1 : ((J6A.SL.cG1 W p (sWidth p α) (4 * t) + J6Seg.Src.ctlPhC W (32 * t) (4 * t) +
      J6A.SL.cTail W + 2 : ℕ) : ℝ) ≤ C)
    (hC2 : (((32 * t + 4 * t + 1) * ((2 + 1) * J6Seg.Src.uC W J6Seg.Src.DD +
        J6Seg.Src.uC W J6Seg.Src.DD) + (4 + 1) * J6Seg.Src.uC W J6Seg.Src.DD + 2 : ℕ) : ℝ) ≤ C) :
    SetupS I iprog (.call ju) (.call jd) ρS dA (J6A.PA.dL k pre post sr t p α d)
      (slabV (J6Seg.ctlOf (32 * t) (8 * (M * (8 * J6A.PA.HH p α)))
        (J6A.srcG sr t (J6A.PA.HH p α) (J6A.WA p α (J6A.PA.HH p α)) M (8 * J6A.PA.HH p α)) (fun _ => 0))
        pre post (8 * (M * (8 * J6A.PA.HH p α))) [] []) C

Context. A lines, IL side 20: the leaves in contract form

For a descriptor stack dA ∈ {30, 31} holding dL k pre post s t p α d (entries below 2^W):

• dupS: .call j with iprog j = (dupP dA).code is a PassOK step for dupL 32;
• fineS: .call ju / .call jd with fsUp dA ea ey fl dF / fsDn dF is a SetupS pair on ![dF] building descFine (p + 2) fl a y;
• gathS / compS: slUp (gP1 dA) 7 12 / slDn and slUp (cP1 dA) 7 4 / slDn are SetupS pairs on ρS building the gather / compress slab register files,

each with its explicit cost (plus 2 for the call) below a given C.

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