The axis facts, eventually (round six, `axNum_ev`)
ProvedJ6Seg.Side.axNum_evThe axis facts, eventually.
The following holds (Lean statement, in the scope of module Solutions.J6SegSideCost2):
theorem J6Seg.Side.axNum_ev (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, AxNum P n src D k
Context. Side costs 2: the sizes of one round-six axis
AxNum P n src D k: the natural-number facts the side costs need, on axis k
(T = TP6, p = pP6, β = log₂ lg n):
pre · t · post = T, pre, post ≥ 1, p ≤ T, size (2T) ≤ p, Q ≤ 3p, log₂ λ ≤ 2β + 2,
pre · nc · λ · post ≤ T, d · (pre · G · post) ≤ 99 T, log₂ G ≤ ℓ ≤ p, G ≤ 3t,
d ≤ T, lg n < 2^(β+1).
axNum_ev: all of them for large n.
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 J6Seg J6Seg.Side open IntMul NLogN IntMul.Kappa.R6 J6Seg
theorem J6Seg.Side.axNum_ev (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, AxNum P n src D k := by sorry