hilbert_polya_elliptic_curve
plain-language theorem explainer
The theorem shows that for any elliptic curve over F_q with Frobenius trace a obeying the Hasse bound, the 2x2 operator T_E with off-diagonal entries equal to the real angle theta = arccos(a/(2 sqrt q)) is symmetric and has eigenvalues plus or minus theta on the vectors (1,1) and (1,-1). Number theorists studying function-field analogues of the Riemann hypothesis cite this result because it supplies an explicit self-adjoint operator whose spectrum matches the imaginary parts of the nontrivial zeta zeros. The proof is a direct conjunction of the
Claim. Let $E$ be an elliptic curve over the finite field $F_q$ with Frobenius trace $a$ satisfying the Hasse-Weil bound $|a|leq 2sqrt q$. Let $theta = arccos(a/(2sqrt q))$. Then the $2times 2$ real matrix $T_E = begin{pmatrix} 0 & theta theta & 0 end{pmatrix}$ is self-adjoint, satisfies $T_E begin{pmatrix} 1 1 end{pmatrix} = theta begin{pmatrix} 1 1 end{pmatrix}$ and $T_E begin{pmatrix} 1 -1 end{pmatrix} = -theta begin{pmatrix} 1 -1 end{pmatrix}$, and $theta$ is real.
background
The module builds an explicit finite-dimensional self-adjoint operator whose eigenvalues are the imaginary parts of the nontrivial zeros of the zeta function of an elliptic curve over a finite field. For $E/F_q$ with trace $a$, the Hasse-Weil bound forces the Frobenius angle $theta = arccos(a/(2sqrt q))$ to lie in $[-pi/2,pi/2]$, so the operator is the symmetric matrix with off-diagonals $theta$. This construction is unconditional by Hasse's 1934 theorem, in contrast to the integer Hilbert-Polya conjecture. The local setting is the function-field case of the Riemann hypothesis, which Weil proved in 1948; the cost framework supplies the operator definition while the Hasse bound supplies reality of $theta$.
proof idea
The proof is a one-line wrapper that applies four sibling lemmas: hpOperator_isSymm for self-adjointness, hpOperator_eigenvector_pos and hpOperator_eigenvector_neg for the two eigenvector equations, and hasse_implies_arccos_valid for the interval membership of the scaled trace.
why it matters
This supplies the unconditional function-field Hilbert-Polya statement for elliptic curves, confirming that the constructed operator has spectrum matching the imaginary parts of the zeta zeros. It rests on Hasse 1934 and Weil 1948 and sits inside the Recognition Science number-theory development as a concrete operator realization parallel to the forcing chain. No downstream uses are recorded yet; the result closes the elliptic-curve case but leaves the integer conjecture and higher-genus curves open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.