theorem
proved
tactic proof
hasse_implies_arccos_valid
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
127 (which is unconditional, by Hasse 1934 / Weil 1948), the
128 `2 × 2` real symmetric matrix
129 `T_E = [[0, θ], [θ, 0]]`
130 is self-adjoint, and its eigenvalues `±θ` are real numbers equal to
131 the imaginary parts of the two non-trivial zeros of the zeta function
132 of `E`.
133
134 Unlike the integer case, this is unconditional: it is a theorem, not
135 a conjecture. The cost framework provides the operator construction;
136 Hasse's theorem provides the reality of `θ`. -/