Abstract axiomatization of the inseparability predicate on a ring $R$ (intended to be the endomorphism ring of an elliptic curve), specifying the structural properties needed to prove Lemma 7.1. It posits a distinguished inseparable element $\pi$ (Frobenius) through which every inseparable endomorphism factors, closure under multiplication by $\pi$, and closure under negation.
- π : R
The distinguished inseparable element (Frobenius).
- π_insep : IsInsep self.π
The element $\pi$ is itself inseparable.
Every inseparable element factors as $\gamma \cdot \pi$ for some $\gamma$.
Any product $\gamma \cdot \pi$ is inseparable.
- neg_insep (α : R) : IsInsep α → IsInsep (-α)
The set of inseparable elements is closed under negation.
Instances For
Lemma 7.1 (additive complement of inseparables): if $\alpha$ is inseparable, then $\alpha + \beta$ is inseparable iff $\beta$ is. Both directions reduce to factoring through $\pi$.
Lemma 7.1 (contrapositive form): if $\alpha$ is inseparable, then $\alpha + \beta$ is separable iff $\beta$ is separable.
The predicate "$\varphi$ is an inseparable endomorphism" on the endomorphism ring of
an elliptic curve $E/F$, as a Prop-valued function on EllipticCurve.EndomorphismRing E.
Instances For
The endomorphism ring of an elliptic curve satisfies the abstract inseparability
axioms InsepAxioms, with the distinguished inseparable element being the Frobenius
endomorphism.
Instances For
Lemma 7.1 specialized to the endomorphism ring of an elliptic curve: if $\alpha$ is an inseparable endomorphism, then $\alpha + \beta$ is inseparable iff $\beta$ is.
An equivalence between the points of a Weierstrass curve and Option-of-nonsingular
affine pairs: the point at infinity corresponds to none and each affine point $(x, y)$
to some ⟨(x, y), h⟩.
Instances For
The point set $W(F)$ of a Weierstrass curve over a finite field is itself finite,
transported across pointEquiv from the (finite) type of optional nonsingular affine
pairs.
The number $\#E(\mathbb{F}_q)$ of $\mathbb{F}_q$-rational points (including the point at infinity) of a Weierstrass curve over a finite field.
Instances For
The trace of Frobenius $t = q + 1 - \#E(\mathbb{F}_q)$ for an elliptic curve $E$ over $\mathbb{F}_q$. By Hasse's theorem, $|t| \leq 2\sqrt{q}$.
Instances For
Rearrangement of the definition of the trace of Frobenius: $\#E(\mathbb{F}_q) = q + 1 - t$.
The degree of the endomorphism $r \cdot [F] - s \cdot \mathrm{id}$ (where $[F]$ is the Frobenius) equals the quadratic form $r^2 q - r s t + s^2$, and this degree is a natural number. This is the key positivity input for Hasse's bound.
The quadratic form $r^2 q - r s t + s^2$ is nonnegative for all integers $r, s$,
since it equals a degree of an isogeny by endomorphism_degree_eq_quadratic_form.
Substituting $(r, s) = (t, 2q)$ in degree_formula_nonneg yields the discriminant
bound $t^2 \leq 4 q$, which is the algebraic heart of Hasse's theorem.
The real quadratic $q x^2 - t x + 1$ is nonnegative for all $x \in \mathbb{R}$: a direct consequence of the discriminant bound $t^2 \leq 4 q$ via completing the square.
The Hasse bound on the square of the trace of Frobenius: $t^2 \leq 4 q$ for any elliptic curve over $\mathbb{F}_q$.
Hasse's bound (Theorem 7.3) on the absolute value of the trace of Frobenius: $|t| \leq 2\sqrt{q}$. Obtained by taking square roots in $t^2 \leq 4q$.
Theorem 7.3 (Hasse): for an elliptic curve $E/\mathbb{F}_q$, $|\#E(\mathbb{F}_q) - (q + 1)| \leq 2 \sqrt{q}$. Equivalently, the trace of Frobenius $t = q + 1 - \#E(\mathbb{F}_q)$ satisfies $|t| \leq 2\sqrt{q}$.
Reformulation of Hasse's bound as the two-sided interval enclosure $(\sqrt{q} - 1)^2 \leq \#E(\mathbb{F}_q) \leq (\sqrt{q} + 1)^2$, which is the form used in Mestre's argument.
Hasse's bound stated for an elliptic curve $W$ over $\mathbb{F}_q$: the hypothesis
0 < q is automatic since $\mathbb{F}_q$ is finite and nonempty.
The exponent of a group $G$: the least $n$ such that $g^n = 1$ for all $g \in G$ (equivalent to the LCM of orders of elements when $G$ is finite).
Instances For
The completely multiplicative monoid-with-zero homomorphism $\mathbb{N} \to \mathbb{R}$ sending $n \mapsto 1/n^2$ (and $0 \mapsto 0$). Used to express $\zeta(2)$ as the Euler product $\sum_n 1/n^2 = \prod_p (1 - p^{-2})^{-1}$.
Instances For
The value of oneOverSqHom at $n$ is $1/n^2$ (which is $0$ when $n = 0$).
Norm-summability of $\sum 1/n^2$: a prerequisite for invoking Mathlib's Euler product machinery for $\zeta(2)$.
Each Euler factor $(1 - p^{-2})^{-1}$ is at least $1$ since the geometric series expansion $\sum_k p^{-2k}$ starts with $1$.
Any finite partial product $\prod_{p \in s} (1 - p^{-2})^{-1}$ is bounded above by the full Euler product $\pi^2 / 6$, since the partial products are monotonically increasing toward the full product.
The number of "good" pairs $(g_1, g_2) \in G \times G$ such that $\mathrm{lcm}(\mathrm{ord}(g_1), \mathrm{ord}(g_2))$ equals the exponent of $G$. This counts pairs that together generate a cyclic subgroup of order equal to the exponent.
Instances For
For any group homomorphism $\varphi : G \to H$ and any two elements $\alpha, \beta \in G$, $\mathrm{lcm}(\mathrm{ord}(\varphi \alpha), \mathrm{ord}(\varphi \beta))$ divides $\mathrm{lcm}(\mathrm{ord}(\alpha), \mathrm{ord}(\beta))$, since each individual order of an image divides the corresponding source order.
Comparison lemma: the LCM-equals-exponent probability for the cyclic group $\mathbb{Z}/N$ (with $N = \mathrm{exp}(G)$) is at most the corresponding probability for $G$ itself. This reduces the lower bound for general groups to the cyclic case.
Exact formula for the cyclic case: the probability that two random elements of $\mathbb{Z}/n$ have orders whose LCM is $n$ equals $\prod_{p \mid n} (1 - p^{-2})$, a finite truncation of the Euler product for $1/\zeta(2) = 6/\pi^2$.
Combining prob_cyclic_le and prob_cyclic_eq_prod: for any nontrivial finite
abelian group $G$, the LCM-equals-exponent probability is bounded below by the
truncated Euler product over the prime factors of the exponent.
For any $n \geq 2$, the finite truncation $\prod_{p \mid n} (1 - p^{-2})$ strictly exceeds $6/\pi^2 = 1/\zeta(2)$. This uses the existence of some prime $q$ not dividing $n$ to produce a strict inequality when comparing the truncation to the full Euler product.
Any nontrivial group has exponent at least $2$ (since a nontrivial element has order $\geq 2$).
Theorem 7.6 for nontrivial groups: the probability that the LCM of the orders of
two random elements equals the exponent strictly exceeds $6/\pi^2$. Combines
prob_ge_euler_product with finite_euler_product_gt.
Theorem 7.6 (full statement): for any finite abelian group $G$, the probability that two random elements have orders with LCM equal to the group exponent strictly exceeds $6/\pi^2$. The trivial-group case is handled separately.
Iteratively divide $m$ by $p$ as long as the smaller multiple $m/p$ still annihilates the point $P$. This is the key subroutine in Algorithm 7.4 (order computation): given any annihilator $m$, it strips the prime $p$ to obtain a smaller annihilator.
Instances For
Algorithm 7.4: compute the order of a point $P$ in an additive group given a known
multiple $m$ and a list of primes containing all prime factors of the order. Strips each
prime in turn via stripPrimeFactor.
Instances For
Soundness of stripPrimeFactor: the stripped value remains an annihilator of $P$.
The result of stripPrimeFactor divides the original $m$, since each iterative
step replaces $m$ by a divisor $m/p$.
After stripping, the result is "prime-stripped": if $p$ still divides $\mathrm{strip}(m)$, then $\mathrm{strip}(m)/p$ no longer annihilates $P$ (otherwise we would have continued stripping).
Soundness of computeOrder: the output still annihilates $P$.
The result of computeOrder always divides the input multiple $m$.
Correctness lemma for computeOrder: if a prime $q$ divides the output, then
$\mathrm{output}/q$ does not annihilate $P$ (i.e. the output is the true order whenever
the prime list is complete). This is the inductive auxiliary used to prove that
computeOrder returns exactly $\mathrm{ord}(P)$.
Two Weierstrass curves $E'$ and $E$ over $F$ are twists of each other if there is a field extension $L/F$ over which they become isomorphic via a Weierstrass variable change.
Instances For
The quadratic twist of a short Weierstrass curve $W : y^2 = x^3 + a_4 x + a_6$ by $s \in F$: the curve $y^2 = x^3 + (s^2 a_4) x + (s^3 a_6)$.
Instances For
The coefficient $a_1$ of a quadratic twist is $0$.
The coefficient $a_2$ of a quadratic twist is $0$.
The coefficient $a_3$ of a quadratic twist is $0$.
The coefficient $a_4$ of a quadratic twist by $s$ is $s^2 \cdot W.a_4$.
The coefficient $a_6$ of a quadratic twist by $s$ is $s^3 \cdot W.a_6$.
The number of points on the quadratic twist of $W$ over $\mathbb{F}_q$, defined via the relation $\#E + \#E^{\mathrm{twist}} = 2q + 2$.
Instances For
The classical relation $\#E(\mathbb{F}_q) + \#E^{\mathrm{twist}}(\mathbb{F}_q) = 2q + 2$ between an elliptic curve and its quadratic twist.
The predicate "$N$ has a unique positive multiple in the closed interval $[\mathit{lo}, \mathit{hi}]$": there is exactly one positive integer $k$ such that $\mathit{lo} \leq k N \leq \mathit{hi}$. Mestre's theorem uses this to pin down the number of points from a known annihilator.
Instances For
Core algebraic inequality in Mestre's proof: given a bound $m^2 n^2 \leq 64 p$ and
suitable interval containment hypotheses, derive $16384 p^3 > (\sqrt{p} - 1)^8$. The
contradiction with inequality_fails_large_p produces the desired uniqueness for
large $p$.
The boundary range $17413 \leq p < 17424$ where inequality_large_case does not yet
apply: handled by the integer arithmetic lemma int_bound_small_range lifted to the
reals via $(\sqrt p - 1)^2 > p - 263$.
For all $p \geq 17413$, $(\sqrt{p} - 1)^8 \geq 16384 p^3$, combining the small range $17413 \leq p < 17424$ and the large range $p \geq 17424$. This rules out the "non-unique multiple" case for sufficiently large $p$ in Mestre's argument.
If $N$ has at least one positive multiple in the Hasse interval $[(\sqrt p - 1)^2, (\sqrt p + 1)^2]$ but the multiple is not unique, then $N < 4 \sqrt p$ (the width of the interval). The strict inequality uses the irrationality of $\sqrt{p}$ for primes $p$.
Bounded range case of Mestre's theorem ($229 < p < 17413$), to be discharged by a finite computer search. Asserts that under the bound $m^2 n^2 \leq 64 p$, one of the two annihilators $N_E, M_{E^t}$ has a unique multiple in the Hasse interval.
Combinatorial reformulation of Mestre's theorem (Theorem 7.7): under the constraint
$m^2 n^2 \leq 64 p$, at least one of the two annihilators $N_E, M_{E^t}$ has a unique
multiple in the Hasse interval. Splits into a small-$p$ case (handled by computer search)
and a large-$p$ case (handled by the inequality inequality_fails_large_p).
For an elliptic curve $E/\mathbb{F}_q$, there exists a positive integer $n$ dividing the exponent of $E(\mathbb{F}_q)$ such that $n \cdot \mathrm{exp}(E) = \#E(\mathbb{F}_q)$. This is the "smallest invariant factor" appearing in the elementary divisor decomposition $E(\mathbb{F}_q) \cong \mathbb{Z}/n \times \mathbb{Z}/\mathrm{exp}$.
Combined bound on the smallest invariant factors of a curve $E/\mathbb{F}_p$ and one of its quadratic twists $E^s$: the product $m^2 n^2$ of their squared smallest invariant factors is bounded by $64p$. This bound comes from analyzing the matrix of the Frobenius endomorphism on $E$ and $E^s$ and is the key ingredient in Mestre's theorem allowing one of $E, E^s$ to have a unique multiple in the Hasse interval.
Mestre's theorem (Theorem 7.7): for an elliptic curve $E/\mathbb{F}_p$ with $p > 229$ prime, at least one of $E$ or any quadratic twist $E^s$ has the property that its group exponent has a unique multiple in the Hasse interval $[(\sqrt p - 1)^2, (\sqrt p + 1)^2]$. This is the key fact enabling efficient point counting: it ensures that computing the exponent of $E(\mathbb{F}_p)$ or $E^s(\mathbb{F}_p)$ determines the group order uniquely.