The `A` chain (round six, `axA_chain`)

The A chain.

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

theorem J6Seg.Ax.axA_chain {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {dA : Fin HS}
    {desc : List ℤ} {st1 st2 st3 st4 st5 st6 st7 st8 : IStmt HS Pp}
    {C1 C2 C3 C4 C5 C6 C7 C8 : ℝ} (hA0 : dA ≠ 0)
    {p s t α H pre post M f w w' : ℕ} {X0 : ℤ}
    (hM : t / (16 * H) = M) (hf : 2 ^ f = 8 * H) (ht0 : 0 < t) (hp : 0 < post)
    (hsG : MonoSrc (32 * t) (8 * (M * (8 * H))) (J6A.srcG s t H (J6A.WA p α H) M (8 * H)))
    (h1 : PassOK Isym tbl st1 dA desc (fun L => L.length = pre * (t * post) ∧ GB w L)
      (J6A.dupL 32) C1)
    (h2 : PassOK Isym tbl st2 dA desc
      (fun L => L.length = 1 * (2 ^ 5 * (pre * (t * post))) ∧ GB w L)
      (blkT (2 ^ 5) (pre * (t * post)) 1) C2)
    (h3 : PassOK Isym tbl st3 dA desc (fun L => L.length = pre * (2 ^ 5 * (t * post)) ∧ GB w L)
      (blkT (t * post) (2 ^ 5) pre) C3)
    (h4 : PassOK Isym tbl st4 dA desc
      (fun L => L.length = pre * (32 * t * post) ∧ ∀ u ∈ gflat L, zsz u ≤ w)
      (slabPass (32 * t) (8 * (M * (8 * H))) post (J6A.srcG s t H (J6A.WA p α H) M (8 * H))
        (fun _ z => z)) C4)
    (h5 : PassOK Isym tbl st5 dA desc
      (fun L => L.length = pre * (2 ^ 3 * (M * (8 * H) * post)) ∧ GB w L)
      (blkT (2 ^ 3) (M * (8 * H) * post) pre) C5)
    (h6 : PassOK Isym tbl st6 dA desc
      (fun L => L.length = pre * M * (2 ^ 3 * (8 * H * post)) ∧ GB w L)
      (blkT (8 * H * post) (2 ^ 3) (pre * M)) C6)
    (h7 : PassOK Isym tbl st7 dA desc
      (fun L => L.length = pre * (M * 8) * (2 ^ f * post) ∧ GB w L ∧
        ∀ b < pre * (M * 8), ∀ c < post,
          (fun x : List GI => x.length = 8 * H ∧ KR.AB X0 x) (lineAt (2 ^ f) post L b c))
      (kerPass (2 ^ f) post (pre * (M * 8))
        (fun b => J6A.gK p s t α H (8 * H) (b % (M * 8)))) C7)
    (h8 : PassOK Isym tbl st8 dA desc
      (fun L => L.length = pre * (M * 8 * (8 * H) * post) ∧ ∀ u ∈ gflat L, zsz u ≤ w')
      (slabPass (M * 8 * (8 * H)) t post (J6A.srcC H (8 * H)) (fun _ z => z)) C8)
    (hAB : ∀ x : List GI, GB w x → KR.AB X0 x)
    (hgl : ∀ q x, x.length = 8 * H → (J6A.gK p s t α H (8 * H) q x).length = 8 * H)
    (hgB : ∀ q < M * 8, ∀ x : List GI, x.length = 8 * H → KR.AB X0 x →
      GB w' (J6A.gK p s t α H (8 * H) q x)) :
    PassOK Isym tbl (axAProg st1 st2 st3 st4 st5 st6 st7 st8) dA desc
      (fun L => L.length = pre * (t * post) ∧ GB w L) (J6A.pipeAL p s t α H pre post)
      (C1 + C2 + C3 + C4 + C5 + C6 + C7 + C8)

Context. A-line axis program (AxisUA6), part 4: the eight-step chain of pipeAL

The A per-axis pipeline J6A.pipeAL p s t α H pre post (J6AIL6) is the composition of eight one-array steps (M = t / 16H, 2^f = 8H, N = pre · t · post):

1. dupL 32 (the copies), 2. blkT 2^5 N 1 (fine exposure, forward),
2. blkT (t·post) 2^5 pre (back), 4. the gather slab pass (srcG),
3. blkT 2^3 (M·8H·post) pre, 6. blkT (8H·post) 2^3 (pre·M) (rgp),
4. the kernel pass kerPass 2^f post (pre·8M) (gK ∘ (· % 8M)),
5. the compress slab pass (srcC).

axA_chain: PassOK steps for these maps (with their natural preconditions: the length, GB w before the kernel, GB w' after it) compose to a PassOK step for pipeAL with the precondition |L| = N ∧ GB w L. Also the value-bound helpers GB_dupL, GB_blkTg, GB_lineAt, GB_of_LRep, GB_slabId.

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