The cost of the set-up (round six, `cNat_le`)
ProvedJ6Seg.ATab.cNat_leThe cost of the set-up.
The following holds (Lean statement, in the scope of module Solutions.J6AILTab14):
theorem J6Seg.ATab.cNat_le {W p s t α pkA pkC bA bC : ℕ} (h : CB W p t α pkA pkC bA bC) :
cNat W p t α pkA pkC bA bC (W + 1)
(tabA p s t α (pkA * p + pkC) (bA * p + bC)).length + 2 ≤ 10 ^ 45 * (W + 40) ^ 12
Context. A lines, table set-up, part 14: the cost of the native pair is polynomial in W
With the unit U W = 10^42 (W+40)^10 (≥ every expression, expNeg/expPos call and stack
move), and every loop count ≤ W (CB): cNat … + 2 ≤ 10^45 (W+40)^12 and
cTear … + 2 ≤ 10^45 (W+40)^12 (cNat_le, cTear_le).
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 Function
theorem J6Seg.ATab.cNat_le {W p s t α pkA pkC bA bC : ℕ} (h : CB W p t α pkA pkC bA bC) :
cNat W p t α pkA pkC bA bC (W + 1)
(tabA p s t α (pkA * p + pkC) (bA * p + bC)).length + 2 ≤ 10 ^ 45 * (W + 40) ^ 12 := by sorry