Round-six lemma `axSteps_at`

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

theorem J6Seg.Ax.axSteps_at {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {dA dF : Fin HS}
    {ρ : Fin 19 → Fin HS} {eF eB eK eJK eC eCd eJ eJd pM : Fin Pp} {pc : ℕ → Fin Pp}
    {u1 d1 u3 d3 u5 d5 u7 d7 : IStmt HS Pp}
    {P : Prm} {ap : AxPlan6} {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} {C₀ Cp Cs Cc : ℝ} (hk : k ≤ D)
    (hMul : MulOK Isym tbl pM NLogN.KFUU.MS) (hK : tbl eK = KR.chunkI2 pM)
    (hJ : tbl eJK = JK.jKprog.code pM pc)
    (hFine : FineBody6 Isym tbl eF eB dF C₀) (hC0 : 0 ≤ C₀)
    (hRC : RegOK ρ KR.dT dF) (hRJ : RegOK ρ JK.dTJ dF) (hρA : ∀ i, ρ i ≠ dA)
    (hfree : SlabFree dA) (hDA : AxC.DAok dA) (h49 : KR.dT ≠ dA) (h33 : JK.dTJ ≠ dA)
    (hSC : SetupBody6 Isym tbl eC eCd ρ dA (descAx6 P n src D k) (chunkRegs6 P n src D k ap.pl) Cp)
    (hSJ : SetupBody6 Isym tbl eJ eJd ρ dA (descAx6 P n src D k) (jRegs6 P n src D k ap.pl) Cp)
    (hS1 : SetupS Isym tbl u1 d1 ρS dA (descAx6 P n src D k) (slabV1 P n src D k) Cs)
    (hS3 : SetupS Isym tbl u3 d3 ρS dA (descAx6 P n src D k) (slabV3 P n src D k) Cs)
    (hS5 : SetupS Isym tbl u5 d5 ρS dA (descAx6 P n src D k) (slabV5 P n src D k) Cs)
    (hS7 : SetupS Isym tbl u7 d7 ρS dA (descAx6 P n src D k) (slabV7 P n src D k) Cs)
    (hReg : AxReg P n src D k) (hTab : TabAt P n src k) (hgC : ChunkOutAt P ap n src k)
    (hV : ValAt P ap n src D k) (hBud : AxBudgetAt P ap n src D k Cc) :
    AxStepsAt Isym tbl (slSt u1 d1 bodySc) (kpSt eC eCd ρ KR.dT dF eF eB eK) (AxC.copyRS dA).code
      (slSt u3 d3 bodyId) (kpSt eJ eJd ρ JK.dTJ dF eF eB eJK) (slSt u5 d5 bodyId)
      (kpSt eC eCd ρ KR.dT dF eF eB eK) (AxC.swapRS dA).code
      (slSt u7 d7 (passP drP rdP (itO pM) bkP)) dA P n src D k
      (8 * Cs + 6 * Cp + (9 + 6 * C₀) * Cc)

Context. B-line axis program (AxisU6), part 9: AxStepsAt from the components

axSteps_at: the nine steps of axis k (slab 1, chunk, copy, gather, J, scatter, chunk, swap, output) with total cost 8 Cs + 6 Cp + (9 + 6 C₀) Cc, from the step lemmas of parts 7 and 8, the copy / swap of J6SegAxCopy (S2), the array lengths (arr_lens) and the value bounds (ValAt).

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