frobeniusAngle
plain-language theorem explainer
The definition supplies the Frobenius angle θ(q,a) for an elliptic curve over F_q with trace a as arccos(a/(2√q)). Researchers studying the function-field Riemann hypothesis cite it to build the 2x2 symmetric matrix whose eigenvalues recover the imaginary parts of the zeta zeros. It is a direct one-line transcription of the standard conversion from the Hasse-Weil bound into a real angle.
Claim. The Frobenius angle θ(q,a) of an elliptic curve over the finite field F_q with Frobenius trace a is given by θ(q,a) = arccos(a / (2 √q)).
background
In the function-field setting the zeta function of an elliptic curve E over F_q has exactly two non-trivial zeros whose imaginary parts are ±θ, where θ is the Frobenius angle. The Hasse-Weil bound guarantees |a| ≤ 2√q so that the argument of arccos lies in [-1,1]. This module constructs the Hilbert-Pólya operator T_E as the symmetric matrix with off-diagonals θ, whose eigenvalues are precisely ±θ. The local theoretical setting is the unconditional proof of the Riemann hypothesis for elliptic curves over finite fields, due to Hasse and Weil.
proof idea
The definition is a direct one-line wrapper that applies the real arccos function to the normalized Frobenius trace a/(2√q).
why it matters
This definition is the input to the Hilbert-Pólya operator hpOperator and to the main theorem hilbert_polya_elliptic_curve, which states that the eigenvalues of T_E are the imaginary parts of the non-trivial zeta zeros. It completes the explicit construction of a self-adjoint operator realizing the function-field Hilbert-Pólya conjecture for the elliptic case. The framework here provides an unconditional analogue of the integer Hilbert-Pólya program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.