The group of $\mathbb{Q}_p$-points of a Weierstrass curve $W$ defined over $\mathbb{Q}$, obtained by base-changing to $\mathbb{Q}_p$ and taking the affine point set.
Instances For
Membership predicate for the $n$-th piece $E_n(\mathbb{Q}_p)$ of the $p$-adic filtration: a point is either the identity, or has $y \ne 0$ and $v_p(x) - v_p(y) \ge n$.
Instances For
The $p$-adic filtration is monotone in the level: $E_{n+1}(\mathbb{Q}_p) \subseteq E_n(\mathbb{Q}_p)$.
Negation preserves the $p$-adic filtration: if $P \in E_n(\mathbb{Q}_p)$ then so is $-P$. This uses that negation only flips the sign of $y$ in short form, and $v_p$ is sign-invariant.
Secant case: when $x_1 \ne x_2$, adding two points $P, Q \in E_n(\mathbb{Q}_p)$ stays in $E_n(\mathbb{Q}_p)$. Axiomatized for now.
Tangent case: when $x_1 = x_2$ but $y_1 \ne -y_2$, doubling-type addition still preserves $E_n(\mathbb{Q}_p)$. Axiomatized for now.
Combined statement (secant + tangent): the explicit addition formula on the Weierstrass curve preserves the $p$-adic filtration; established by case analysis on whether $x_1 = x_2$.
Re-statement using let for readability: the addition formula preserves the $p$-adic
filtration.
Closure under addition: if $P, Q \in E_n(\mathbb{Q}_p)$ then $P + Q \in E_n(\mathbb{Q}_p)$. This combines the trivial cases (one summand is $0$ or $P + Q = 0$) with the addition formula.
The $n$-th piece $E_n(\mathbb{Q}_p)$ of the $p$-adic filtration on $E(\mathbb{Q}_p)$ realized
as an additive subgroup, with closure properties supplied by negation_preserves_filtration and
addition_preserves_filtration.
Instances For
The $p$-adic filtration, viewed as a function $\mathbb{N} \to \mathrm{AddSubgroup}\,E$, is antitone.
If $H$ is the kernel of a surjective additive group homomorphism $G \to \mathbb{Z}/p\mathbb{Z}$, then $[G : H] = p$.
Axiomatized reduction homomorphism $E_n(\mathbb{Q}_p) \to \mathbb{Z}/p\mathbb{Z}$ used to detect the next layer of the filtration.
Instances For
Axiomatized: the reduction homomorphism reduction_hom_ax is surjective.
Axiomatized: the kernel of reduction_hom_ax is exactly $E_{n+1}(\mathbb{Q}_p)$ viewed as a
subgroup of $E_n(\mathbb{Q}_p)$.
Bundled form: there exists a surjective additive homomorphism $E_n(\mathbb{Q}_p) \to \mathbb{Z}/p\mathbb{Z}$ whose kernel is $E_{n+1}(\mathbb{Q}_p)$.
Lemma 24.12: for $n \ge 1$, the relative index $[E_n(\mathbb{Q}_p) : E_{n+1}(\mathbb{Q}_p)]$ equals $p$. Each successive layer of the $p$-adic filtration is a quotient of order $p$.
The descending chain $E_0(\mathbb{Q}_p) \supseteq E_1(\mathbb{Q}_p) \supseteq \cdots$ as a function $\mathbb{N} \to \mathrm{AddSubgroup}$.
Instances For
The kernel of reduction modulo $p$ on $E(\mathbb{Q}_p)$, equal to $E_1(\mathbb{Q}_p)$, the first non-trivial layer of the $p$-adic filtration.
Instances For
A point that lies in every filtration piece $E_n(\mathbb{Q}_p)$ is the identity: the only element with infinite valuation difference is $0$.
Axiomatized: if $P \in E_n(\mathbb{Q}_p)$ and $pP = 0$, then $P$ already lies in $E_{n+1}(\mathbb{Q}_p)$.
Any torsion point of $E(\mathbb{Q}_p)$ lying in $E_1(\mathbb{Q}_p)$ must be zero. The proof
proceeds by strong induction on the torsion order, distinguishing the cases of coprime-to-$p$
torsion (annihilated by the surjective reduction) and $p$-power torsion (pushed deeper into the
filtration via p_nsmul_in_filtration_succ_ax).
Corollary 24.18 (kernel-of-reduction form): the additive subgroup $E_1(\mathbb{Q}_p)$ has no
nontrivial torsion. Proved from torsion_in_E1_eq_zero by reducing equalities of subgroup
elements to differences.
Corollary 24.18: the kernel of reduction $E_1(\mathbb{Q}_p)$ is torsion-free, the user-facing
restatement of cor_24_18_torsion_free_ax.