hasse_implies_arccos_valid

formal source

  93content of the Hasse--Weil bound. -/
  94
  95/-- If the Hasse bound `a^2 ≤ 4q` holds, then `a / (2√q) ∈ [-1, 1]`. -/
  96theorem hasse_implies_arccos_valid
  97    (q : ℕ) (hq : 0 < q) (a : ℤ) (h_hasse : hasseBound q a) :
  98    ((a : ℝ) / (2 * Real.sqrt (q : ℝ))) ∈ Set.Icc (-1 : ℝ) 1 := by
  99  unfold hasseBound at h_hasse
 100  have hq_pos : (0 : ℝ) < (q : ℝ) := by exact_mod_cast hq
 101  have hsqrt_pos : 0 < Real.sqrt (q : ℝ) := Real.sqrt_pos.mpr hq_pos
 102  have h2sqrt_pos : 0 < 2 * Real.sqrt (q : ℝ) := by linarith
 103  have h_sqrt_sq : (Real.sqrt (q : ℝ)) ^ 2 = (q : ℝ) :=
 104    Real.sq_sqrt (le_of_lt hq_pos)
 105  -- |a|^2 = a^2 ≤ 4q = (2√q)^2, so |a| ≤ 2√q.
 106  have h_abs_sq : |(a : ℝ)| ^ 2 ≤ (2 * Real.sqrt (q : ℝ)) ^ 2 := by
 107    rw [_root_.sq_abs]
 108    have h_rhs : (2 * Real.sqrt (q : ℝ)) ^ 2 = 4 * (q : ℝ) := by
 109      rw [mul_pow, h_sqrt_sq]; ring
 110    rw [h_rhs]
 111    exact h_hasse
 112  -- Take square roots: |a| ≤ 2√q.
 113  have h_abs_a : |(a : ℝ)| ≤ 2 * Real.sqrt (q : ℝ) := by
 114    have h_abs_nonneg : 0 ≤ |(a : ℝ)| := abs_nonneg _
 115    have h_2sq_nonneg : 0 ≤ 2 * Real.sqrt (q : ℝ) := le_of_lt h2sqrt_pos
 116    nlinarith [h_abs_sq, sq_nonneg (|(a : ℝ)| + 2 * Real.sqrt (q : ℝ))]
 117  -- |a / (2√q)| ≤ 1.
 118  rw [Set.mem_Icc, ← abs_le]
 119  rw [abs_div, abs_of_pos h2sqrt_pos]
 120  exact (div_le_one h2sqrt_pos).mpr h_abs_a
 121
 122/-! ## The unconditional Hilbert--Pólya statement -/
 123
 124/-- **The Function-Field Hilbert--Pólya Theorem (Elliptic-Curve Case).**
 125
 126    For any elliptic curve `E / F_q` satisfying the Hasse--Weil bound