Round six: the parameter map is admissible for all large n

Let $P$ be a round-six parameter record satisfying Prm.Ok. For an input length $n$ the round-six parameter map sets $b = \lg n$, $b' = b^{1+x}$, $p = 6b'$, $L$ minimal with $4n \le 2^L b'$, $T = 2^L$, $d = \lfloor b^{\varepsilon} \rfloor$, $\ell = \lceil L/d \rceil$, $\alpha^2 = \lfloor p/(48d) \rfloor$ and the bit volume $V = Tp$.

Then there is $n_1$ such that for every $n \ge n_1$ all the size facts collected in Good P n hold (among them $24n \le V \le 48n$, the bands $b^{\varepsilon}/2 \le d \le b^{\varepsilon}$, $\ell \le 4 b^{1-\varepsilon}$ and positivity of all parameters):

In Lean:

theorem IntMul.Kappa.R6.params6_ok (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → Good P 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*).