The eventual sizes, for an arbitrary constant `c` (kept abstract (`crt_big_aux`)

The eventual sizes, for an arbitrary constant c (kept abstract: CU is huge).

The following holds (Lean statement, in the scope of module Solutions.R6CrtNeed):

theorem IntMul.Kappa.R6.crt_big_aux (P : Prm) (hP : P.Ok) (c : ℕ) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n →
    Good P n ∧ 2 ≤ dP6 P n ∧ 2 ≤ ℓP6 P n ∧ dP6 P n + 1 ≤ 2 ^ hN6 P n ∧
    (dP6 P n + 2) * (c * (3 * pP6 P n + 1) ^ 2 + 15 * pP6 P n + 10 ^ 4) ≤ TP6 P n

Context. CRT reversal §12: CrtNeed6

crtNeed6 : ∀ P, P.Ok → CrtNeed6 P.

The table is mTab4 tab ext₁ ext0 ext0 ext0 own with ext₁ the table of IL.SwapNeedτ tab P.τ and own = [phiFE, phiBE] (KFUU's uniform Φ, Φ⁻¹ with the reversal revE, whose phase 2 uses three composite swaps of h⌊d/2⌋-bit digits and six digit-selector rotation sets instead of KFUU's ⌊d/2⌋ single-digit swaps). RowUCP is not used.

Cost: c ≤ C₀ · T p · Ncost6 with A = 0, from

• the frozen part (natCost, O((d+1) T p) once d + 1 ≤ 2^h),
• the rest of p2E (O((d+1) T p) once d + 1 ≤ 2^h and T ≥ poly(b)),
• three composite swaps, each ≤ K (4 T p ℓ (d ln p)^τ + 96 T p).

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*).