The `A` axis step is the list pipeline (round six, `pipeA6_eq_r6`)
ProvedJ6Seg.pipeA6_eq_r6The A axis step is the list pipeline (round-six regime).
The following holds (Lean statement, in the scope of module Solutions.J6AIL9):
theorem J6Seg.pipeA6_eq_r6 (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, ∀ L : List GI,
L.length = (List.ofFn (tD6 P n D)).prod →
pipeA6 P n src D k L = J6A.pipeAL (pP6 P n) (src k) (tF6 P n k) (αN6 P n) (HA6 P n)
(preT P n D k) (postT P n D k) L
Context. A lines, IL side 9: the pipeline is the axis step pipeA6
pipeA6_eq: for an array of length pre · (t_k · post_k), the k-th A axis step
pipeA6 P n src D k equals the list pipeline J6A.pipeAL (copies, gather slab pass,
regrouping, kernel pass, compress slab pass) at p = pP6, s = s_k, t = t_k, α = αN6,
H = HA6 (= J6A.PA.HH (pP6 P n) (αN6 P n)), under the numeric side conditions of
J6A.pipeAL_rep.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs63 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function open IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf
theorem J6Seg.pipeA6_eq_r6 (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, ∀ L : List GI,
L.length = (List.ofFn (tD6 P n D)).prod →
pipeA6 P n src D k L = J6A.pipeAL (pP6 P n) (src k) (tF6 P n k) (αN6 P n) (HA6 P n)
(preT P n D k) (postT P n D k) L := by sorry