Round-six lemma `swapE_le`

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.R6CrtCost):

theorem NLogN.KFUU.R6Crt.swapE_le (τ K : ℝ) (hK : 0 ≤ K) (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) (w u : ℕ) (sh : Shape)
    (p T ℓ d : ℕ) (hlen : sh.length = 5) (hvol : vol sh = T) (hw : w = p + 2) (hp : 6 ≤ p)
    (hu : u ≤ ℓ * d) (hℓ : 1 ≤ ℓ) (hsz : Nat.size T + w + u + 1 ≤ 4 * p) (hpT : p ≤ T) :
    cSwNτ τ K w u sh ≤ K * (4 * (T : ℝ) * p * ((ℓ : ℝ) * ((d : ℝ) * Real.log p) ^ τ) +
      96 * (T : ℝ) * p)

Context. CRT reversal §11: the cost arithmetic

• cFwdE_nat, cBwdE_nat: the cost of phiFE / phiBE is at most the frozen natCost (the part of KFUU's Φ other than its phase-2 swaps) plus cP2E.
• cP2E_split: cP2E = rest + 3 ⌈cSwNτ …⌉.
• T0_le, rest_le: with V_T = 2T, w = p + 2, d + 1 ≤ 2^h and T large, both nat parts are O((d+1) T p).
• swapE_le: one composite swap costs ≤ 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*).