The Hasse Bound — Lean blueprint🔗

This is the blueprint for the Hasse-Weil formalisation of Hasse's theorem for an elliptic curve E over a finite field \mathbb{F}_q: the unconditional bound \bigl|\,\#E(\mathbb{F}_q) - (q + 1)\,\bigr| \;\le\; 2\sqrt{q} on the number of \mathbb{F}_q-rational points. Equivalently, writing t = q + 1 - \#E(\mathbb{F}_q) for the trace of Frobenius, it is the integer inequality t^2 \le 4q.

The argument is the classical one (Silverman V.1.1): the degree map on the endomorphism ring \operatorname{End}(E) is a positive-definite quadratic form, and applying it to r\pi - s (where \pi is the q-power Frobenius) forces the discriminant of a binary quadratic form to be non-positive — which is exactly t^2 \le 4q. The Lean development isolates a pure-arithmetic core (the binary-form discriminant bound and the passage to square roots) from the geometric input (the non-negativity of the degree form), discharges that geometric input two ways — through the dual isogeny and through the Weil pairing on \ell-torsion — and the capstone hasse_bound is unconditional and sorry-free.

Each node carries a (lean := …) reference to the actual declaration in the HasseWeil library, so Verso reads its completion status directly from Lean, and its prose cites the corresponding numbered result in Silverman, The Arithmetic of Elliptic Curves. The dependency graph at the foot of the page records the logical spine.