The coefficients at τ₁₆₃ (Milla, ch. 10)

The arithmetic half of the proof, specialized to τ₁₆₃ = (1 + i√163)/2:

• jwert_τ₁₆₃ : 1728·J(τ₁₆₃) = −640320³;
• s₂_τ₁₆₃ : s₂(τ₁₆₃) = 77265280/90856689, equivalently (1 − s₂(τ₁₆₃))/6 = 13591409/545140134;
• theohud : Milla's final form √(640320³)/(12π) = ∑ n, (6n)!/((3n)!(n!)³)·(13591409 + 545140134·n)/(−640320³)ⁿ.

The proofs (Phase D2 of the PLAN) combine the estimates of ch. 5 (Estimates.lean), verified numerics (Numerics.lean) and the integrality/rationality inputs of Phase C (SingularModuli.lean, with the auxiliary-number bookkeeping b₁₆₃ = 10996566783048, a₁₆₃ = 9351571368960 from the paper's satzhilfszahlen): an algebraic integer that is rational is an integer, and an integer within distance < 1/2 of a certified numerical approximation is determined exactly.

theorem Chudnovsky.jwert_τ₁₆₃_of (hjm : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) : 1728 * J τ₁₆₃ = -640320 ^ 3

Milla's jwert2 at N = 163, from the integrality input 1728·J(τ₁₆₃) ∈ ℤ as an explicit hypothesis: the singular value 1728·J(τ₁₆₃) = −640320³.

theorem Chudnovsky.jwert_τ₁₆₃ : 1728 * J τ₁₆₃ = -640320 ^ 3

Milla's jwert2 at N = 163: the singular value 1728·J(τ₁₆₃) = −640320³.

theorem Chudnovsky.J_τ₁₆₃_of (hjm : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) : J τ₁₆₃ = -↑(640320 ^ 3 / 1728)

J(τ₁₆₃) itself, as a rational number, from the integrality input as a hypothesis.

theorem Chudnovsky.J_τ₁₆₃ : J τ₁₆₃ = -↑(640320 ^ 3 / 1728)

J(τ₁₆₃) itself, as a rational number.

theorem Chudnovsky.s₂_τ₁₆₃_of (hjm : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) (hsr : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r) : s₂ τ₁₆₃ = ↑(77265280 / 90856689)

Milla's s2nenner/satzhilfszahlen at N = 163, from the integrality and rationality inputs as explicit hypotheses: s₂(τ₁₆₃) = 77265280/90856689.

theorem Chudnovsky.s₂_τ₁₆₃ : s₂ τ₁₆₃ = ↑(77265280 / 90856689)

Milla's s2nenner/satzhilfszahlen at N = 163: s₂(τ₁₆₃) = 77265280/90856689.

theorem Chudnovsky.one_sub_s₂_τ₁₆₃_div_six_of (hjm : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) (hsr : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r) : (1 - s₂ τ₁₆₃) / 6 = ↑(13591409 / 545140134)

The combination entering the Chudnovsky formula, from the integrality and rationality inputs as hypotheses: (1 − s₂(τ₁₆₃))/6 = 13591409/545140134.

theorem Chudnovsky.one_sub_s₂_τ₁₆₃_div_six : (1 - s₂ τ₁₆₃) / 6 = ↑(13591409 / 545140134)

The combination entering the Chudnovsky formula: (1 − s₂(τ₁₆₃))/6 = 13591409/545140134.

theorem Chudnovsky.theohud_of (hjm : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m) (hsr : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r) : ↑√(640320 ^ 3) / (12 * ↑Real.pi) = ∑' (n : ℕ), ↑(6 * n).factorial / (↑(3 * n).factorial * ↑n.factorial ^ 3) * ((13591409 + 545140134 * ↑n) / (-640320 ^ 3) ^ n)

Milla's theohud: the Chudnovsky formula in the paper's normalization, √(640320³)/(12π) = ∑ n, (6n)!/((3n)!(n!)³)·(13591409 + 545140134·n)/(−640320³)ⁿ, obtained by substituting τ = τ₁₆₃ into the Main Theorem; from the integrality and rationality inputs as explicit hypotheses.

theorem Chudnovsky.theohud : ↑√(640320 ^ 3) / (12 * ↑Real.pi) = ∑' (n : ℕ), ↑(6 * n).factorial / (↑(3 * n).factorial * ↑n.factorial ^ 3) * ((13591409 + 545140134 * ↑n) / (-640320 ^ 3) ^ n)

Milla's theohud: the Chudnovsky formula in the paper's normalization, √(640320³)/(12π) = ∑ n, (6n)!/((3n)!(n!)³)·(13591409 + 545140134·n)/(−640320³)ⁿ, obtained by substituting τ = τ₁₆₃ into the Main Theorem.