Glue: from Milla's theohud to Mathlib's chudnovskySum = π⁻¹

Phase D3 of the PLAN: convert Milla's normalization √(640320³)/(12π) = ∑ n, (6n)!/((3n)!(n!)³)·(13591409 + 545140134·n)/(−640320³)ⁿ into Mathlib's statement chudnovskySum = π⁻¹, where chudnovskySum = 12/640320^(3/2) · ∑' n, chudnovskyTerm n. This involves 640320^(3/2 : ℝ) = √(640320³) (rpow lemmas), the ℚ → ℝ coercion of chudnovskyTerm, and inverting both (positive) sides.

The intermediate milestone chudnovsky_of_singular_moduli states the full theorem with the Phase C inputs (SingularModuli.lean) as explicit hypotheses: the paper's proof minus the literature citations (Silverman II.6.1, II.4.3(b), Buell, Masser Thm. A1).

theorem Chudnovsky.summable_chudnovskyTerm : Summable fun (n : ℕ) => ↑(chudnovskyTerm n)

The Chudnovsky series is (absolutely) summable — needed for hauptformel substitution, the series rearrangement, and the final inversion.

theorem Chudnovsky.chudnovsky_of_singular_moduli (h₁ : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) (h₂ : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r) : chudnovskySum = Real.pi⁻¹

Intermediate milestone (PLAN, Phase C): the Chudnovsky formula assuming the singular-moduli inputs — 1728·J(τ₁₆₃) is a (rational) integer and s₂(τ₁₆₃) is rational. Everything else (Phases A, B, D) is proved.

theorem Chudnovsky.chudnovskySum_eq_pi_inv : chudnovskySum = Real.pi⁻¹

Chudnovsky's formula (Mathlib's proof_wanted chudnovskySum_eq_pi_inv).