Round-six lemma `compS`

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.compS {dA : Fin HS} (h30 : 30 ≤ dA.val) (h31 : dA.val ≤ 31) {ju jd : Fin Pp}
    (hju : iprog ju = J6A.SL.slUp (J6A.SL.cP1 dA) 7 4) (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 α))
    (hpre : 0 < pre) (hpost : 0 < post) (hB : 64 * (pre * (t * post)) < 2 ^ W) {C : ℝ}
    (hC1 : ((J6A.SL.cC1 W p (sWidth p α) t + J6Seg.Src.ctlPhC W (4 * t) t +
      J6A.SL.cTail W + 2 : ℕ) : ℝ) ≤ C)
    (hC2 : (((4 * t + 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 (M * 8 * (8 * J6A.PA.HH p α)) t (J6A.srcC (J6A.PA.HH p α) (8 * J6A.PA.HH p α)) (fun _ => 0))
        pre post t [] []) 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*).