The chain (round six, `axis_chain`)

The chain.

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

theorem J6Seg.Ax.axis_chain {st1 st2 stc st3 st4 st5 st6 sts st7 : IStmt HS Pp}
    {P1 P2 P3 P4 P5 P6 : List GI → Prop} {Pc Ps P7 : List GI → List GI → Prop}
    {g1 g2 g3 g4 g5 g6 : List GI → List GI} {g7 : List GI → List GI → List GI}
    {C1 C2 Cc C3 C4 C5 C6 Cs C7 : ℝ}
    (h1 : PassOK Isym tbl st1 dA desc P1 g1 C1) (h2 : PassOK Isym tbl st2 dA desc P2 g2 C2)
    (hc : Pass2OK Isym tbl stc dA desc Pc (fun A _ => (A, A)) Cc)
    (h3 : PassOK Isym tbl st3 dA desc P3 g3 C3) (h4 : PassOK Isym tbl st4 dA desc P4 g4 C4)
    (h5 : PassOK Isym tbl st5 dA desc P5 g5 C5) (h6 : PassOK Isym tbl st6 dA desc P6 g6 C6)
    (hs : Pass2OK Isym tbl sts dA desc Ps (fun A B => (B, A)) Cs)
    (h7 : Pass2OK Isym tbl st7 dA desc P7 (fun A B => (g7 A B, [])) C7)
    (hZ0 : sZ ≠ (0 : Fin HS)) (hZA : sZ ≠ dA) (hA0 : dA ≠ 0)
    (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l : List ℤ)
    (hF : ∀ j, j ≠ 0 → j ≠ dA → F j = []) (hd : F dA = desc) (h0 : F 0 = gflat L ++ l)
    (hp1 : P1 L) (hp2 : P2 (g1 L)) (hpc : Pc (g2 (g1 L)) [])
    (hp3 : P3 (g2 (g1 L))) (hp4 : P4 (g3 (g2 (g1 L)))) (hp5 : P5 (g4 (g3 (g2 (g1 L)))))
    (hp6 : P6 (g5 (g4 (g3 (g2 (g1 L))))))
    (hps : Ps (g6 (g5 (g4 (g3 (g2 (g1 L)))))) (g2 (g1 L)))
    (hp7 : P7 (g2 (g1 L)) (g6 (g5 (g4 (g3 (g2 (g1 L))))))) :
    ∃ c : ℕ, IRuns Isym tbl (axProg st1 st2 stc st3 st4 st5 st6 sts st7) (encK s F)
      (encK s (update F 0
        (gflat (g7 (g2 (g1 L)) (g6 (g5 (g4 (g3 (g2 (g1 L))))))) ++ l))) c ∧
      (c : ℝ) ≤ C1 + C2 + Cc + C3 + C4 + C5 + C6 + Cs + C7

Context. B-line axis program (AxisU6), part 1: the pass contracts and the chain

The axis program of AxisBody6 is a sequence of passes, each in the convention of FineBody6 (only stack 0, the descriptor stack dA and, for the two-array steps, rZ = 53 are nonempty):

pass1 (slabSc) ; pass2 (chunk kernel) ; copy (Y → rZ) ; pass3 (gather) ; pass4 (J kernel) ;
pass5 (scatter) ; pass6 (chunk kernel) ; swap (0 ↔ rZ) ; pass7 (slabOut)

• PassOK Isym tbl st dA desc Pre g C: st maps the array L on stack 0 to g L (precondition Pre L), reading desc on dA, cost ≤ C.
• Pass2OK Isym tbl st dA desc Pre g C: the same for the pair (stack 0, stack rZ): (A, B) ↦ g A B. The copy is g A [] = (A, A), the swap g A B = (B, A), the output pass g Y Y₂ = (out, []).
• axis_chain: the nine steps compose (the copy of Y on rZ is carried through passes 3–6 in the base state).

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