4 Kernel lemmas
The lemmas of this chapter are proved in Lean. Some are pure algebra with no classical input behind them; those are dark green in the graph. The others consume classical inputs and are light green.
Let \(R\) be a commutative ring in which \(2x = 0\) implies \(x = 0\), let \(f, U \in R[[T]]\) with \(f(0) = 0\) and \(U(0) = 1\), and suppose \(f\bigl((1+T)^{-1} - 1\bigr) = U\, f\). Then the coefficient of \(T\) in \(f\) is \(0\).
Comparing coefficients of \(T\) on both sides gives \(-c_1 = c_1\), so \(2c_1 = 0\). coeff_one_Lp_eq_zero is the specialisation to \(R = \mathbb {Z}_p\).
Assume \(L(E,1) = 0\) and \(w(E) = +1\). Then for every good ordinary prime \(p\), writing \(L_p(E,T) = c_0(p) + c_1(p)\, T + c_2(p)\, T^2 + \cdots \),
This is Lemma 3.1 of the paper.
\(c_0(p) = 0\) (c0_eq_zero): the interpolation formula with \(L(E,1)/\Omega _E = 0\) gives \(c_0(p) = 0\) in \(\mathbb {Q}_p\), hence in \(\mathbb {Z}_p\). \(c_1(p) = 0\) (c1_eq_zero): the functional equation and \(c_0(p) = 0\) put \(L_p\) under Lemma 19.
Let \(E/\mathbb {Q}\) have complex multiplication by \(\mathbb {Z}[i]\) and let \(p \equiv 1 \pmod4\) be a prime of good reduction. Then \(a_p\) is even, and \(p\) is anomalous for \(E\) if and only if \(p = 5\) and \(a_5 = -4\). This is Lemma 2.2 of the paper, for split \(p\).
anomalous_iff_five: over \(p \equiv 1 \pmod4\), \(2 \mid a\) and \(a^2 \le 4p\), \((a : \mathbb {Z}/p) = 1\) if and only if \(p = 5\) and \(a = -4\). eq_five_or_thirteen_le splits into \(p = 5\) and \(p \ge 13\); for \(p \ge 13\) the Hasse bound excludes \(a \equiv 1\), and at \(p = 5\) the congruence, the bound and evenness leave \(a = -4\). Evenness is two_dvd_ap, from \(a_p = 2\, \mathrm{Re}(\pi )\). noAnomalous is the form the normalisation consumes: for split \(p\) with \(a_5 \ne -4\) when \(p = 5\), \(1 - \alpha _p^{-1}\) is a \(p\)-adic unit. The part of the paper’s lemma for \(p \not\equiv 1 \pmod4\) is not formalised; no theorem uses it.
Let \(p = {\mathfrak {p}}\bar{\mathfrak {p}}\) be a split prime of good reduction with \(p \nmid \prod _v c_v \cdot \# E(\mathbb {Q})_{\mathrm{tors}}\), not anomalous. Then \(\tilde c_2(p) \in \mathbb {Z}_p^\times \) if and only if \(c_2(p) \in \mathbb {Z}_p^\times \). This is Proposition 3.3 of the paper.
isPUnit_c2tilde_iff proves the equivalence from two hypotheses: \(1 - \alpha _p^{-1}\) is a \(p\)-adic unit, and \((\# \mathrm{tors})^2/\prod _v c_v = 1\). Theorem A discharges the first through ClassicalInputs.isPUnit_one_sub_alphaInv, from the field notAnomalous, and the second from torsSqOverTam_eq. isPUnit_c2tilde_iff_of_split discharges the first instead from Lemma 21; it is kept because it bounds what notAnomalous assumes.
Let \(f \in \Lambda \) with \(c_0(f) = c_1(f) = 0\) and \(c_2(f) \in \mathbb {Z}_p^\times \). Then \(f = T^2 u\) for a unit \(u \in \Lambda ^\times \); hence \(\mu (f) = 0\), \(\lambda (f) = 2\), and \(f\) and \(T^2\) generate the same ideal.
tsq_factor produces \(u\); the three consequences are read off from the factorisation.
Let \(X\) be a finitely generated \(\Lambda \)-module with no nonzero finite submodule, and suppose there is a \(\Lambda \)-linear map \(X \to \prod _i \Lambda /(f_i)\) with finite kernel and cokernel such that \(\prod _i f_i\) and \(T^2\) generate the same ideal. If \(\dim _{\mathbb {Q}_p}(X/TX) \otimes \mathbb {Q}_p \ge 2\), then \(TX = 0\) and \(X \cong \mathbb {Z}_p^2\).
selmer_dual_structure is the statement. The pseudo-isomorphism and the characteristic ideal \((T^2)\) bound the \(\mathbb {Z}_p\)-rank of \(X/TX\) by \(2\); with the lower bound, \(X/TX\) is free of rank \(2\), and the absence of finite submodules forces \(TX = 0\). rank_lower_bound supplies the lower bound from a surjection onto \(\mathbb {Z}_p^2\), and quotient_collapse identifies \(X/TX\) with \(X\) once \(TX = 0\). This is the algebraic core of Theorem A, Steps 2 and 3 of the paper.
Let \(0 \to A \xrightarrow {\iota } S \xrightarrow {\pi } \mathbb {Z}_p^2 \to 0\) be an exact sequence of finitely generated \(\mathbb {Z}_p\)-modules with \(S \cong \mathbb {Z}_p^2\). Then \(A = 0\) and \(\mathrm{rank}_{\mathbb {Z}_p} S = 2\).
\(\pi \) is a surjective endomorphism of a finitely generated module over a commutative ring, up to the identification \(S \cong \mathbb {Z}_p^2\), hence injective; so \(\ker \pi = \iota (A) = 0\). This is Step 5 of the paper.
Let \(R\) be a commutative ring and \(A, B \in R[[T]]\) with \(c_0(B) = c_1(B) = 0\). Then \(c_2(AB) = A(0)\, c_2(B)\).
For \(p \notin S_E\) split, \(c_2(p)\) is a \(p\)-adic unit if and only if \(c_2(L^{\mathrm{K}})\) is.
This is Lemma 6.3 of the paper.
Part (1) is Decoupling.coeff_two_mul: \(c_2(AB) = c_0(A)c_2(B) + c_1(A)c_1(B) + c_2(A)c_0(B)\) and the last two terms vanish. Part (2) is Decoupling.isUnit_coeff_two_of_comparison: part (1) along a local ring homomorphism moves the unit property across the comparison of Classical input 16. No derivative of the comparison factor or of the Euler factor reaches the second coefficient.
Let \(W\) be a local integral domain with maximal ideal \((\varpi )\), let \(\kappa _0 \in W^\times \), and let \(c, m \in W\) with \(\varpi ^2(\kappa _0 c - m) \in (\varpi ^3)\). Then \(c\) is a unit if and only if the residue of \(m\) is nonzero. Applied to the grading congruence: \(v_p(c_2(L^{\mathrm{K}})) = 0\) if and only if the criterion class \(\mathfrak {c}({\mathfrak {p}}) := p^{-2}M_2({\mathfrak {p}}) \bmod \mathfrak {m}_W\) is nonzero. This is Proposition 6.2(2) of the paper.
The Lean lemma is the abstract statement about \(W\), with no interface dependence; it is instantiated at \(\varpi = p\) over the Katz coefficient ring.