Singular moduli at τ₁₆₃: the cited arithmetic inputs (Phase C)

Milla's paper (arXiv:1809.00533v6) does not prove the following three statements; it cites them from the literature, and they are the main open risk of this formalization (PLAN Phase C):

1. isIntegral_j_τ₁₆₃ : j(τ₁₆₃) = 1728·J(τ₁₆₃) is an algebraic integer [Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Thm. II.6.1];
2. j_τ₁₆₃_rational : j(τ₁₆₃) has degree h(-163) = 1 over ℚ, hence is rational [Silverman ATAEC II.4.3(b), together with h(-163) = 1 from Buell, Binary Quadratic Forms];
3. s₂_τ₁₆₃_rational : s₂(τ₁₆₃) ∈ ℚ(j(τ₁₆₃)) = ℚ [Masser, Elliptic Functions and Transcendence (1975), Appendix A1, Thm. A1; Masser's Ψ(τ) is (3/2)·s₂(τ)].

Their combination j_τ₁₆₃_integer (a rational algebraic integer is an integer) is what ch. 10 actually consumes, together with statement 3.

Everything else in the development (Phases A, B, D) can be completed with these as explicit hypotheses, giving the intermediate milestone chudnovsky_of_singular_moduli (PLAN Phase C).

theorem Chudnovsky.isIntegral_j_τ₁₆₃ : IsIntegral ℤ (1728 * J τ₁₆₃)

Cited input 1 [Silverman ATAEC II.6.1]. The value of the j-invariant j = 1728·J at the CM point τ₁₆₃ = (1 + i√163)/2 is an algebraic integer.

theorem Chudnovsky.j_τ₁₆₃_rational : ∃ (r : ℚ), 1728 * J τ₁₆₃ = ↑r

Cited input 2 [Silverman ATAEC II.4.3(b); Buell]. The degree of j(τ₁₆₃) over ℚ is the class number h(-163) = 1, so j(τ₁₆₃) is rational.

theorem Chudnovsky.s₂_τ₁₆₃_rational : ∃ (r : ℚ), s₂ τ₁₆₃ = ↑r

Cited input 3 [Masser 1975, Thm. A1]. Ramanujan's function s₂ is rational at τ₁₆₃: s₂(τ) ∈ ℚ(j(τ)) at CM points, and here ℚ(j(τ₁₆₃)) = ℚ.

theorem Chudnovsky.j_τ₁₆₃_integer : ∃ (m : ℤ), 1728 * J τ₁₆₃ = ↑m

Combination of isIntegral_j_τ₁₆₃ and j_τ₁₆₃_rational: a rational algebraic integer is an integer, so j(τ₁₆₃) = 1728·J(τ₁₆₃) ∈ ℤ. (Ch. 10 then pins it down to -640320³ using the numeric bounds of Phases A5/D1.)