The width conditions (round six, `axOK_of`)
ProvedJ6Seg.ATab.axOK_ofThe width conditions.
The following holds (Lean statement, in the scope of module Solutions.J6AILTab13):
theorem J6Seg.ATab.axOK_of {p s t α d k pre post pkA pkC bA bC : ℕ} (h : AxF p s t α d k pre post) :
AxOK (Wd pkA pkC bA bC p t) (Wd pkA pkC bA bC p t + 1) p s t α pre post k d pkA pkC bA bC
Context. A lines, table set-up, part 13: the width conditions at W = K (p + t + 100)
From the elementary per-axis facts AxF (0 < s < t, 1 ≤ α, α² ≤ p, k < d ≤ p,
pre, post, pre·t·post ≤ 2^p), every width condition AxOK of the native set-up holds at
W = Wd = (40 + pkA + pkC + bA + bC) (p + t + 100), B = W + 1 (axOK_of).
Everything is 2^{O(p + t)}: polynomial quantities are ≤ 2^{11} X⁵ ≤ 2^{5X+11} (X = p+t+100),
the scaled tables are ≤ 2^{16p+35}.
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.axOK_of {p s t α d k pre post pkA pkC bA bC : ℕ} (h : AxF p s t α d k pre post) :
AxOK (Wd pkA pkC bA bC p t) (Wd pkA pkC bA bC p t + 1) p s t α pre post k d pkA pkC bA bC := by sorry