Round-six lemma `crt_absorb`

An 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.R6CrtNeed):

theorem IntMul.Kappa.R6.crt_absorb (P : Prm) (n : ℕ) (hp : 6 ≤ pP6 P n) (K : ℝ) (hK : 0 ≤ K) (c1 : ℕ)
    (c T0 R : ℕ) (x : ℝ) (hx0 : 0 ≤ x)
    (hc : c ≤ c1 * T0 + R + 3 * ⌈x⌉₊)
    (hT0 : T0 ≤ 10 ^ 6 * ((dP6 P n + 1) * TP6 P n * pP6 P n))
    (hR : R ≤ 10 ^ 13 * ((dP6 P n + 1) * TP6 P n * pP6 P n))
    (hx : x ≤ K * (4 * (TP6 P n : ℝ) * pP6 P n *
      ((ℓP6 P n : ℝ) * ((dP6 P n : ℝ) * Real.log (pP6 P n)) ^ P.τ) + 96 * (TP6 P n : ℝ) * pP6 P n)) :
    (c : ℝ) ≤ ((c1 : ℝ) * 10 ^ 6 + 10 ^ 13 + 300 * K + 3) * cU6 P n 0

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