hpOperator_eigenvector_neg
plain-language theorem explainer
The declaration establishes that the vector (1, -1) is an eigenvector of the 2 by 2 Hilbert-Pólya operator for an elliptic curve over F_q, with eigenvalue equal to the negative of the Frobenius angle θ. Number theorists verifying explicit matrix realizations of the function-field Riemann hypothesis would cite this when confirming the full spectrum of the operator. The verification follows from componentwise expansion of the matrix-vector product and algebraic simplification via the ring tactic.
Claim. Let $T$ be the $2×2$ real symmetric matrix $[[0, θ], [θ, 0]]$ where $θ = $ frobeniusAngle $q$ $a$ satisfies $cos θ = a/(2√q)$. Then $T · [1, -1]^T = -θ [1, -1]^T$.
background
The module constructs an explicit 2 by 2 self-adjoint operator whose eigenvalues are the imaginary parts of the non-trivial zeros of the zeta function of an elliptic curve over a finite field. The operator is defined as the matrix with zero diagonal and off-diagonal entries equal to the Frobenius angle θ, where cos θ = a/(2√q) and the Hasse-Weil bound guarantees θ is real. The local setting is the unconditional function-field Hilbert-Pólya statement for the elliptic case, with the spectrum {+θ, -θ} matching the two non-trivial zeros.
proof idea
The proof applies extensionality to the vector equality, then uses fin_cases on the index i. Each component is simplified by unfolding the matrix-vector multiplication and vector constructors, after which the ring tactic closes the resulting algebraic identities.
why it matters
This result is invoked by the parent theorem hilbert_polya_elliptic_curve, which asserts that the operator is symmetric and has eigenvalues ±θ equal to the imaginary parts of the zeta zeros. It completes the spectral verification for the negative eigenvalue in the module's explicit construction of the function-field Hilbert-Pólya operator. The construction sits inside the Recognition Science framework as an instance of spectral emergence realized by a finite-dimensional self-adjoint matrix controlled by the Hasse bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.