The pipeline represents the `A` lines (round six, `pipeAL_rep`)

The pipeline represents the A lines.

The following holds (Lean statement, in the scope of module Solutions.J6AIL6):

theorem J6A.pipeAL_rep (p s t α H pre post : ℕ) (hH : 1 ≤ H) {M : ℕ} (hM : 0 < M)
    (ht : t = M * 8 * (2 * H)) (hp : 0 < post) (hWs : WA p α H ≤ s) (hst : s ≤ t)
    (hsep : 2 * WA p α H * t ≤ 16 * H * s) (hWw : 2 * WA p α H ≤ 8 * H)
    {L : List (ℤ × ℤ)} {φ : ℕ → ℕ → List (ℤ × ℤ)} (hL : LRep pre t post L φ) :
    LRep pre t post (pipeAL p s t α H pre post L)
      (fun b c => (List.range t).map (chirpC p s t α H fun j => (φ b c).getD j (0, 0)))

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