%% Generated from draft.md. Typeset with: latexmk -pdf paper.tex %% Needs: amsmath amsthm amssymb hyperref longtable array booktabs-free %% (see README-for-Rin.md). The author line is provisional. \documentclass[11pt,a4paper]{article} \IfFileExists{lmodern.sty}{\usepackage{lmodern}}{} %% scalable T1 fonts \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage[margin=28mm]{geometry} \usepackage{amsmath,amsthm,amssymb} \usepackage{array,longtable} \usepackage{enumitem} \usepackage[hidelinks]{hyperref} \usepackage[english]{babel} %% ---- symbols used by the unicode declarations below ---------------------- \newcommand{\txtsym}[1]{\ifmmode\text{#1}\else#1\fi} %% Tate--Shafarevich symbol: the cyrillic font if the distribution has it, %% otherwise the roman abbreviation. Nothing else depends on this package. \IfFileExists{cyrillic.sty}{% \usepackage{cyrillic}% \providecommand{\Sha}{\text{\usefont{OT2}{wncyr}{m}{n}Sh}}}{% \providecommand{\Sha}{\mathrm{Sha}}} %% every non-ASCII character of the source, declared once: \DeclareUnicodeCharacter{00A7}{\txtsym{\S}} \DeclareUnicodeCharacter{00B0}{\ensuremath{^\circ}} \DeclareUnicodeCharacter{00B1}{\ensuremath{\pm}} \DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}} \DeclareUnicodeCharacter{00B3}{\ensuremath{{}^3}} \DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}} \DeclareUnicodeCharacter{00B9}{\ensuremath{{}^1}} \DeclareUnicodeCharacter{00C1}{\txtsym{\'A}} \DeclareUnicodeCharacter{00CA}{\txtsym{\^E}} \DeclareUnicodeCharacter{00D7}{\ensuremath{\times}} \DeclareUnicodeCharacter{00E4}{\txtsym{\"a}} \DeclareUnicodeCharacter{00E9}{\txtsym{\'e}} \DeclareUnicodeCharacter{00EA}{\txtsym{\^e}} \DeclareUnicodeCharacter{00FC}{\txtsym{\"u}} \DeclareUnicodeCharacter{0112}{\txtsym{\=E}} \DeclareUnicodeCharacter{0169}{\ensuremath{\tilde{u}}} \DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} \DeclareUnicodeCharacter{039B}{\ensuremath{\Lambda}} \DeclareUnicodeCharacter{03A3}{\ensuremath{\Sigma}} \DeclareUnicodeCharacter{03A6}{\ensuremath{\Phi}} \DeclareUnicodeCharacter{03A8}{\ensuremath{\Psi}} \DeclareUnicodeCharacter{03A9}{\ensuremath{\Omega}} \DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{03B2}{\ensuremath{\beta}} \DeclareUnicodeCharacter{03B4}{\ensuremath{\delta}} \DeclareUnicodeCharacter{03B7}{\ensuremath{\eta}} \DeclareUnicodeCharacter{03B9}{\ensuremath{\iota}} \DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} \DeclareUnicodeCharacter{03BC}{\ensuremath{\mu}} \DeclareUnicodeCharacter{03BE}{\ensuremath{\xi}} \DeclareUnicodeCharacter{03C0}{\ensuremath{\pi}} \DeclareUnicodeCharacter{03C1}{\ensuremath{\rho}} \DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} \DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} \DeclareUnicodeCharacter{03C6}{\ensuremath{\varphi}} \DeclareUnicodeCharacter{03C8}{\ensuremath{\psi}} \DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}} \DeclareUnicodeCharacter{03D5}{\ensuremath{\phi}} \DeclareUnicodeCharacter{03F1}{\ensuremath{\varrho}} \DeclareUnicodeCharacter{0428}{\ensuremath{\Sha}} \DeclareUnicodeCharacter{2013}{\txtsym{\textendash}} \DeclareUnicodeCharacter{2014}{\txtsym{\textemdash}} \DeclareUnicodeCharacter{2026}{\ensuremath{\dots}} \DeclareUnicodeCharacter{2032}{\ensuremath{{}^{\prime}}} \DeclareUnicodeCharacter{2033}{\ensuremath{{}^{\prime\prime}}} \DeclareUnicodeCharacter{2074}{\ensuremath{{}^4}} \DeclareUnicodeCharacter{2076}{\ensuremath{{}^6}} \DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}} \DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}} \DeclareUnicodeCharacter{2083}{\ensuremath{{}_3}} \DeclareUnicodeCharacter{2084}{\ensuremath{{}_4}} \DeclareUnicodeCharacter{2085}{\ensuremath{{}_5}} \DeclareUnicodeCharacter{2086}{\ensuremath{{}_6}} \DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} \DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}} \DeclareUnicodeCharacter{2192}{\ensuremath{\to}} \DeclareUnicodeCharacter{21A6}{\ensuremath{\mapsto}} \DeclareUnicodeCharacter{2202}{\ensuremath{\partial}} \DeclareUnicodeCharacter{2208}{\ensuremath{\in}} \DeclareUnicodeCharacter{2209}{\ensuremath{\notin}} \DeclareUnicodeCharacter{220E}{\ensuremath{\blacksquare}} \DeclareUnicodeCharacter{220F}{\ensuremath{\prod}} \DeclareUnicodeCharacter{2212}{\ensuremath{-}} \DeclareUnicodeCharacter{2216}{\ensuremath{\setminus}} \DeclareUnicodeCharacter{2217}{\ensuremath{\ast}} \DeclareUnicodeCharacter{2218}{\ensuremath{\circ}} \DeclareUnicodeCharacter{2223}{\ensuremath{\mid}} \DeclareUnicodeCharacter{2224}{\ensuremath{\nmid}} \DeclareUnicodeCharacter{2229}{\ensuremath{\cap}} \DeclareUnicodeCharacter{2245}{\ensuremath{\cong}} \DeclareUnicodeCharacter{2248}{\ensuremath{\approx}} \DeclareUnicodeCharacter{2260}{\ensuremath{\neq}} \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} \DeclareUnicodeCharacter{2264}{\ensuremath{\le}} \DeclareUnicodeCharacter{2265}{\ensuremath{\ge}} \DeclareUnicodeCharacter{2282}{\ensuremath{\subset}} \DeclareUnicodeCharacter{2297}{\ensuremath{\otimes}} \DeclareUnicodeCharacter{22EF}{\ensuremath{\cdots}} \DeclareUnicodeCharacter{2605}{\ensuremath{\star}} \DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}} \DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}} \DeclareUnicodeCharacter{27F8}{\ensuremath{\Longleftarrow}} \DeclareUnicodeCharacter{27F9}{\ensuremath{\Longrightarrow}} \DeclareUnicodeCharacter{27FA}{\ensuremath{\Longleftrightarrow}} %% ---- named theorem environments (the labels are those of the draft) ------ \newtheoremstyle{named}{\topsep}{\topsep}{\itshape}{0pt}{\bfseries}{.}{ }{\thmnote{#3}} \theoremstyle{named} \newtheorem*{namedthm}{} \newenvironment{mdproof}[1][Proof]{\par\medskip\noindent\textit{#1.}\ }{\par\medskip} \newlist{leancode}{itemize}{1} \setlist[leancode]{label={},leftmargin=1.2em,topsep=.5em,itemsep=.15em,parsep=0pt} \setlength{\parskip}{.35em} \sloppy \hbadness=10000 \begin{document} \title{Integrality of the p-adic height pairing at an anomalous prime is equivalent to a point of order p in $E(Q_p)$\\[.5em]\large Splitting of the reduction sequence, the vanishing of a Fermat quotient of the p-th division polynomial, and p-integrality of the height matrix on E(Q)/tors are one and the same condition; in rank one $v_p(Reg_p)$ ≥ 0 ⟺ split, the non-split value being −1 exactly against the elementary baseline r − 2} \author{Kiichi \and Shiori \and Rin} \date{Draft, 2026-09-24. Not submitted. See §8 for what is not claimed and §6 for the boundary between the machine-checked part and the paper part.} \maketitle \begin{center}\small wvbks0 [at] gmail.com · \url{https://computoergosum.com/en/index.html}\end{center} \section*{Abstract} Let E/Q be an elliptic curve, p ≥ 5 a prime of good ordinary reduction, r the rank of E(Q), and $Reg_p$ the cyclotomic p-adic regulator in the normalisation of [MST] used by [Har], $h_p(P)$ = 2 $log_p(σ_p(P)/d(P))$ with $σ_p$ the Mazur–Tate sigma function. Call p \textit{anomalous} when p ∣ $\#E(F_p)$ $(a_p$ = 1, that is $\#E(F_p)$ = p, for p ≥ 7) and E \textit{split at p} when $E(Q_p)[p]$ ≠ 0. At an anomalous prime $Reg_p$ need not be p-integral: counting indices gives $v_p(Reg_p)$ ≥ r − 2 when p ∤ $∏_{ℓ}$ $c_{ℓ}$ and ≥ r otherwise (Theorem A). That baseline is elementary and it is not ours — the one negative entry of the table of [MST, §4.2], the precision loss 2 $v_p(n)$ of [Har], a hypothesis of [Ban]. What this note contributes is a local mechanism that governs the deficit, in both directions: \begin{quote} \textbf{Integrality theorem for the p-adic regulator at split anomalous primes.} Suppose $\#E(F_p)$ = p, p ∤ $∏_{ℓ}$ $c_{ℓ}$, and that Λ := E(Q)/tors surjects onto $E(F_p)$. Then \textbf{every entry of the height matrix $M_{Λ}$ on a basis of Λ lies in $Z_p$ if and only if $E(Q_p)[p]$ ≠ 0}; in rank one, $v_p(Reg_p)$ ≥ 0 ⟺ $E(Q_p)[p]$ ≠ 0, the non-split value being \textbf{−1 exactly}; and in the split case $v_p(Reg_p)$ ≥ max(r − 2, 0) in every rank. \end{quote} Three things are separated throughout. The \textbf{baseline} r − 2 is a known phenomenon. The equivalence for the \textbf{matrix} is the content of the note, and it holds in every rank. The bound on the \textbf{determinant} improves on the baseline in rank one only, since max(r−2, 0) = r−2 for r ≥ 2. The proof is local and runs through one element λ ∈ $F_p$, the Fermat quotient $q_p(φ_p(x₀))/2$ of the p-th division polynomial at a lift of a nonzero class of $E(F_p)$. With P = (α/d², β/d³) in lowest terms the height splits into a formal part of valuation b and 2 $log_p(α/β)$ of valuation c ≥ 1 (Lemma 3); in a model with p ∣ a₁ — always available, since p is odd — one has b ≥ 2 and $q_p(α/β)$ = −λ (Theorem B), so the height is integral exactly when λ vanishes. Vélu's factorisation of multiplication by p kills λ in the split case (Theorem C, Corollary D); conversely λ = 0 forces splitting, a known criterion (Proposition 6, [LR, Thm 4.1], [DW, Lemma 3.2]) proved here through the Euler identity for the weighted-homogeneous division polynomial and a residue computation at the cusp. CM curves split at every anomalous prime of good reduction (Theorem F). The arithmetic steps are theorems of Lean 4 with Mathlib (no \texttt{sorry}, no \texttt{native\_\allowbreak{}decide}, axioms [propext, Classical.choice, Quot.sound]), the geometric inputs entering as hypotheses. Nothing here bears on the conjecture of Birch and Swinnerton-Dyer. \textbf{Keywords.} p-adic height, p-adic regulator, anomalous prime, local torsion, division polynomial, Fermat quotient, Vélu isogeny, Tate curve, Lean 4. \textbf{MSC 2020.} 11G50, 11G07, 11S31, 11Y40, 68V20. \section*{1. Introduction} The cyclotomic p-adic height pairing of Mazur–Tate and Schneider attaches to E/Q and a prime p of good ordinary reduction a symmetric bilinear form on E(Q) ⊗ $Q_p$, whose determinant $Reg_p$ on a basis of Λ := E(Q)/tors is the regulator in the p-adic analogue of the conjecture of Birch and Swinnerton-Dyer [MST] [BMS]. Unlike the archimedean regulator it is not known to be non-zero (Schneider's conjecture [SW, Conj. 4.1]), and nothing here bears on that. This note concerns a coarser invariant, the valuation of $Reg_p$. At an \textit{anomalous} prime — p ∣ $\#E(F_p)$, which for p ≥ 7 means $a_p$ = 1, the notion of [Maz72] — it can be negative, because the points reducing to O at p form a subgroup of index divisible by p and dividing the determinant by the square of that index costs 2. This is the baseline $v_p(Reg_p)$ ≥ r − 2 of Theorem A; it is known (§9), and it is attained. What this note proves is that the deficit is present exactly when the reduction sequence 0 → $E_1(Q_p)$ → $E(Q_p)$ → $E(F_p)$ → 0 fails to split, that is exactly when $E(Q_p)$ contains no point of order p. Splitting makes the height of every point of Λ p-integral — a statement about the pairing, which the baseline gives in no rank — and its failure puts the valuation −1 into the matrix, in every rank, and into the determinant in rank one. The obstruction sits in the second p-adic digit of the height, where it is a Fermat quotient, and the route runs: decomposition of the height (Lemma 3), a criterion expressing that digit through one element λ ∈ $F_p$ (Theorem B), the vanishing of λ in the split case by Vélu's factorisation of multiplication by p (Theorem C, Corollary D), and its non-vanishing in the non-split case (Proposition 6), which is a known criterion for local torsion. The materials are classical and we do not call the lemmas new; what we did not find in the sources we read is the equivalence itself, and the presentation of the local criterion through a Fermat quotient. §9 records where we looked, §6 draws the boundary between what a kernel has checked and what it has not, §7 lists what is open and §8 what is not claimed. \section*{2. Setting and normalisation} \textbf{The curve.} E/Q is given by a global minimal Weierstrass equation with coefficients a₁, …, a₆, and p ≥ 5 is a prime of good ordinary reduction; Λ := E(Q)/tors has rank r, and $c_{ℓ}$ is the Tamagawa number at ℓ. Write t = −x/y for the parameter of the formal group Ê, $E_n(Q_p)$ := \{P : $v_p(t(P))$ ≥ n\}, and for P ∈ E(Q) \begin{quote} P = (α(P)/d(P)², β(P)/d(P)³), gcd(α, d) = gcd(β, d) = 1, d ≥ 1. \end{quote} $v_p$ is normalised by $v_p(p)$ = 1, $log_p$ is the Iwasawa logarithm with $log_p(p)$ = 0, and for a p-adic unit u, $q_p(u)$ := $(u^{p−1}$ − 1)/p mod p is the Fermat quotient. Then $q_p$ : $Z_p^{×}$ → $F_p$ is a surjective homomorphism and $v_p(log_p$ u) = 1 + $v_p(q_p(u))$, so "the second p-adic digit of $log_p$ u" and "the Fermat quotient of u" are the same datum. \textbf{The height.} The height is taken in the explicit form of [Har, §2.2], which quotes the definition of [MST]: if P satisfies \begin{quote} (A1) P reduces to O at p, and (A2) P reduces to a nonsingular point at every bad prime, \end{quote} then $h_p(P)$ = 2 $log_p(σ_p(P)/d(P))$; for a general point $h_p(Q)$ := $h_p(nQ)/n²$ with n = $lcm(\#E(F_p)$, $lcm_{ℓ}$ $c_{ℓ}$). This is 2p times the normalisation of [MST], so the two valuations of $Reg_p$ differ by r. The pairing is $h_p(P$, R) = $(h_p(P+R)$ − $h_p(P)$ − $h_p(R))/2$ and $Reg_p$ := $det(h_p(P_i$, $P_j$)) on a basis of Λ. \textit{Which σ matters.} $σ_p$ is the Mazur–Tate sigma function: the unique odd σ(t) = t + c₂t² + ⋯ with \textbf{$σ_p$ ∈ $tZ_p[[t]]$} solving x(t) + c = −(d/ω)((1/σ)(dσ/ω)) with c = (b₂ − E₂(E, ω))/12 [Har, (2)], [MT91]; c₂ = a₁/2. Another constant in place of E₂ shifts $h_p$ by a multiple of the square of the p-adic elliptic logarithm, and only this choice keeps the coefficients in $Z_p$. Every statement below is about $σ_p$. \textit{Which model matters.} $h_p(P)$ and $v_p(h_p(P))$ are invariants of E/Q, but the two halves b and c of the decomposition of Lemma 3 are not: the substitution (x, y) ↦ (x, y + sx) with s ∈ Z carries a global minimal equation to a global minimal equation, fixes x, α, d, $φ_p$, $ψ_p$ and λ, and moves only β ↦ β + sαd, so b and c trade with each other while min(b, c) stands. Since p is odd, s can be chosen with \textbf{p ∣ a₁}, and that is the model in which Theorem B and Theorem S are proved; in it b ≥ 2e comes for free, and the whole question is c. Statements about b or c alone are statements about a model, and the invariant form of Theorem S is $v_p(h_p(pP′))$ = 1. \textbf{Anomalous, split, ι.} p is \textit{anomalous} when p ∣ $\#E(F_p)$, which for p ≥ 7 means $\#E(F_p)$ = p (§3.1); E is \textit{split at p} when $E(Q_p)[p]$ ≠ 0; ι says that Λ → $E(F_p)$ is onto. \textbf{Division polynomials.} $φ_n$, $ψ_n$, $ω_n$ are normalised by x(nQ) = $φ_n/ψ_n²$, y(nQ) = $ω_n/ψ_n³$, with $φ_n$ monic of degree n² in x. For odd n and a rational cyclic D of order n, the Vélu isogeny $π_D$ : E → E/D has x-part $\bar{φ}/\bar{ψ}²$ with $\bar{ψ}(x)$ = $∏_{{±T}⊂D∖{O}}(x$ − x(T)) monic of degree (n−1)/2 and $\bar{φ}$ monic of degree n. Modulo p, for E ordinary, $φ_p(x)$ = $f(x^p)$ and $ψ_p(x)$ = $g(x^p)$ in $F_p[A$, B][X] with f monic of degree p in X, g of degree (p−1)/2 with leading coefficient the Hasse invariant, and f/g² the x-part of the Verschiebung V; when p is anomalous, ker V = $E(F_p)$. \textbf{Grades.} \textbf{[Lean]} kernel-checked, no \texttt{sorry}, no \texttt{native\_\allowbreak{}decide}, axioms within [propext, Classical.choice, Quot.sound]; \textbf{[paper]} a complete proof here or cited; \textbf{[computation]} verified over a stated range; \textbf{[known]} in the literature. Where grades mix, the weakest governs. \section*{3. Main theorems} Throughout, p ≥ 5 is a prime of good ordinary reduction for E. \subsection*{3.1 The baseline, and the decomposition of the height} \begin{quote} \begin{namedthm}[Theorem A (baseline) [paper]] Let G := \{P ∈ E(Q) : (A1) and (A2) hold\} and k := [Λ : image of G]. Then $v_p(Reg_p)$ ≥ r − 2 $v_p(k)$. If moreover p ∤ $∏_{ℓ}$ $c_{ℓ}$, then $v_p(k)$ ≤ 1, with equality exactly when the image of Λ in $E(F_p)$ meets $E(F_p)[p]$ ≠ 0, so that \textgreater{} $v_p(Reg_p)$ ≥ r − 2 in that case, $v_p(Reg_p)$ ≥ r otherwise. \end{namedthm} \end{quote} The hypothesis is the one the proof uses and is weaker than $a_p$ = 1: by Hasse, p ∣ $\#E(F_p)$ forces $\#E(F_p)$ ∈ \{p, 2p\} for p ≥ 5, and 2p occurs only at p = 5 with $a_p$ = −4, so for p ≥ 7 it is exactly $a_p$ = 1, $E(F_p)$ ≅ Z/p and the condition on Λ is ι, while at p = 5 with $\#E(F_5)$ = 10 it is strictly weaker than ι. \textbf{Everything after Lemma 4 assumes $\#E(F_p)$ = p}, and no statistic below mixes the two. The argument is index bookkeeping and nothing more (§4.2), and it is known (§9); we give it because the rest of the paper is measured against it. What it does \textit{not} give is control on the entries of the height matrix, only on the determinant (§3.2). For P satisfying (A1) and (A2), with e := $v_p(t(P))$ ≥ 1: \begin{quote} \begin{namedthm}[Lemma 1 [paper]] $σ_p(P)/d(P)$ ∈ $Z_p^{×}$. \textbf{Lemma 2 [paper].} $h_p(P)$ ∈ $2pZ_p$; more precisely $v_p(h_p(P))$ = 1 + $v_p(q_p(σ_p(P)/d(P)))$. \textbf{Lemma 3 (decomposition) [paper].} With u(P) := $σ_p(t)/t$ ∈ 1 + $p^eZ_p$ and $n_{ℓ}(P)$ := $v_{ℓ}(α)$ − $v_{ℓ}(β)$ ∈ Z, \textgreater{} $h_p(P)$ = 2 $log_p(u(P))$ + 2 $Σ_{ℓ≠p}$ $n_{ℓ}(P)$ $log_p(ℓ)$ =: $2Λ_{σ}$ + 2A, and, with b := $v_p(Λ_{σ})$ and c := $v_p(A)$: b ≥ e (and b ≥ 2e when p ∣ a₁), and \textbf{c ≥ 1}. \end{namedthm} \end{quote} By §2 the pair (b, c) depends on the model and min(b, c) does not; in the model with p ∣ a₁ one has b ≥ 2e ≥ 2 for free. \subsection*{3.2 The main theorem} \begin{quote} \textbf{Integrality theorem for the p-adic regulator at split anomalous primes} (\textit{Split-integrality theorem}) \textbf{[paper].} Suppose $\#E(F_p)$ = p, p ∤ $∏_{ℓ}$ $c_{ℓ}$ and ι. Then, with $M_{Λ}$ the height matrix on a basis of Λ, \textgreater{} \textbf{(i)} every entry of $M_{Λ}$ lies in $Z_p$ ⟺ $E(Q_p)[p]$ ≠ 0; \textgreater{} \textgreater{} \textbf{(ii)} if r = 1, then $v_p(Reg_p)$ ≥ 0 ⟺ $E(Q_p)[p]$ ≠ 0, and in the non-split case $v_p(Reg_p)$ = −1 exactly; \textgreater{} \textgreater{} \textbf{(iii)} if $E(Q_p)[p]$ ≠ 0, then $v_p(Reg_p)$ ≥ max(r − 2, 0) in every rank. Without ι the hypothesis of Theorem A is not met and that theorem already gives $v_p(Reg_p)$ ≥ r. \end{quote} Three things are being said, and only some of them are new against Theorem A. \textit{The pairing.} That the \textbf{entries} are integral, and that they cease to be exactly when $E(Q_p)[p]$ = 0, does not follow from any determinant bound. The direction ⟸ of (i) is the mechanism of §4.8; the direction ⟹ is Theorem S, which produces an entry of valuation −1 whenever the reduction sequence does not split. This is what the proof gives, and it holds in every rank. \textit{The determinant.} Since max(r−2, 0) = r−2 for r ≥ 2, the bound on $v_p(Reg_p)$ is new only in \textbf{rank one}, where the baseline −1 becomes 0 and, by (ii), is attained exactly in the non-split case: Theorem A says the rank-one regulator may fail to be integral, and (ii) says which curves those are. \textit{The baseline.} r − 2 in higher rank is the elementary count of §4.2 and is not ours. \subsection*{3.3 The criterion: one element of $F_p$} Let $\#E(F_p)$ = p, P′ ∈ E(Q) with reduction of exact order p and satisfying (A2), P := pP′, e := $v_p(d(P))$. \begin{quote} \begin{namedthm}[Lemma 4 (splitting and depth) [paper]] $E(Q_p)[p]$ ≠ 0 ⟺ e ≥ 2. \textbf{Lemma 4′ (the same, read locally) [paper].} Let $\bar{ψ}(x)$ := $∏_{{±T} ⊂ E(F_p)∖{O}}$ (x − x(T)) ∈ $F_p[x]$, monic of degree (p−1)/2. Then $ψ_p$ ≡ $u·\bar{ψ}^p$ (mod p) for some u ∈ $F_p^{×}$; hence p ∣ $ψ_p′$ and \textgreater{} p² ∣ $ψ_p(x₀$ + pk) − $ψ_p(x₀)$ for all x₀, k ∈ $Z_p$. Consequently, for an integral lift x₀ of a class $\bar{x}$ ∈ $E(F_p)∖{O}$: $v_p(ψ_p(x₀))$ ≥ 1, \textbf{$min(v_p(ψ_p(x₀))$, 2) depends on $\bar{x}$ only} and not on the lift, and $E(Q_p)[p]$ ≠ 0 ⟺ $v_p(ψ_p(x₀))$ ≥ 2. \end{namedthm} \end{quote} The \textit{exact} value of $v_p(ψ_p(x₀))$ is \textbf{not} a function of $\bar{x}$ alone once it is ≥ 2 (§5.2), which is why only the cut at 2 is used; Lemma 4′ is what makes the measurements of §5.2 legitimate. \begin{quote} \begin{namedthm}[Theorem B (criterion) [paper; arithmetic step in Lean]] Put λ := $q_p(φ_p(P′))/2$ ∈ $F_p$. If e ≥ 2, or if the model is chosen with p ∣ a₁, then $q_p(α(P)/β(P))$ = −λ, hence \textbf{c ≥ 2 ⟺ λ = 0}. \textbf{Theorem B′ (the general model) [paper].} Without either hypothesis $q_p(α(P)/β(P))$ = −λ − w₁/2, where w₁ := $a₁·ω_p(P′)·(ψ_p(P′)/p)/φ_p(P′)²$ mod p. \textbf{Lemma 5 (λ is local and finite) [paper].} $φ_p$ mod p is a polynomial in $x^p$, so $φ_p(x)$ mod p² depends only on x mod p. Hence λ = λ(E mod p², $\bar{x}$) is a function of the reduction of E modulo p² and of the class $\bar{x}$ ∈ $E(F_p)∖{O}$ alone: not of the global point, not of the height, not of the lift. \end{namedthm} \end{quote} By Theorem B and Lemma 3 the second p-adic digit of the height is λ, in a model chosen with p ∣ a₁. The rest of §3 determines λ. \subsection*{3.4 The two directions of the criterion} \begin{quote} \begin{namedthm}[Theorem C (Vélu factorisation) [paper]] Let K be a field of characteristic 0, E/K given by a Weierstrass equation, n ≥ 3 odd, D ⊂ $E(\bar{K})$ a Galois-stable cyclic subgroup of order n, and T ∈ D∖\{O\} with x(T) ∈ K. Then, with $\bar{φ}$ monic of degree n as in §2, \textgreater{} $φ_n(x(T))$ = $\bar{φ}(x(T))^n$. \textbf{Corollary D [paper].} If p is anomalous and $E(Q_p)[p]$ ≠ 0, then $λ(\bar{x})$ = 0 for every $\bar{x}$ ∈ $E(F_p)∖{O}$. \textbf{Corollary E [paper; arithmetic step in Lean].} In the situation of §3.3, if E is split at p then c ≥ 2. \end{namedthm} \end{quote} The converse holds, and the equivalence it produces is a known criterion for local torsion. \begin{quote} \begin{namedthm}[Proposition 6 (a known criterion, read as a Fermat quotient) [paper; known]] Let p ≥ 5 be a prime of good ordinary reduction with $\#E(F_p)$ = p. Then for every $\bar{x}$ ∈ $E(F_p)∖{O}$, \textgreater{} $λ(\bar{x})$ = 0 ⟺ $E(Q_p)[p]$ ≠ 0. Neither side depends on the lift x₀ or on the model, and both are determined by E mod p². \end{namedthm} \end{quote} The equivalence is known. It is the case n = 1 of Gross's tameness criterion — for good ordinary reduction with E[p] irreducible, the decomposition group at p is diagonalisable modulo $p^{n+1}$ exactly when $j_E$ ≡ j₀ (mod $p^{n+1}$), j₀ the j-invariant of the canonical lift, quoted as [LR, Thm 4.1] — and it is the content of [DW, Lemma 3.2 and Cor. 3.5], where the primes with $E(Q_p)[p]$ ≠ 0 are the \textit{local torsion primes} and the criterion reads: of the lifts of Ē to Z/p², exactly those congruent to the canonical lift have a rational point of order p. What we did not find in the sources we read is the presentation of that condition as the vanishing of a Fermat quotient of $φ_p$ at a single point (§9); the proof in §4.6 is independent of the sources above and gives the statement for all p ≥ 5 without a bound. \subsection*{3.5 The non-split case: the exact value} \begin{quote} \begin{namedthm}[Theorem S [paper; arithmetic steps in Lean]] Suppose $\#E(F_p)$ = p, p ∤ $∏_{ℓ}$ $c_{ℓ}$, and let P′ ∈ E(Q) have reduction of exact order p and reduce to a nonsingular point at every bad prime; put P := pP′. If $E(Q_p)[p]$ = 0 then \textgreater{} $v_p(h_p(P))$ = 1 exactly, hence $v_p(h_p(P′))$ = −1. \end{namedthm} \end{quote} So in the non-split case the height of a point of Λ∖Λ₀ is not p-integral, which is the direction ⟹ of (i) and the exact value in (ii). The invariance is worth stating: the quantity that Theorem S pins down is $v_p(h_p(pP′))$, not b or c separately, and the model with p ∣ a₁ is where the proof runs (§2, §4.7). \subsection*{3.6 Two further properties of λ} \begin{quote} \begin{namedthm}[Theorem H (scaling) [paper; arithmetic step in Lean]] Let p be anomalous, Q ∈ $E(Z_p)$ with $\bar{Q}$ ≠ O, and m prime to p. Then $q_p(φ_p(x(mQ)))$ = $m²·q_p(φ_p(x(Q)))$, that is λ(m $\bar{x}$) = m² $λ(\bar{x})$. \textbf{Corollary H′ [paper, in Lean].} λ vanishes at one nonzero class of $E(F_p)$ if and only if it vanishes at all of them; λ is a quadratic, not a linear, function on $E(F_p)$ ≅ Z/p. \textbf{Theorem L (the canonical subgroup contributes a p-th power) [paper].} Let C := Ê[p], which is $Q_p-rational$ for good ordinary reduction, $π_C$ : E → E″ := E/C the Vélu isogeny with x-part $φ_C/ψ_C²$, and $\hat{π}_C$ the dual with x-part $φ_{\hat{π}}/ψ_{\hat{π}}²$, the leading coefficient of $φ_{\hat{π}}$ being A. For Q ∈ $E(Z_p)$ with $\bar{Q}$ ≠ O and ξ := $φ_C(\bar{x})/ψ_C(\bar{x})²$, \textgreater{} $A·φ_p(\bar{x})$ = $(ψ_C(\bar{x})²)^p$ · $φ_{\hat{π}}(ξ)$, so in $Q_p^{×}/(Q_p^{×})^p$ the class of $φ_p(\bar{x})$ is that of $φ_{\hat{π}}(ξ)/A$, and A = c² with $\hat{π}_C^*ω_E$ = $c·ω_{E″}$. \end{namedthm} \end{quote} \subsection*{3.7 The CM case} \begin{quote} \begin{namedthm}[Theorem F [paper, using Deuring's lifting theorem]] Suppose E/Q has complex multiplication by an order O of conductor f in an imaginary quadratic field k, p ≥ 5 is a prime of good reduction which is ordinary (equivalently, split in k), p ∤ f, and $a_p$ = 1. Then $E(Q_p)[p]$ ≠ 0. (For E/Q the thirteen possible orders have f ∈ \{1, 2, 3\}, so p ∤ f is automatic for p ≥ 5.) \textbf{Corollary F′ [paper].} If in addition p ∤ $∏_{ℓ}$ $c_{ℓ}$, then $v_p(Reg_p)$ ≥ max(r − 2, 0); in rank one, $v_p(Reg_p)$ ≥ 0. So a CM curve never shows the deficit at a prime of good ordinary reduction. \end{namedthm} \end{quote} \subsection*{3.8 A rank-theoretic refinement of the baseline} \begin{quote} \begin{namedthm}[Theorem J [paper; determinant step in Lean]] Assume $\#E(F_p)$ = p, ι, p ∤ $∏_{ℓ}$ $c_{ℓ}$. Let Λ₀ := ker(Λ → $E(F_p)$), $M_{Λ₀}$ the height matrix on a basis of Λ₀ (entries in $pZ_p$ by Lemma 2), and $ρ_0$ := $rank_{F_p}((M_{Λ₀}/p)$ mod p). Then $v_p(Reg_p)$ = $v_p(det$ $M_{Λ₀}$) − 2 ≥ 2r − 2 − $ρ_0$. \end{namedthm} \end{quote} With $ρ_0$ ≤ r this recovers Theorem A; the stronger bound max(2r−4, 0) that its shape suggests is \textbf{false} (§5.3). \section*{4. Proofs} \subsection*{4.1 Lemmas 1–3} \textit{Lemma 1.} $σ_p(t)/t$ ∈ 1 + $tZ_p[[t]]$ and $v_p(t)$ = e ≥ 1, so $v_p(σ_p(t))$ = e; from $v_p(x(P))$ = −2e and gcd(α, d) = 1 we get $v_p(d)$ = e and $v_p(α)$ = 0, whence $v_p(σ_p(P)/d(P))$ = 0. ∎ \textit{Lemma 2.} For w ∈ $Z_p^{×}$ one has $w^{p−1}$ ∈ 1 + $pZ_p$ and log(1 + px) ∈ $pZ_p$, so $v_p(log_p$ w) ≥ 1, refined as in §2; apply this to w = $σ_p(P)/d(P)$. ∎ \textit{Lemma 3.} From t = −x/y and x = α/d², y = β/d³ we get t/d = −α/β, hence $σ_p(P)/d(P)$ = u(P)·(−α(P)/β(P)) with u = $σ_p(t)/t$ ∈ 1 + $p^eZ_p$. Taking $log_p$, using $log_p(−1)$ = 0 and factoring α/β into primes ℓ ≠ p (both are prime to p by Lemma 1), gives the decomposition with $n_{ℓ}$ ∈ Z; each ℓ is a p-adic unit, so $v_p(log_p$ ℓ) ≥ 1 by Lemma 2, and c ≥ 1 as the $n_{ℓ}$ are rational integers. Finally u ∈ 1 + $p^eZ_p$ gives b ≥ e, and b ≥ 2e when p ∣ a₁, the coefficient c₂ = a₁/2 of $σ_p$ then being divisible by p. ∎ \subsection*{4.2 Theorem A} (1) If P, R, P+R ∈ G, Lemma 2 puts all three heights in $2pZ_p$ and p is odd, so $h_p(P,R)$ ∈ $pZ_p$; the matrix $M_G$ on a basis of the image of G has entries in $pZ_p$, and every term of the Leibniz expansion of det $M_G$ has valuation ≥ r. (2) A change of basis between G and Λ has determinant ±k, so det $M_G$ = k² det $M_{Λ}$ and $v_p(Reg_p)$ ≥ r − $2v_p(k)$. (3) Λ/(image of G) embeds into $E(F_p)$ × $∏_{ℓ}$ $Φ_{ℓ}(F_{ℓ})$, so for p ∤ $∏_{ℓ}$ $c_{ℓ}$ the p-part comes from $E(F_p)$, which by Hasse has order \textless{} p², its p-part cyclic of order at most p. Hence $v_p(k)$ ≤ 1, with equality exactly when p ∣ $\#E(F_p)$ and the reduction of Λ meets $E(F_p)[p]$. ∎ \subsection*{4.3 Lemmas 4 and 4′} (⟹) Let τ ∈ $E(Q_p)$ have order p. For p ≥ 5 the formal group $Ê(pZ_p)$ is torsion-free, so $\bar{τ}$ ≠ O, and $\#E(F_p)$ = p gives $E(F_p)$ = $⟨\bar{τ}⟩$; hence R := P′ − jτ ∈ $E_1(Q_p)$ for some j and pP′ = pR. For a formal group over $Z_p$, [p](t) = pt + (higher terms with $Z_p$ coefficients), so $v_p([p](t))$ ≥ min(1 + $v_p(t)$, $2v_p(t)$) ≥ 2 whenever $v_p(t)$ ≥ 1. Thus e = $v_p(t(pP′))$ ≥ 2. (⟸, contrapositive) If $E(Q_p)[p]$ = 0 then $E(Q_p)$ is torsion-free, prime-to-p torsion injecting into $E(F_p)$ of order p, and being a compact p-adic Lie group of dimension 1 it is ≅ $Z_p$ with $E_1(Q_p)$ = $pE(Q_p)$ of index p. Torsion-freeness lets one \textit{extend} the formal logarithm by ℓ(P) := $log_E(pP)/p$, an injective homomorphism with $ℓ(E(Q_p))$ = $Z_p$ and $ℓ(E_1(Q_p))$ = $pZ_p$, since $log_E$ : $E_1(Q_p)$ ≅ $pZ_p$ for p ≥ 5. So ℓ(P′) ∈ $Z_p^{×}$ when $\bar{P}′$ ≠ O, $v_p(log_E(pP′))$ = 1, and as $v_p(log_E(t))$ = $v_p(t)$ on $E_1$, e = 1. ∎ \textit{Lemma 4′.} E being ordinary at p, E[p] over $\bar{F}_p$ is an extension of the étale Z/p by $μ_p$, with p distinct geometric points each of multiplicity p, and Frobenius acts on $E[p]^{ét}$ through the unit root of X² − $a_pX$ + p ≡ X² − X (mod p), hence trivially; so $E[p]^{ét}$ ⊂ $E(F_p)$, with equality as $\#E(F_p)$ = p. The divisor of $ψ_p$ mod p on the x-line is therefore $p·Σ_{±T}(x(T))$ over the (p−1)/2 classes of $E(F_p)∖{O}$, which matches deg $ψ_p$ − (p−1)/2 since $ψ_p$ has leading coefficient p; hence $ψ_p$ ≡ $u·\bar{ψ}^p$ (mod p), p ∣ $ψ_p′$, and p² ∣ $ψ_p(x₀+pk)$ − $ψ_p(x₀)$ by the step of Lemma 5, so $min(v_p(ψ_p(x₀))$, 2) is a function of $\bar{x}$. For the last claim lift $\bar{x}$ to Q ∈ $E(Z_p)$: as $φ_p$ and $ψ_p²$ are coprime with resultant a power of Δ ∈ $Z_p^{×}$ [known] and $v_p(x(pQ))$ \textless{} 0, we get $v_p(ψ_p(x(Q)))$ = $v_p(t(pQ))$, and Lemma 4 gives $E(Q_p)[p]$ ≠ 0 ⟺ $v_p(ψ_p(x₀))$ ≥ 2. ∎ \subsection*{4.4 Theorem B, Theorem B′, Lemma 5} \textit{Step 1 (denominators do not matter).} Write x(P′) = a/d′², y(P′) = b/d′³ with p ∤ d′, possible as $\bar{P}′$ ≠ O. Homogenising, Φ := $d^{\prime 2p²}φ_p(P′)$, Ψ := $d^{\prime p²−1}ψ_p(P′)$, $\tilde{Ω}$ := $d^{\prime 3p²}ω_p(P′)$ are integers, and \begin{quote} x(P) = Φ/(d′Ψ)², y(P) = $\tilde{Ω}/(d′Ψ)³$, so d(P) = d′\textbar{}Ψ\textbar{}, α = ±Φ, β = $±\tilde{Ω}$, α/β = $(φ_p(P′)/ω_p(P′))·d^{\prime −p²}$. \end{quote} That d(P) = d′\textbar{}Ψ\textbar{} with no cancellation is where (A2) is used: it is what the factor $∏_{ℓ}$ $c_{ℓ}$ in the definition of P′ secures, and it fails without it (§5.5). As $q_p$ is a homomorphism and $q_p(d^{\prime p²})$ = 0, \begin{quote} $q_p(α/β)$ = $q_p(φ_p(P′))$ − $q_p(ω_p(P′))$. (∗) \end{quote} \textit{Step 2 (the Weierstrass equation).} Multiply it at pP′ by $ψ_p(P′)^6$ and write φ = $φ_p(P′)$, ω = $ω_p(P′)$, ψ = $ψ_p(P′)$: \begin{quote} ω² + a₁φωψ + a₃ωψ³ = φ³ + a₂φ²ψ² + a₄φψ⁴ + a₆ψ⁶. \end{quote} Since $v_p(ψ)$ = $v_p(d(P))$ = e (as p ∤ d′), every term of ω² − φ³ other than a₁φωψ has valuation ≥ 2e, and that one has valuation $v_p(a₁)$ + e. Hence ω² ≡ φ³ (mod p²) under either hypothesis of Theorem B: e ≥ 2, or p ∣ a₁ with e ≥ 1. \textit{Step 3.} Write $φ^{p−1}$ = 1 + pA′, $ω^{p−1}$ = 1 + pB′. Raising ω² ≡ φ³ (mod p²) to the power p−1 gives 2B′ ≡ 3A′ (mod p), so with λ := A′/2 mod p = $q_p(φ)/2$ we get $q_p(φ)$ = 2λ, $q_p(ω)$ = 3λ, and (∗) gives $q_p(α/β)$ = −λ, while c ≥ 2 ⟺ $q_p(α/β)$ = 0 (§2). In the form 2(A′ − B′) = −A′ the implication λ ≠ 0 ⟹ $q_p(α/β)$ ≠ 0 needs no division. Under neither hypothesis the term a₁φωψ survives modulo p²; dividing by φ³ and using $q_p(1+pw)$ = −w gives the correction w₁ of Theorem B′. ∎ \textit{Lemma 5.} In characteristic p, [p] = V ∘ F and E is defined over $F_p$, so x ∘ [p] is a rational function of $x^p$; hence $φ_p$ mod p is a polynomial in $x^p$ and $φ_p′$ ≡ 0 (mod p). For a polynomial f with p ∣ f′(x) one has p² ∣ f(x + pk) − f(x) (the Lean statement \texttt{eval\_\allowbreak{}sub\_\allowbreak{}eval\_\allowbreak{}dvd\_\allowbreak{}sq}), so $φ_p(x)$ mod p² depends only on x mod p. ∎ \subsection*{4.5 Theorem C, Corollary D, Corollary E} \textit{Theorem C.} D being Galois-stable of order n, $π_D$ and $\hat{π}_D$ are defined over K and [n] = $\hat{π}_D$ ∘ $π_D$. Fix a Weierstrass model of E/D and write x ∘ $\hat{π}_D$ = $φ_{\hat{π}}/ψ_{\hat{π}}²$ with $φ_{\hat{π}}(X)$ = $Σ_{i≤n}$ $c_i$ $X^i$, $c_n$ = A ≠ 0 and deg $ψ_{\hat{π}}²$ = n − 1. Clearing denominators in x ∘ [n] = $(φ_{\hat{π}}/ψ_{\hat{π}}²)∘(\bar{φ}/\bar{ψ}²)$, \begin{quote} N(x) := $Σ_{i≤n}$ $c_i$ $\bar{φ}(x)^i$ $\bar{ψ}(x)^{2(n−i)}$, Den(x) := $\bar{ψ}^{2n}·ψ_{\hat{π}}(\bar{φ}/\bar{ψ}²)²$, $φ_n/ψ_n²$ = N/Den. \end{quote} Now $deg(\bar{φ}^i$ $\bar{ψ}^{2(n−i)}$) = n² − n + i, so i = n alone attains the top degree: deg N = n² with leading coefficient A $(\bar{φ}$ being monic) and deg Den = n² − 1. Since x ∘ [n] : P¹ → P¹ has degree n², and the degree of a reduced representation is the larger of the two, cancelling a common factor of degree d would give n² − d = n²; so d = 0, N/Den is reduced, and as $φ_n$ and $ψ_n²$ are coprime with $φ_n$ monic, N = $A·φ_n$. At x = x(T) one has $\bar{ψ}(x(T))$ = 0, so every term with i \textless{} n vanishes and N(x(T)) = $A·\bar{φ}(x(T))^n$. ∎ \textit{Corollary D.} Let τ ∈ $E(Q_p)$ have order p; as in Lemma 4, $\bar{τ}$ ≠ O. D := ⟨τ⟩ is $Q_p-rational$ with D∖\{O\} ⊂ $E(Q_p)$, so x(T) ∈ $Z_p$ and Theorem C gives $φ_p(x(T))$ = $\bar{φ}(x(T))^p$. Both sides are p-adic units, $φ_p$ = $x(pQ)ψ_p²$ with $v_p(x(pQ))$ = −2e and $v_p(ψ_p)$ = e, so $q_p(φ_p(x(T)))$ = $p·q_p(\bar{φ}(x(T)))$ = 0 in $F_p$. The reduction D∖\{O\} → $E(F_p)∖{O}$ is injective (D ∩ Ê = 0) between sets of cardinality p − 1, hence bijective, so x(T) mod p runs over all nonzero classes; by Lemma 5, λ ≡ 0. ∎ \textit{Corollary E.} Lemma 4 gives e ≥ 2, Corollary D gives λ = 0, Theorem B gives $q_p(α/β)$ = 0, that is c ≥ 2. ∎ \subsection*{4.6 Proposition 6, the direction λ = 0 ⟹ split} The statement is [known] (§3.4); the argument below is independent of the sources cited there and carries no bound on p. It is given in outline. The arithmetic steps are the Lean theorems of \texttt{PadicHeightValuation\{5,6,7\}} (§6); the analytic steps use the Tate parametrisation as recorded in [ATAEC] and [Dok]. \textit{(1) An Euler identity.} $φ_p$ is weighted homogeneous of weight 2p² for weights (4, 6, 2) on (A, B, x); giving X = $x^p$ the weight 2p and reducing $4A∂_Aφ_p$ + $6B∂_Bφ_p$ + $2x∂_xφ_p$ = $2p²φ_p$ modulo p, both the right-hand side and $∂_x$ $f(x^p)$ vanish, leaving $4A·∂_A$ f + $6B·∂_B$ f = 0 in $F_p[A$, B][X]. Hence A ∣ $∂_B$ f; put ũ := $(∂_B$ f)/A. \textit{(2) One slope.} For $E_s$ : y² = x³ + (a₄ + sp)x + a₆ a Taylor expansion of $φ_p$ in its coefficients gives $λ_s$ = $λ_0$ − s·B₄/2, and likewise a slope B in the a₆ direction. λ is invariant under (x, y) ↦ (u²x, u³y), $φ_p$ transforming by the p-th power $u^{2p²}$; with u = 1 + pt that invariance reads 4a₄B₄ + 6a₆B ≡ 0, which is (1) again, so both slopes are multiples of one scalar $ρ(\bar{x})$ = $−ũ(\bar{x})/(4f(\bar{x}))$, the denominator being non-zero by Vélu's formulas in the shape f(X₀) = $4Y₀²g′(X₀)²/c_V²$. By Serre–Tate theory the family $E_s$ exhausts the deformations of Ē over Z/p² and exactly one member splits, where λ = 0 by Corollary D. An affine function with non-zero slope vanishes once, so ρ ≠ 0 gives the assertion. \textit{(3) A dichotomy.} $Res_X(ũ$, g) has weight (p−1)(p−2)(p+3) = 12 $m_p$. Take the transversal family $E_t$ : y² = x³ − 3x + (2 + t) over $\bar{F}_p((t))$ at the cusp, of split multiplicative reduction with v(q) = v(Δ) = 1 [ATAEC, Thm V.5.3], [Dok, Thm A.1]; the Tate parametrisation [ATAEC, Thm V.3.1] gives ker V = ⟨q⟩ mod $q^p$, so the roots of g have $v(β_j$ − 1) = j (1 ≤ j ≤ n := (p−1)/2), those of f have valuations \{0, 1, 1, …, n, n\}, and the Newton polygon of f gives $v(f(β_j))$ = j(p−j). Here ũ = −(1/3)(d/dt)f, and differentiation lowers a valuation by at most 1, so $ord_{Δ}$ $Res_X(ũ$, g) ≥ $Σ_j$ (j(p−j) − 1) = $m_p$; weighted homogeneity then forces $Res_X(ũ$, g) = $c_p·Δ^{m_p}$ with $c_p$ ∈ $F_p$ constant. For each p, either ρ ≠ 0 for every ordinary curve over $\bar{F}_p$ and every point of ker V∖\{O\}, or ρ = 0 for all of them. \textit{(4) Which side.} $E^{(p)}$ is the member of the same family at parameter $t^p$, hence defined over $K^p$, so d/dt reaches only the argument of the Tate parameter and $v(dβ_j/dt)$ = j − 1 exactly. Of the p−2j+1 roots of f at distance j from $β_j$, the two flanking ones contribute 1/(1−u) + $1/(1−u^{−1})$ = 1 between them, so $f′(β_j)/f(β_j)$ has valuation exactly −j with leading coefficient p − 2j ≡ −2j. The chain rule gives $12ρ_j$ = (d/dt)log $f(β_j)$ − $f′(β_j)(dβ_j/dt)/f(β_j)$ = (−j² + 2j²)/t + O(1): the residues −j² and −2j² differ by j² ≠ 0, so $v(ρ_j)$ = −1, $ord_{Δ}$ $Res_X(ũ$, g) = $m_p$ exactly, and $c_p$ ≠ 0. ∎ The naive estimate fails — the second term has valuation −1, not ≥ 0 — and what closes the argument is that the two residues differ. \subsection*{4.7 Theorem S} Choose the model with p ∣ a₁ (§2); e = 1 since E is not split (Lemma 4). Then b ≥ 2e = 2 by Lemma 3, and by Theorem B, applicable in this model for e ≥ 1, $q_p(α/β)$ = −λ with λ ≠ 0 by Proposition 6; so c = 1. From $h_p(P)/2$ = $Λ_{σ}$ + A with b ≥ 2 \textgreater{} 1 = c we get $v_p(h_p(P)/2)$ = 1, and p is odd, so $v_p(h_p(P))$ = 1. Finally $h_p$ is a quadratic form, so $h_p(P)$ = $p²h_p(P′)$ and $v_p(h_p(P′))$ = −1. ∎ \subsection*{4.8 The main theorem} Put n := $∏_{ℓ}$ $c_{ℓ}$, so p ∤ n. As $h_p$ is a quadratic form, $v_p(h_p(P))$ = $v_p(h_p(nP))$; and nP satisfies (A2) for every P ∈ E(Q). \textit{(⟸ of (i)), case P ∈ Λ∖Λ₀.} Then $\bar{P}$ has order exactly p, $\#E(F_p)$ being p, and so does the reduction of P′ := nP as p ∤ n; P″ := pP′ satisfies (A1) and (A2). As E is split, Lemma 4 gives e = $v_p(d(P″))$ ≥ 2, hence b ≥ e ≥ 2 by Lemma 3 and c ≥ 2 by Corollary E, so $v_p(h_p(P″))$ ≥ 2; and $h_p(P″)$ = $p²h_p(P′)$ gives $v_p(h_p(P))$ = $v_p(h_p(P′))$ ≥ 0. \textit{(⟸ of (i)), case P ∈ Λ₀.} Then nP satisfies (A1) and (A2), so $h_p(nP)$ ∈ $2pZ_p$ by Lemma 2 and $v_p(h_p(P))$ ≥ 1. So $v_p(h_p(P))$ ≥ 0 for every P ∈ Λ. Polarising, $h_p(P,R)$ ∈ $Z_p$ since p is odd; every entry of the height matrix on any basis of Λ lies in $Z_p$, every term of the Leibniz expansion has valuation ≥ 0, and $v_p(Reg_p)$ ≥ 0. With Theorem A this is (iii). \textit{(⟹ of (i)).} Suppose $E(Q_p)[p]$ = 0. By ι there is P ∈ Λ whose reduction has order p; with P′ := nP, Theorem S gives $v_p(h_p(P′))$ = −1, hence $v_p(h_p(P))$ = −1. If every entry of $M_{Λ}$ were in $Z_p$ then so would be the value of the quadratic form at every point of Λ (the Lean statement \texttt{quadratic\_\allowbreak{}value\_\allowbreak{}mem\_\allowbreak{}of\_\allowbreak{}entries\_\allowbreak{}mem}), a contradiction. \textit{(ii).} Let r = 1 and let Q generate Λ; by ι, Q ∉ Λ₀ and $Reg_p$ = $h_p(Q)$. If E is split then $v_p(Reg_p)$ ≥ 0 by the first case above. If not, Theorem S gives $v_p(Reg_p)$ = −1 exactly. ∎ The choice of lattice is what carries the proof: what is needed is $v_p(h_p)$ ≥ 0 on Λ, not $v_p(h_p)$ ≥ 2 on Λ₀, and for a point of Λ∖Λ₀ it is enough that its reduction have order p. \subsection*{4.9 Theorems H, L, F, J} \textit{Theorem H.} The composition rule $ψ_{ab}(R)$ = $ψ_b(R)^{a²}ψ_a(bR)$ at (a,b) = (p,m) and (m,p), with $φ_k(x(R))$ = $x(kR)ψ_k(R)²$ and $φ_m$ monic of degree m² over Z[a₁,…,a₆] evaluated at X := x(pQ) of valuation −2e ≤ −2, gives the exact identity \begin{quote} $φ_p(x(mQ))·ψ_m(Q)^{2p²}$ = $φ_p(x(Q))^{m²}·(1$ + δ), δ ∈ $p²Z_p$. (★) \end{quote} Only even powers of $ψ_m(Q)$ occur, so (★) is well posed for every m prime to p. Its three division-polynomial values are p-adic units, $ψ_m(Q)^{2p²}$ is a p-th power and 1 + δ ∈ 1 + $p²Z_p$, so $q_p$ applied to (★) gives the claim; Corollary H′ follows since $E(F_p)$ ≅ Z/p and m² ≠ 0 in $F_p$. ∎ \textit{Theorem L.} Repeat the computation of Theorem C with D = C = Ê[p], Galois-stable for good ordinary reduction: N(x) = $ψ_C(x)^{2p}·φ_{\hat{π}}(φ_C(x)/ψ_C(x)²)$, the degree count is unchanged, so N = $A·φ_p$ and evaluating at $\bar{x}$ gives the identity, the factor $(ψ_C(\bar{x})²)^p$ being a p-th power. The leading coefficient of the x-part of $\hat{π}_C$ is $c^{−2}$, since $t_E(\hat{π}_C$ R) = c·t″(R) + O(t″²), whence A = c². ∎ \textit{Theorem F.} p splits in k, so k ⊂ $Q_p$ and the CM order acts on $E_{/Q_p}$ by $Q_p-endomorphisms$; by Deuring's lifting theorem $End(E_{/Q_p})$ → $End(Ē_{/F_p})$ is an isomorphism for ordinary reduction, so Frobenius ϕ lifts to π with π + $\bar{π}$ = 1 and $π\bar{π}$ = p. Put ϱ := 1 − π = $\bar{π}$, of degree p; on the special fibre $\bar{ϱ}$ = 1 − ϕ is separable, as $(1−ϕ)^*ω$ = ω ≠ 0, so ker ϱ is étale of order p over $Z_p$. On it π = 1, so Frobenius acts trivially, and its points, being étale, are defined over $Q_p^{ur}$, where Galois acts through Frobenius. Hence ker ϱ ⊂ $E(Q_p)$. ∎ \textit{Theorem J.} [Λ : Λ₀] = p gives det $M_{Λ₀}$ = p²·det $M_{Λ}$; the entries of $M_{Λ₀}$ lie in $pZ_p$ by Lemma 2, so $M_{Λ₀}$ = p·N, and if N mod p has rank $ρ_0$, Smith normal form gives $v_p(det$ N) ≥ r − $ρ_0$. ∎ \section*{5. Computations} All computations use PARI/GP 2.17.3 with \texttt{elldata} (Cremona's tables) on one core, with positive and negative controls; none is a proof, and no number is quoted outside its stated range. \textbf{The convention, made explicit.} \texttt{ellpadicheight(E,p,n,P)} returns the coordinates [f, g] of the height on the basis (ω, η = xω) of $H¹_dR$ ⊗ $Q_p$; the height of §2 is \begin{quote} $h_p(P)$ = −( f − s₂·g ), s₂ := \texttt{ellpadics2(E,p,n)} = b₂/12 − E₂(E, ω)/12, \end{quote} since s₂ is precisely the constant c of [Har, (2)] that singles out $σ_p$: \textbf{the first component alone is a different height}, the one belonging to c = 0, whose σ is not in $tZ_p[[t]]$. As a control this reproduces the two entries of [MST, §4.2], v = −1 for 37A at p = 53 and v = +1 for 5077A at p = 5, their −2 shifted by r. Every count below was recomputed with $h_p$, the two conventions differing by a correction of valuation ≥ 0 that never moves a negative valuation. \subsection*{5.1 The decomposition} Rank one, conductor ≤ 900, $a_p$ = 1, p ≤ 43, p ∤ $∏c_{ℓ}$, ι, precision 14 — \textbf{474 boxes} — with P = nQ, n = $lcm(ord(\bar{Q})$, $∏c_{ℓ}$), b := $v_p(h_p(P)/2$ − $log_p(α/β)$), c := $v_p(log_p(α/β))$, e := $v_p(d(P))$. Lemma 3 (c ≥ 1; b ≥ e; b ≥ 2e in the 223 boxes with p ∣ a₁) and Corollary E (in the 45 split boxes) held without exception, and $v_p(h_p(P))$ = min(b, c) in 470 boxes, the other 4 having b = c with cancelling leading terms. Among the 429 non-split boxes c ≥ 2 occurred 26 times, all of them in Cremona's model with a₁ odd (§5.5). The choice of σ moves b in 98 boxes and $v_p(h_p)$ in none. \subsection*{5.2 λ = 0 ⟺ split} λ is measured with no rational point in sight: by Lemma 5 it is a function of E mod p² and $\bar{x}$, and by Lemma 4′ splitting is $v_p(ψ_p(x₀))$ ≥ 2 for an integral lift. Over all curves of conductor N ≤ 1200 (any rank), 5 ≤ p ≤ 43, $a_p$ = 1 — \textbf{1,445 boxes}, controls deg $φ_p$ = p² and leading coefficient 1 — these held with \textbf{no exception}: the scaling λ(m $\bar{x}$) = m² $λ(\bar{x})$ for m = 2, …, p−1 (Theorem H); $ψ_p$ ≡ $u·\bar{ψ}^p$ (mod p) (Lemma 4′); the invariance of $min(v_p(ψ_p(x₀))$, 2) and of λ under the lifts x₀ + kp, k ≤ 3; and \textbf{λ = 0 ⟺ split} (158 split boxes, 158 with λ = 0, the same ones), which is Proposition 6. The identity (★) was checked as an exact rational identity in 403 boxes and Theorem B′ in 310, both without exception, and splitting read independently, by \texttt{polrootspadic} on $ψ_p$, agreed wherever the PARI stack allowed it (1,234 boxes). One limit: the \textit{exact} value of $v_p(ψ_p(x₀))$ is not invariant under change of lift, failing in 85 boxes — which is why only the cut at 2 is used, and is all that Lemma 4′ proves. Proposition 6 was also tested where it is stated, over $F_p$ rather than over the tables: running (A, B) over $F_p²$ for the anomalous curves with 5 ≤ p ≤ 157 — 4,824 curves, 260,258 classes $\bar{x}$ — the slope ρ of §4.6 was non-zero without exception, the family $E_s$ contained exactly one split member, and the zero of $λ_s$ sat at that member. The identity $Res_X(ũ$, g) = $c_p·Δ^{m_p}$ was verified exactly for p = 17, 19, 23 $(m_p$ = 400, 561, 1001) at more points than the degree bound, and the cusp estimates — the valuations of the roots of f and g, $ord_t$ $Res_X(ũ$, g) = $m_p$, and the ratio of leading coefficients predicted by $12ρ_j$ = j²/t — held for p ≤ 29 without exception. \subsection*{5.3 The height matrix, the regulator, and a bound that is too strong} Conductor ≤ 1500, p ≤ 19, $a_p$ = 1, p ∤ $∏c_{ℓ}$, ι, ranks 1 and 2 — \textbf{659 boxes}: the minimum valuation of the entries of $M_{Λ}$ is 0, 1 or 2 in the 71 split boxes and −1 in every one of the 588 non-split boxes, which is part (i) of the main theorem in both directions. Rank 1, conductor ≤ 2000, p ≤ 23, $a_p$ = 1 — \textbf{1,107 boxes}: in the 8 where ι fails, $v_p(Reg_p)$ ∈ \{1,2\} ≥ r as Theorem A requires; of the other 1,099, every one of the 976 non-split boxes has $v_p(Reg_p)$ = −1 exactly and every one of the 123 split boxes has $v_p(Reg_p)$ ∈ \{0,1,2\}. Part (ii) accounts for the first; the distribution inside \{0,1,2\} is not accounted for by anything here. Rank ≥ 2, conductor ≤ 9000, p ≤ 19 — \textbf{262 boxes}: 23 split boxes of rank 2 with $v_p(Reg_p)$ ∈ \{0,1\}, so the bound 0 is attained, and one split box of rank 3 with $v_p(Reg_p)$ = 1 = max(r−2,0) \textless{} 2, which \textbf{refutes} the stronger bound max(2r−4, 0) suggested by the shape of Theorem J; in two of the 24 split boxes the height form does not vanish on the kernel of the reduction character, as that bound would require. \subsection*{5.4 CM curves} Over all curves of conductor ≤ 1500 (8,163 curves, 138 with CM) and p ≤ 43, all \textbf{14} anomalous CM boxes are split, against 178 of 1,935 in the non-CM boxes; the primes occurring are p = 7, 19, 37 for curves with j = 0, which is what $a_p$ = 1 with $π\bar{π}$ = p forces. This is the content of Theorem F, not independent evidence for it. \subsection*{5.5 The model, and the exact value in the non-split case} Conductor ≤ 3000, p ≤ 23, rank ≥ 1, $a_p$ = 1, p ∤ $∏c_{ℓ}$, ι, with P′ = $(∏c_{ℓ})·Q$ for a generator Q of non-zero reduction and P = pP′ computed exactly — \textbf{1,765 boxes}, in both Cremona's model and the model with p ∣ a₁. In the model with p ∣ a₁ the identity $q_p(α/β)$ = −λ of Theorem B held in \textbf{1,765 of 1,765}, and \textbf{no non-split box had c ≥ 2}; the positive control, 185 split boxes with λ = 0 and c ≥ 2, held throughout. In Cremona's model the same identity failed in 719 boxes, all of them with e = 1 and a₁ odd, and 90 non-split boxes had c ≥ 2, all of them with a₁ odd; the shift of §2 removes all 90. This is the numerical form of the remark that b and c are quantities of a model while min(b, c) is not. The relation d(P) = d′·\textbar{}Ψ\textbar{} — no cancellation, Step 1 of §4.4 — held in every box, and fails when the factor $∏_{ℓ}$ $c_{ℓ}$ is dropped from P′: (A2) is used at exactly that point. On the side of the height matrix, conductor ≤ 900 and p ≤ 13 with \texttt{ellpadicheightmatrix} gave \textbf{239 boxes}: $min_{i,j}$ $v_p(M_{Λ}[i,j])$ = −1 in all 206 non-split boxes and ≥ 0 in all 33 split ones. \section*{6. What is proved in Lean and what is not} Eight files, each checking from \texttt{import\ \allowbreak{}Mathlib} alone, in the namespace \texttt{PadicHeight}: \texttt{PadicHeightValuation\{,2,3,4,5,6,7,8\}.\allowbreak{}lean}. Every statement is about integers, matrices, finite sums or p-adic congruences; Mathlib has neither the p-adic sigma function nor division polynomials nor Vélu's formulas nor the Tate curve, so the geometry and the p-adic analysis enter as hypotheses. The companion \texttt{statements-and-dependencies.\allowbreak{}md} lists all Lean names; the main line is \begin{small} \begin{longtable}{>{\raggedright\arraybackslash}p{0.324\linewidth}>{\raggedright\arraybackslash}p{0.596\linewidth}>{\raggedright\arraybackslash}p{0.05\linewidth}} \hline \textbf{Statement} & \textbf{Lean name} & \textbf{File} \\ \hline \endfirsthead \hline \textbf{Statement} & \textbf{Lean name} & \textbf{File} \\ \hline \endhead \hline \endfoot Theorem A & \texttt{norm\_\allowbreak{}det\_\allowbreak{}div\_\allowbreak{}sq\_\allowbreak{}le} & 1–4 \\ Theorem B, step 3 & \texttt{fermatQuot\_\allowbreak{}sub\_\allowbreak{}iff\_\allowbreak{}of\_\allowbreak{}sq\_\allowbreak{}eq\_\allowbreak{}cube}, \texttt{dvd\_\allowbreak{}three\_\allowbreak{}mul\_\allowbreak{}sub\_\allowbreak{}two\_\allowbreak{}mul}, \texttt{sub\_\allowbreak{}ne\_\allowbreak{}zero\_\allowbreak{}of\_\allowbreak{}two\_\allowbreak{}mul\_\allowbreak{}eq\_\allowbreak{}three\_\allowbreak{}mul} & 1–4, 8 \\ Theorem B, the model with p ∣ a₁ & \texttt{sq\_\allowbreak{}sub\_\allowbreak{}cube\_\allowbreak{}dvd\_\allowbreak{}of\_\allowbreak{}dvd\_\allowbreak{}a1} (and \texttt{sq\_\allowbreak{}sub\_\allowbreak{}cube\_\allowbreak{}dvd\_\allowbreak{}of\_\allowbreak{}sq\_\allowbreak{}dvd\_\allowbreak{}psi} for e ≥ 2) & 8 \\ Lemmas 4′ and 5 & \texttt{eval\_\allowbreak{}sub\_\allowbreak{}eval\_\allowbreak{}dvd\_\allowbreak{}sq} & 1–4 \\ Corollary D & \texttt{sq\_\allowbreak{}dvd\_\allowbreak{}pow\_\allowbreak{}sub\_\allowbreak{}one\_\allowbreak{}of\_\allowbreak{}isPow} & 1–4 \\ Corollary E & \texttt{sq\_\allowbreak{}dvd\_\allowbreak{}alpha\_\allowbreak{}sub\_\allowbreak{}beta\_\allowbreak{}of\_\allowbreak{}isPow} & 1–4 \\ Theorem H & \texttt{fermatQuot\_\allowbreak{}scale} & 1–4 \\ Theorem J & \texttt{dvd\_\allowbreak{}det\_\allowbreak{}of\_\allowbreak{}col\_\allowbreak{}dvd}, \texttt{pow\_\allowbreak{}succ\_\allowbreak{}dvd\_\allowbreak{}det\_\allowbreak{}of\_\allowbreak{}col} & 1–4 \\ Main theorem, linear algebra & \texttt{regulator\_\allowbreak{}valuation\_\allowbreak{}of\_\allowbreak{}split\_\allowbreak{}anomalous} & 5 \\ Main theorem (ii), equivalence & \texttt{regulator\_\allowbreak{}valuation\_\allowbreak{}of\_\allowbreak{}split\_\allowbreak{}anomalous\_\allowbreak{}iff\_\allowbreak{}split} & 5 \\ §4.6 (2), the single slope and the affine zero & \texttt{slope\_\allowbreak{}of\_\allowbreak{}rho}, \texttt{fermatQuot\_\allowbreak{}deform}, \texttt{affine\_\allowbreak{}zero\_\allowbreak{}unique}, \texttt{lambda\_\allowbreak{}eq\_\allowbreak{}zero\_\allowbreak{}iff\_\allowbreak{}split}, \texttt{lambda\_\allowbreak{}dichotomy} & 5 \\ §4.6 (3), the weight count and the Newton polygon & \texttt{weight\_\allowbreak{}split}, \texttt{twelve\_\allowbreak{}dvd\_\allowbreak{}weight}, \texttt{sum\_\allowbreak{}pole\_\allowbreak{}orders}, \texttt{cusp\_\allowbreak{}sum\_\allowbreak{}eq\_\allowbreak{}m}, \texttt{mul\_\allowbreak{}compl\_\allowbreak{}le\_\allowbreak{}half\_\allowbreak{}mul\_\allowbreak{}half}, \texttt{eq\_\allowbreak{}C\_\allowbreak{}mul\_\allowbreak{}of\_\allowbreak{}dvd\_\allowbreak{}of\_\allowbreak{}natDegree\_\allowbreak{}eq} & 6 \\ §4.6 (4), the residues & \texttt{inv\_\allowbreak{}one\_\allowbreak{}sub\_\allowbreak{}add\_\allowbreak{}inv\_\allowbreak{}one\_\allowbreak{}sub\_\allowbreak{}inv}, \texttt{first\_\allowbreak{}term\_\allowbreak{}residue}, \texttt{second\_\allowbreak{}term\_\allowbreak{}leading\_\allowbreak{}ne\_\allowbreak{}zero}, \texttt{residues\_\allowbreak{}do\_\allowbreak{}not\_\allowbreak{}cancel}, \texttt{twelve\_\allowbreak{}mul\_\allowbreak{}sum\_\allowbreak{}cusp\_\allowbreak{}orders} & 7 \\ Theorem S, the ledger & \texttt{exists\_\allowbreak{}shift\_\allowbreak{}dvd\_\allowbreak{}a1}, \texttt{add\_\allowbreak{}val\_\allowbreak{}exactly\_\allowbreak{}one}, \texttt{not\_\allowbreak{}dvd\_\allowbreak{}of\_\allowbreak{}val\_\allowbreak{}one} & 8 \\ Main theorem (⟹ of (i)) & \texttt{quadratic\_\allowbreak{}value\_\allowbreak{}mem\_\allowbreak{}of\_\allowbreak{}entries\_\allowbreak{}mem} & 8 \\ \hline \end{longtable} \end{small} \textbf{How the main theorem appears there.} \texttt{regulator\_\allowbreak{}valuation\_\allowbreak{}of\_\allowbreak{}split\_\allowbreak{}anomalous} takes as hypotheses that the entries of the height matrix on Λ₀ are divisible by p and that det $M_{Λ₀}$ = p²·det $M_{Λ}$, and concludes $p^{r−2}$ ∣ det $M_{Λ}$; \texttt{regulator\_\allowbreak{}valuation\_\allowbreak{}of\_\allowbreak{}split\_\allowbreak{}anomalous\_\allowbreak{}iff\_\allowbreak{}split} takes the two halves — split ⟹ $Reg_p$ ∈ $Z_p$, and non-split ⟹ $Reg_p$ = z/p with p ∤ z — and turns them into the equivalence of (ii). That is, \textbf{integrality of the height matrix is a hypothesis there, not a conclusion}: what the kernel checks is the bookkeeping, and the geometry that produces the hypotheses is on paper. \textbf{Trust base.} \texttt{\#print\ \allowbreak{}axioms} is run at the end of each file on every theorem listed; every line reads \texttt{depends\ \allowbreak{}on\ \allowbreak{}axioms:} followed by a subset of [propext, Classical.choice, Quot.sound], and the logs are kept beside the sources. There is no \texttt{sorryAx} and no \texttt{Lean.\allowbreak{}ofReduceBool}, that is no \texttt{native\_\allowbreak{}decide}; no \texttt{decide} is load-bearing, and each file checks with exit code 0 and no warnings. \textbf{What is not in Lean.} The p-adic sigma function and the formula for $h_p$; the Iwasawa logarithm; division polynomials, their composition rule and their shape modulo p; Vélu's formulas and the degree count of Theorem C; [p] = V ∘ F and the group scheme E[p]; Serre–Tate theory; the Tate parametrisation and the valuations read off it; Deuring's lifting theorem; the structure of $E(Q_p)$ used in Lemma 4; the height pairing itself. So \textbf{the main theorem is not a Lean theorem}: what is machine-checked is the arithmetic skeleton along which its proof runs, and its grade is [paper]. \section*{7. What is open} \begin{enumerate} \item[1.] \textbf{The quadratic residue class of the slope.} Over every anomalous curve over $F_p$ with p ≤ 157 the slope ρ of §4.6 satisfies (ρ/p) = (−3/p), so that −3ρ is a square and $ρ(\bar{x})$ = $−3μ(\bar{x})²$ for a homomorphism μ : $E(F_p)$ → $F_p$ determined up to sign. This is [computation] and nothing more; μ has no closed form here. At the cusp $ρ_j$ ≈ 9j²/Δ, and the shape ρ = $9L(\bar{x})²/Δ$ with L a homomorphism is excluded by the residue class together with the squareness of −Δ. \item[2.] \textbf{One source under §4.6.} The step $"E^{(p)}$ is the member of the family at parameter $t^p"$ uses that the Tate parameter q, as a series in 1/j, has coefficients in the prime field. j(q) ∈ Z[[q]] is standard; the inverse series is what we did not locate in a source (§9), and [ATAEC] itself we did not retrieve. \item[3.] \textbf{Exact values rather than bounds.} Part (iii) is a lower bound, and the distribution of $v_p(Reg_p)$ inside \{0, 1, 2\} in the split boxes of §5.3 is not explained by anything here; nor is the behaviour at p = 5 with $\#E(F_5)$ = 10, which all statements after Lemma 4 exclude. \item[4.] \textbf{The geometry in Lean.} §6 lists what would have to exist in Mathlib for the main theorem to become a Lean theorem. \end{enumerate} \section*{8. What is not claimed} \begin{enumerate} \item[1.] \textbf{Nothing here bears on the conjecture of Birch and Swinnerton-Dyer}, nor on Ш, on L-functions or on the rank: every statement is about the valuation of a p-adic regulator under hypotheses on the reduction at one prime. Schneider's conjecture is not proved either; its CM case is [known], due to [Ber82], which we did not retrieve. \item[2.] \textbf{The baseline is not ours.} Theorem A is elementary and known (§9); what we add is the splitting hypothesis and its mechanism. \item[3.] \textbf{The local criterion is not ours.} The equivalence of Proposition 6 is [known] ([LR, Thm 4.1] for Gross's criterion, [DW, Lemma 3.2, Cor. 3.5]); we give an independent proof and a presentation through a Fermat quotient, and we do not give it a name. \item[4.] \textbf{The theorem is a lower bound in rank ≥ 2.} The exactness of §5.3 in the non-split case is Theorem S; in the split case nothing here predicts the value. Deuring's lifting theorem, Vélu's formulas, Serre–Tate theory, the composition rule for division polynomials, the coprimality of $φ_p$ and $ψ_p²$, and the Tate parametrisation are used as standard facts, and for the last we cite sources that quote [ATAEC] rather than [ATAEC] itself. \item[5.] \textbf{The hypotheses are as used, not the weakest possible.} Everything from Lemma 4 on assumes p ≥ 5 and $\#E(F_p)$ = p, so $\#E(F_5)$ = 10 lies outside, while Theorem A needs only p ∣ $\#E(F_p)$. \item[6.] \textbf{The computations are not kernel-checked, and the statistics are not statements.} All of §5 is PARI/GP with controls, at stated precision and over stated ranges; an earlier round used the height belonging to σ ≠ $σ_p$, and every count here has been recomputed with $h_p$. \item[7.] \textbf{No claim of priority, and no external review.} We searched [MST], [SW], [Har], [BMS], [BD], [Ban], [Wut], [BG], [LR], [DW], Sage's documentation and arXiv (§9): the baseline we found, the local criterion we found, the equivalence with integrality of the height matrix we did not, in a narrow search — no MathSciNet or zbMATH, and several primary sources not retrieved — so the statements may well be known. Observation, proofs, programs, Lean development and draft were produced by the same agent, and Lean's kernel, which covers §6 alone, is the only check not internal to the authors. \end{enumerate} \section*{9. Related work} \textbf{Where the baseline already is.} In the table of [MST, §4.2], for curves of rank 1 to 5, the entry for 37A at p = 53 is the only one of negative valuation, and the text notes there that $\#E(F_p)$ = p, "i.e., p is anomalous" — the phenomenon, with no bound stated and no index in sight. [Har] has the mechanism as an estimate: the working precision must be raised by 2 $v_p(n)$, n = $lcm(\#E(F_p)$, $lcm_{ℓ}$ $c_{ℓ}$), which is the "cost 2" of Theorem A as a loss of precision. [Ban, §2.2] uses the contrapositive as a hypothesis, non-anomalousness being what "extends the regulator estimate of Proposition 4.2 from E°(Q) to all of E(Q)", and that Proposition 4.2 is the positive half of Theorem A in rank two; Sage's \texttt{padic\_\allowbreak{}regulator} documents the same example. So the baseline is known to practitioners; we did not find it written as a proposition, and we do not need it to be new. \textbf{Where the local criterion already is.} Proposition 6 is the case n = 1 of Gross's tameness criterion, quoted as [LR, Thm 4.1]: for good ordinary reduction with E[p] irreducible, the decomposition group is diagonalisable modulo $p^{n+1}$ exactly when $j_E$ ≡ j₀ (mod $p^{n+1}$), with j₀ the j-invariant of the canonical lift, determined by the modular equation. It is also [DW, Lemma 3.2 and Cor. 3.5], where a prime with $E(Q_p)[p]$ ≠ 0 is a \textit{local torsion prime} and the criterion is that the lift to Z/p² be the canonical one — of the $p^d$ lifts exactly one has the larger p-rank — together with [DW, Prop. 2.1] for the fact that a local torsion prime is anomalous. The same statement circulates in cryptography, where the attacks on anomalous curves fail exactly for the lifts congruent to the canonical one modulo p². What we did not find is the criterion in the form $q_p(φ_p(x₀))$ = 0 — a Fermat quotient of a division polynomial at one point, which needs neither the j-invariant nor root-finding; the proof of §4.6 is independent of the sources above. Searches returning nothing on point (2026-09-24): \texttt{elliptic\ \allowbreak{}Wieferich\ \allowbreak{}prime}, \texttt{Fermat\ \allowbreak{}quotient\ \allowbreak{}elliptic\ \allowbreak{}curve}, \texttt{anomalous\ \allowbreak{}prime\ \allowbreak{}elliptic\ \allowbreak{}curve\ \allowbreak{}p-torsion}, \texttt{canonical\ \allowbreak{}lift\ \allowbreak{}p-torsion\ \allowbreak{}criterion\ \allowbreak{}mod\ \allowbreak{}p\textasciicircum{}2}. Near but different: the elliptic Wieferich primes of [Sil88] and [Vol] concern $N_p·P$ modulo p² for a rational point P, not rationality of the p-torsion, and the division-polynomial criteria of [Deb] are modulo p. \textbf{What we did not find} is the splitting hypothesis $E(Q_p)[p]$ ≠ 0 in connection with the valuation of $Reg_p$, or any statement that the height pairing is p-integral exactly under it. [SW] is our source for Schneider's conjecture; their §3.3 anomalous example is 446d1 at p = 5 with $\#E(F_5)$ = 10, the p = 5 case of §3.1, and its ord₅(Reg₅) is +1, not negative. The word "anomalous" does not occur in [BMS]. [Wut] studies the quantity e of §3.3 from the global side and [BG] the universal p-adic sigma function; [Kat] on Serre–Tate local moduli, the natural language for §4.6, we could not obtain. The nearest computation in the literature is [Ban] (2026), five rank-two CM curves at every good ordinary prime below 30,000 with a non-unit at 3 of 8,050 primes — the slice orthogonal to ours — which also formalises part of its argument in Lean 4. \begin{thebibliography}{XXXXX} \bibitem[ATAEC]{ATAEC} J. H. Silverman, \textit{Advanced Topics in the Arithmetic of Elliptic Curves}, GTM 151. [not retrieved; Thm V.5.3, Thm V.3.1, Prop. V.6.1 and Exercise V.5.13 are cited as quoted in [Ked] and [Sym]; the minimality of the Tate model and the integrality of the coefficients of q as a series in 1/j we could not attach to numbered statements] \bibitem[Ban]{Ban} B. S. Banwait, \textit{Second derivatives of p-adic L-functions and the Shafarevich–Tate group of rank-two CM elliptic curves}, arXiv:2609.08431 (2026). \bibitem[BMS]{BMS} J. S. Balakrishnan, J. S. Müller, W. A. Stein, \textit{A p-adic analogue of the conjecture of Birch and Swinnerton-Dyer for modular abelian varieties}, arXiv:1210.2739. \bibitem[Ber82]{Ber82} D. Bertrand, \textit{Valeurs de fonctions thêta et hauteurs p-adiques}, Progr. Math. \textbf{22}, Birkhäuser, 1982, 1–11. [not retrieved] \bibitem[BG]{BG} C. Blakestad, D. Grant, arXiv:1903.02480. \bibitem[BD]{BD} A. Burungale, D. Disegni, arXiv:1803.09268. \bibitem[Deb]{Deb} C. Debry, \textit{Beyond two criteria for supersingularity}, J. Théor. Nombres Bordeaux \textbf{26} (2014) 595–605. \bibitem[Dok]{Dok} T. Dokchitser, V. Dokchitser, \textit{Local invariants of isogenous elliptic curves}, arXiv:1208.5519, Thm A.1. \bibitem[DW]{DW} C. David, T. Weston, \textit{Local torsion on elliptic curves and the deformation theory of Galois representations}, arXiv:math/0701882. \bibitem[Har]{Har} D. Harvey, \textit{Efficient computation of p-adic heights}, arXiv:0708.3404. \bibitem[Kat]{Kat} N. Katz, \textit{Serre–Tate local moduli}. [not retrieved] \bibitem[Ked]{Ked} K. S. Kedlaya, \textit{The Tate curve}, lecture notes, MIT 18.727. [used only as a conduit for the statements of [ATAEC]] \bibitem[LR]{LR} Á. Lozano-Robledo, \textit{Division fields of elliptic curves with minimal ramification}, Rev. Mat. Iberoam. \textbf{31} (2015) 1311–1332; Thm 4.1 quotes B. Gross, Duke Math. J. (1990), §§14–15. \bibitem[Maz72]{Maz72} B. Mazur, Invent. Math. \textbf{18} (1972). [not retrieved; the source of "anomalous"] \bibitem[MST]{MST} B. Mazur, W. Stein, J. Tate, \textit{Computation of p-adic heights and log convergence}, Documenta Math. Extra Vol.: John H. Coates' Sixtieth Birthday (2006) 585–622. \bibitem[MT91]{MT91} B. Mazur, J. Tate, \textit{The p-adic sigma function}, Duke Math. J. \textbf{62} (1991) 663–688. [not retrieved] \bibitem[Sch]{Sch} P. Schneider, \textit{p-adic height pairings I, II} (1982, 1985). [not retrieved] \bibitem[Sil88]{Sil88} J. H. Silverman, \textit{Wieferich's criterion and the abc-conjecture}, J. Number Theory \textbf{30} (1988) 226–237. \bibitem[SW]{SW} W. Stein, C. Wuthrich, \textit{Algorithms for the arithmetic of elliptic curves using Iwasawa theory}, Math. Comp. \textbf{82} (2013) 1757–1792. \bibitem[Sym]{Sym} \textit{Symplectic criteria for elliptic curves, revisited}, arXiv:2509.19938, Prop. 2.2. [used only as a conduit for [ATAEC, Prop. V.6.1]] \bibitem[Vél]{Vl} J. Vélu, \textit{Isogénies entre courbes elliptiques} (1971). [not retrieved] \bibitem[Vol]{Vol} J. F. Voloch, J. Number Theory \textbf{81} (2000) 205–209. \bibitem[Wut]{Wut} C. Wuthrich, \textit{On p-adic elliptic logarithms and p-adic approximation lattices} (2006). \end{thebibliography} \noindent Software: PARI/GP 2.17.3 with \texttt{elldata} (Cremona's tables, conductor \textless{} 500000); Sage, \texttt{src/sage/schemes/elliptic\_\allowbreak{}curves/padics.\allowbreak{}py}, docstrings of \texttt{padic\_\allowbreak{}regulator} and \texttt{padic\_\allowbreak{}height}. \end{document}