theorem even_of_sq_eq_prime_pow (p : ℕ) (hp : Nat.Prime p) (n k : ℕ) : k ^ 2 = p ^ n → Even n

Number-theoretic lemma: if k² = pⁿ for a prime p and natural number k, then n is even. Proved by strong induction on n using that primes are not squares.

theorem even_of_int_sq_eq_four_mul_prime_pow (p : ℕ) (hp : Nat.Prime p) (n : ℕ) (t : ℤ) (h : t ^ 2 = 4 * ↑p ^ n) : Even n

Integer analogue: if an integer satisfies t² = 4·pⁿ for a prime p, then n is even. This is used to detect when tr π_E)² = 4q forces special behavior over even-degree extensions.

theorem frobeniusNotInt_of_odd_or_ordinary {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP F p] (n : ℕ) (hcard : Fintype.card F = p ^ n) (E : WeierstrassCurve.Affine F) (h : Odd n ∨ OrdinarySupersingular.IsOrdinary E p) : EndomorphismRingOverFiniteField.frobeniusNotInt E

Under the hypotheses of Corollary 13.7, the Frobenius endomorphism is not an integer. Concretely: if #F = pⁿ and either n is odd or E is ordinary, then the Frobenius π_E does not satisfy tr(π_E)² = 4q (i.e. is not a scalar multiple of the identity). This is the key technical step toward showing that End⁰(E) = ℚ(π_E) is an imaginary quadratic field.

theorem endAlg_imagQuad_of_ordinary_or_odd {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP F p] (n : ℕ) (hcard : Fintype.card F = p ^ n) (E : WeierstrassCurve.Affine F) (h : Odd n ∨ OrdinarySupersingular.IsOrdinary E p) : EndomorphismRingOverFiniteField.frobeniusDiscriminant E < 0 ∧ Module.finrank ℚ (EllipticCurve.EndAlgebra E) = 2 ∧ ∃ (α : EllipticCurve.EndAlgebra E), (∀ (q : ℚ), α ≠ (algebraMap ℚ (EllipticCurve.EndAlgebra E)) q) ∧ ∃ d < 0, α * α = (algebraMap ℚ (EllipticCurve.EndAlgebra E)) d

Corollary 13.7 (Sutherland §13.1). Let E be an elliptic curve over 𝔽_q with q = pⁿ. If n is odd or E is ordinary, then End⁰(E) = ℚ(π_E) ≃ ℚ(√D) is an imaginary quadratic field with D = (tr π_E)² - 4q. Concretely we extract three pieces of data: (1) the Frobenius discriminant is negative; (2) the endomorphism algebra has ℚ-dimension 2; (3) it contains an element α ∉ ℚ with α² ∈ ℚ_{<0} (an imaginary generator).