hasseBound
plain-language theorem explainer
The declaration defines the Hasse-Weil bound as the proposition a squared at most 4q for natural q and integer a. Researchers on function-field analogs of the Riemann hypothesis cite it to guarantee that the Frobenius angle remains real. The definition is a direct embedding of the classical inequality into the reals with no auxiliary lemmas.
Claim. For natural number $q$ and integer $a$, the Hasse-Weil bound holds when $a^2 ≤ 4q$.
background
The module constructs an explicit 2×2 real symmetric operator whose eigenvalues recover the imaginary parts of the non-trivial zeros of the zeta function of an elliptic curve E over the finite field F_q. The Frobenius trace a and field cardinality q enter the definition of the angle θ via cos θ = a/(2√q). The bound ensures θ is real so that the operator T_E = [[0, θ], [θ, 0]] is well-defined over the reals. Upstream results on spectral emergence supply the edge-counting conventions used to embed this construction into the Recognition Science forcing chain.
proof idea
The definition is a one-line abbrev that directly states the inequality ((a : ℝ)^2) ≤ 4 * (q : ℝ) as a Prop. No tactics or lemmas are invoked; the body is the classical Hasse-Weil statement cast into Lean reals.
why it matters
This definition supplies the hypothesis for hasse_implies_arccos_valid and hilbert_polya_elliptic_curve. The latter proves that the operator is self-adjoint with eigenvalues exactly ±θ, realizing an unconditional function-field Hilbert-Pólya statement (Hasse 1934, Weil 1948). It closes the step from the bound to an explicit matrix whose spectrum matches the zeta zeros, contrasting with the open integer case. The construction sits inside the spectral-emergence layer of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.