hasse_implies_arccos_valid
plain-language theorem explainer
The result shows that the Hasse bound a² ≤ 4q for an elliptic curve over F_q forces the normalized Frobenius trace a/(2√q) to lie in the closed interval [-1,1], making the angle θ real. Researchers constructing explicit self-adjoint operators for zeta zeros in the function-field setting would cite this lemma. The proof unfolds the bound, confirms positivity of √q, squares the inequality to bound |a|, and reduces the interval membership via absolute-value and division lemmas.
Claim. If the Hasse bound holds, that is if $a^2 ≤ 4q$ for positive integer $q$ and integer $a$, then $a/(2√q) ∈ [-1,1]$.
background
The module constructs an explicit 2×2 self-adjoint operator for the zeta function of an elliptic curve E over F_q. The predicate hasseBound q a encodes the arithmetic condition a² ≤ 4q, which is equivalent to the Hasse-Weil bound |a| ≤ 2√q. This bound guarantees that the Frobenius angle θ defined by cos θ = a/(2√q) is real, so that the matrix T_E = [[0, θ], [θ, 0]] has real eigenvalues ±θ matching the imaginary parts of the two non-trivial zeros of ζ_E. The local setting is the unconditional function-field Hilbert-Pólya theorem, contrasting with the open integer case. Upstream results supply the cost framework (J-cost from MultiplicativeRecognizerL4.cost and ObserverForcing.cost) that motivates the operator construction, although the present argument is purely real-analytic.
proof idea
The tactic proof unfolds hasseBound to obtain a² ≤ 4q. It establishes (q : ℝ) > 0 and √q > 0, then rewrites the bound as |a|² ≤ (2√q)². From this squared inequality it deduces |a| ≤ 2√q by nlinarith together with non-negativity facts. Finally it rewrites the target Set.Icc membership as |a/(2√q)| ≤ 1, using abs_div, abs_of_pos, and div_le_one.
why it matters
This lemma is the direct bridge that lets the downstream theorem hilbert_polya_elliptic_curve conclude that hpOperator q a is symmetric with real eigenvalues ±θ. It realizes the paper's unconditional function-field Hilbert-Pólya statement for elliptic curves (Hasse 1934 / Weil 1948), supplying the reality of θ that the cost-derived operator construction requires. In the Recognition Science framework it illustrates how the eight-tick octave and self-similar structures can be realized concretely in finite fields, while leaving the integer Riemann-hypothesis operator construction open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.