One line through the seven passes is `lineB` (round six, `pipeLine_eq`)

One line through the seven passes is lineB.

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

theorem J6Seg.pipeLine_eq (hl : 1 ≤ lam) (hst : s ≤ t) (hN : nc * lam = t)
    (hG : (LJ s t lam w).length ≤ G) (y : List (ℤ × ℤ)) :
    let N := nc * lam
    let S := slabLine N (selSrc s t) (selH p P) y
    let Y := chunksG (fun q => liftG (chunkK P R s t lam α q)) lam nc S
    let Jl := slabLine G (jSrc s t lam w) (fun _ z => z) Y
    let W := liftG (jKer P R s t lam w α K G) Jl
    let Wp := slabLine N (scSrc s t lam w) (fun _ z => z) W
    let Y2 := chunksG (fun q => liftG (chunkK P R s t lam α q)) lam nc Wp
    slabLine N (fun l => some l) (outH p P s t α) (List.zip Y Y2) =
      lineB p P R s t lam w α K nc y

Context. B-line machine, sweep 3: the B₀ axis map as seven passes

On a (pre, N, post) array of Gaussian items (N = n_c λ), the in-place B₀ line map of the axis (axisL N post (lineB …)) is computed by (axisPipe):

1. a selection slab pass (row rowSel l, scaled by 2^{P-p-1}, zeros for l ≥ s);
2. the chunk kernel chunkK on every λ-chunk (one λ-exposure);
3. a slab gather of the m near-boundary rows LJ (padded to G rows);
4. the J kernel (fwdK, bwdK, coupling window) on every G-row (one G-exposure);
5. a slab scatter back to the N rows;
6. the chunk kernel again;
7. the output slab pass on the pair (Y, Y₂): outE l (Y - Y₂).

Real and imaginary parts are carried together (liftG). axisPipe_eq proves the equality.

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