theorem Supersingular.trace_eq_zero_of_dvd_of_sq_le {p : ℕ} (t : ℤ) (hp5 : ↑p ≥ 5) (hle : t ^ 2 ≤ 4 * ↑p) (hdvd : ↑p ∣ t) : t = 0

Auxiliary number-theoretic fact: if t = k * p satisfies t^2 ≤ 4p with p ≥ 5, then t = 0. Used to deduce that, for p ≥ 5, the only multiple of p in the Hasse interval [-2√p, 2√p] is zero.

theorem Supersingular.trace_sq_le_four_mul_prime (p : ℕ) [Fact (Nat.Prime p)] (E : WeierstrassCurve.Affine (ZMod p)) : Hasse.traceFrobenius E ^ 2 ≤ 4 * ↑p

Restatement of the Hasse bound |t|^2 ≤ 4q (Theorem 7.3) specialized to a prime field ZMod p: the trace of Frobenius t = tr π_E of an affine Weierstrass curve over ℤ/pℤ satisfies t^2 ≤ 4p.

theorem Supersingular.trace_dvd_iff_trace_eq_zero (p : ℕ) [hp : Fact (Nat.Prime p)] (hp3 : p > 3) (E : WeierstrassCurve.Affine (ZMod p)) : ↑p ∣ Hasse.traceFrobenius E ↔ Hasse.traceFrobenius E = 0

For E/F_p with p > 3, the prime p divides the trace of Frobenius tr π_E if and only if tr π_E = 0. This is the bridge between the divisibility characterization of supersingularity (Theorem 13.3) and the trace-zero characterization (Corollary 13.4).

theorem Supersingular.trace_zero_iff_card_eq (p : ℕ) [Fact (Nat.Prime p)] (E : WeierstrassCurve.Affine (ZMod p)) : Hasse.traceFrobenius E = 0 ↔ ↑(Hasse.numPoints E) = ↑p + 1

For E/F_p with p prime, tr π_E = 0 iff #E(F_p) = p + 1, since tr π_E = (p + 1) - #E(F_p) by definition.

theorem Supersingular.supersingular_iff_trace_eq_zero (p : ℕ) [hp : Fact (Nat.Prime p)] (hp3 : p > 3) (E : WeierstrassCurve.Affine (ZMod p)) : OrdinarySupersingular.IsSupersingular E p ↔ Hasse.traceFrobenius E = 0

Half of Corollary 13.4: for E/F_p with p > 3 prime, E is supersingular iff tr π_E = 0.

theorem Supersingular.supersingular_iff_card_eq (p : ℕ) [Fact (Nat.Prime p)] (hp3 : p > 3) (E : WeierstrassCurve.Affine (ZMod p)) : OrdinarySupersingular.IsSupersingular E p ↔ ↑(Hasse.numPoints E) = ↑p + 1

Corollary 13.4: for E/F_p with p > 3 prime, E is supersingular iff #E(F_p) = p + 1.