Round-six lemma `numCtx`
ProvedJ6A.NC.numCtxAn 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.J6AIL19):
theorem J6A.NC.numCtx (P : Prm) (hP : P.Ok) (K : ℕ) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, Ctx P n src D k K
Context. A lines, IL side 19: the numerical context of AStepNeed6
numCtx P hP K: for large n, on every axis k, with W = L + 2p + 10: the geometry of
axA_geom, pre · (t · post) = T, 64 T < 2^W, the descriptor entries below 2^W,
sWidth p α + 4 ≤ W, W + 4 ≤ 3p, p + 1 ≤ t, K t p⁶ ≤ T and T p ≤ cU6 P n A / (D + 1).
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 J6A J6A.NC open IntMul NLogN IntMul.Kappa.R6 J6Seg
theorem J6A.NC.numCtx (P : Prm) (hP : P.Ok) (K : ℕ) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, Ctx P n src D k K := by sorry