The numeric side of `PreA6` holds in round six (round six, `numA6`)
ProvedJ6Seg.ATab.numA6The numeric side of PreA6 holds in round six.
The following holds (Lean statement, in the scope of module Solutions.J6AILTab15):
theorem J6Seg.ATab.numA6 (P : Prm) (hP : P.Ok) (pkA pkC bA bC : ℕ) : NumA6 P pkA pkC bA bC
Context. A lines, table set-up, part 15: PreA6 in the round-six regime
For P.Ok, eventually every axis satisfies AxF (r6_axis_nat, pre·t·post = 2^L,
L ≤ b' ≤ p), hence AxOK and the loop-count bounds CB at W = Wd …; the costs are
≤ 10^45 (W+40)^12 ≤ K b^12 t^12 p^12, under the budget by budget_ev. So NumA6 holds
(numA6), and preA6: PreA6 P pkA pkC bA bC tab for every P.Ok.
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_Defs69 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.ATab open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH IntMul.Kappa.R6 Function
theorem J6Seg.ATab.numA6 (P : Prm) (hP : P.Ok) (pkA pkC bA bC : ℕ) : NumA6 P pkA pkC bA bC := by sorry