Round-six lemma `cParA_U`
ProvedJ6Seg.ATab.cParA_UAn 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.J6AILTab14):
theorem J6Seg.ATab.cParA_U : J6A.PA.cParA W p (sWidth p α) ≤ 100 * ((W + 1) * U W)
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
variable {W p t α pkA pkC bA bC : ℕ} (h : CB W p t α pkA pkC bA bC)
include h
theorem J6Seg.ATab.cParA_U : J6A.PA.cParA W p (sWidth p α) ≤ 100 * ((W + 1) * U W) := by sorry