hpOperator_eigenvector_pos
plain-language theorem explainer
The declaration shows that the vector (1, 1) is an eigenvector of the 2 by 2 Hilbert-Pólya operator T_E with eigenvalue equal to the Frobenius angle θ. Number theorists working on function-field analogues of the Hilbert-Pólya conjecture cite this when confirming the spectral properties of the explicit matrix built from the Hasse-Weil data. The proof is a direct term-mode verification that applies matrix multiplication rules followed by algebraic simplification.
Claim. Let $q$ be a natural number and $a$ an integer. Let $T_E$ be the $2×2$ matrix $[[0, θ], [θ, 0]]$ where $θ = arccos(a/(2√q))$ is the Frobenius angle. Then $T_E [1, 1]^T = θ [1, 1]^T$.
background
In the function-field Hilbert-Pólya setting the operator for an elliptic curve E over F_q with Frobenius trace a is the real symmetric matrix T_E = [[0, θ], [θ, 0]], where θ is defined by cos θ = a/(2√q) (real by the Hasse-Weil bound |a| ≤ 2√q). The eigenvalues ±θ are precisely the imaginary parts of the two non-trivial zeros of the zeta function of E. The module constructs this finite-dimensional self-adjoint operator unconditionally, in contrast to the open integer case.
proof idea
The proof applies vector extensionality, then case analysis on the two finite indices. For each component it expands the matrix-vector product using the explicit definition of hpOperator, substitutes the definition of frobeniusAngle, and closes the equality by ring simplification on the resulting scalar expressions.
why it matters
This lemma supplies one of the two eigenvector statements required by the parent theorem hilbert_polya_elliptic_curve, which asserts that T_E is self-adjoint and that its eigenvalues match the imaginary parts of the zeta zeros. It completes the explicit spectral verification for the elliptic-curve case of the function-field Hilbert-Pólya theorem (Hasse 1934, Weil 1948). Within the Recognition Science framework the construction supplies a concrete finite-dimensional operator whose spectrum is forced by the same self-similar and octave structures that appear in the T0-T8 chain, though the present file remains a number-theoretic verification rather than a direct derivation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.