`AStepNeed6` (round six, `aStepNeed6_all`)
ProvedJ6A.AS.aStepNeed6_allAStepNeed6 for every parameter record.
The following holds (Lean statement, in the scope of module Solutions.J6AIL22):
theorem J6A.AS.aStepNeed6_all (P : Prm) (hP : P.Ok) : J6Seg.Ax.AStepNeed6 P
Context. A lines, IL side 22: AStepNeed6
The family aU dA dF (13 procedures): the copy step dupP dA; four fine set-up / tear-down pairs
fsUp dA ea ey fl dF / fsDn dF; the gather and compress slab pairs slUp (gP1 dA) 7 12 / slDn,
slUp (cP1 dA) 7 4 / slDn. With W = L + 2p + 10 every cost is at most 10^16 · T · p ≤ 10^16 · cU6 P n 0 / (D + 1) (J6A.NC.numCtx, J6A.BD.fineC/gathC/compC/dupC).
aStepNeed6_all : ∀ P, P.Ok → AStepNeed6 P.
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_Defs68 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6A J6A.AS open IntMul NLogN NLogN.KIL NLogN.KFB Function NLogN.RS J6Seg.PJ J6A.PA IntMul.Kappa.R6 IntMul.HvdH open J6Seg.Ax (SetupS PassOK ρS slabV sZ Fam)
theorem J6A.AS.aStepNeed6_all (P : Prm) (hP : P.Ok) : J6Seg.Ax.AStepNeed6 P := by sorry