Round-six lemma `monoSrc_G`

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

theorem J6A.monoSrc_G (hH : 1 ≤ H) (hM : 0 < M) (hwin : 0 < win) (ht : t = M * 8 * (2 * H))
    (hWs : W ≤ s) (hst : s ≤ t) (hsep : 2 * W * t ≤ 16 * H * s) (hWw : 2 * W ≤ win) :
    MonoSrc (32 * t) (8 * (M * win)) (srcG s t H W M win)

Context. A lines, IL side 6: the per-axis pipeline at the list level

On a (pre, t, post) array the A line map of an axis is computed by six list passes, each of which has an IL counterpart:

1. cpy 32 t post pre: the lines X become dupL 32 X (32 copies);
2. the gather slab pass slabPass (32 t) (8 (M win)) post (srcG …): output slab l = (r M + j) win + e (r < 8, j < M, e < win) is, for e < 2W, the input X[(jc_b - W + e) mod s] of block b = 8 j + r, read from copy 4 r + c (c ∈ {0,1,2} handles the wrap-around, posE), and 0 otherwise; inside a class r the windows of the blocks r, r + 8, … are disjoint and increasing, so the source is monotone;
3. rgp 8 M win: the windows become rows; row b' holds the window of block b' % (8M);
4. the kernel pass kerPass win post (pre·8M) (fun b => gK (b % 8M)) (gK q the per-block kernel aKerL with the tables of block q);
5. the compress slab pass slabPass (8M win) t post srcC: output k is entry k % 2H of row k / 2H.

pipeAL_rep: the result represents the lines (range t).map (chirpC p s t α H U_X); pipeAL_eq: the pipeline is axisL t post of that line map. monoSrc_G, monoSrc_C: the two sources are monotone (the IL slab passes need this).

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