hilbert_polya_elliptic_curve

formal source

 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 `θ`. -/
 137theorem hilbert_polya_elliptic_curve
 138    (q : ℕ) (hq : 0 < q) (a : ℤ) (h_hasse : hasseBound q a) :
 139    -- The operator is symmetric (self-adjoint over ℝ).
 140    (hpOperator q a).IsSymm ∧
 141    -- It has eigenvalue +θ on (1, 1).
 142    (hpOperator q a).mulVec ![1, 1] = frobeniusAngle q a • ![1, 1] ∧
 143    -- It has eigenvalue -θ on (1, -1).
 144    (hpOperator q a).mulVec ![1, -1] = (-frobeniusAngle q a) • ![1, -1] ∧
 145    -- The angle θ corresponds to a real number (Hasse).
 146    ((a : ℝ) / (2 * Real.sqrt (q : ℝ))) ∈ Set.Icc (-1 : ℝ) 1 :=
 147  ⟨hpOperator_isSymm q a,
 148   hpOperator_eigenvector_pos q a,
 149   hpOperator_eigenvector_neg q a,
 150   hasse_implies_arccos_valid q hq a h_hasse⟩
 151
 152/-! ## Concrete example: y² = x³ + x + 1 over F_5
 153
 154For the elliptic curve `y² = x³ + x + 1` over `F_5`, the Frobenius trace
 155is `a = 2` (computable directly).  The Hasse bound: `a² = 4 ≤ 20 = 4·5`. -/
 156
 157/-- Concrete numerical check of the Hasse bound for our example. -/
 158example : hasseBound 5 2 := by
 159  unfold hasseBound
 160  norm_num
 161
 162/-- The Hilbert--Pólya operator for `E: y² = x³ + x + 1 / F_5` is the
 163    real symmetric `2 × 2` matrix `[[0, arccos(2/(2√5))], [arccos(2/(2√5)), 0]]`,
 164    with real eigenvalues `±arccos(1/√5)`. -/
 165example :
 166    let T := hpOperator 5 2
 167    T.IsSymm ∧ T.mulVec ![1, 1] = frobeniusAngle 5 2 • ![1, 1] := by