\documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage{lmodern,amsmath,amssymb,amsthm,mathtools,microtype,xcolor} \usepackage[margin=1in]{geometry} \usepackage[colorlinks=true,linkcolor=blue!45!black,urlcolor=blue!45!black,citecolor=blue!45!black]{hyperref} \newtheorem{theorem}{Theorem} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{remark}\newtheorem*{remark}{Remark} \newcommand{\Q}{\mathbb Q}\newcommand{\F}{\mathbb F} \newcommand{\Z}{\mathbb Z}\newcommand{\one}{\mathbf1} \newcommand{\Gal}{\operatorname{Gal}}\newcommand{\Li}{\operatorname{Li}} \newcommand{\Nm}{\operatorname{N}}\newcommand{\rad}{\operatorname{rad}} \emergencystretch=2em \hypersetup{pdftitle={Cyclic reductions of elliptic curves at a positive proportion of primes},pdfauthor={Manjul Bhargava},pdfsubject={Cyclic reduction and a zero-free half-plane for Dedekind zeta functions}} \title{Cyclic reductions of elliptic curves\\at a positive proportion of primes} \author{Manjul Bhargava\\Princeton University} \date{24 October 2026} \begin{document} \maketitle \begin{abstract} We prove that every elliptic curve over $\Q$ whose points of order two are not all rational has cyclic reduction at a positive lower density of primes. This is the only necessary restriction: full rational two-torsion prevents cyclic reduction at every odd prime of good reduction. More precisely, a common zero-free half-plane $\Re s>1-1/N$ for Dedekind zeta functions gives a lower proportion of at least $c_E/(N\log N)$, with $c_E>0$ independent of $N$; the theorem of Cureton and Thorner supplies $N=32$. The proof uses the varying-cofactor sieve of our earlier works on primitive roots and primitive points, in conjunction with the marked Type~II estimates of~OpenAI, to construct candidate primes. We then apply a smoothed explicit formula for Dedekind zeta functions, with nonnegative weights on prime ideals, to bound the number of candidates with noncyclic reduction. This gives a common argument for CM and non-CM curves. \end{abstract} \section{Introduction}\label{sec:intro} In this article, we prove the following theorem. \begin{theorem}\label{thm:main} Let $E/\Q$ be an elliptic curve whose points of order two are not all rational. Then there exists a positive lower proportion of primes $p$ such that $E(\F_p)$ is cyclic. \end{theorem} \noindent More precisely, let \[ C_E(X)=\#\{p\le X:p\text{ of good reduction for }E,\ E(\F_p)\text{ cyclic}\}. \] Then Theorem~\ref{thm:main} states that \begin{equation}\label{eq:positive-density} \liminf_{X\to\infty}\frac{C_E(X)}{\pi(X)}>0. \end{equation} The hypothesis in Theorem~\ref{thm:main} is necessary. If all the points of order two are rational, then at every odd prime of good reduction the group $E(\F_p)$ contains a subgroup isomorphic to $(\Z/2\Z)^2$, and so is not cyclic. Thus Theorem~\ref{thm:main} gives a necessary and sufficient condition for an elliptic curve over $\Q$ to have cyclic reduction at a positive lower proportion of primes. The study of cyclic reductions of elliptic curves over $\Q$ was initiated in the suggestive numerical investigations of Borosh, Moreno, and Porta~\cite{bmp}. A precise density prediction was given by Serre, who stated it in an equivalent Galois-theoretic form in his 1977--1978 course summary~\cite[pp.~67--68]{serre-courses}. For each integer $m\ge1$, let $K_m=\Q(E[m])$ be the field generated by the coordinates of the $m$-torsion points of $E$; then Serre predicted that \begin{equation}\label{eq:expected} C_E(X)\sim\delta_E\Li(X),\qquad \delta_E=\sum_{m\ge1}\frac{\mu(m)}{[K_m:\Q]}, \end{equation} when $K_2\ne\Q$, where $\Li(X)=\int_2^Xdt/\log t$; see also~\cite[Sections~2, 3, and 5]{murty}. %The degrees in this sum retain the intersections among the division fields. Adapting Hooley's proof of Artin's conjecture under the generalized Riemann hypothesis~\cite{hooley}, Serre established this cyclicity asymptotic under GRH and observed that the density $\delta_E$ is positive precisely when $K_2\ne\Q$. A proof was published by Murty~\cite[Section~5]{murty}. Cojocaru and Murty~\cite{cojocaru-murty} later obtained sharper error terms in this conditional asymptotic. For curves with complex multiplication, Murty~\cite{murty} removed the GRH assumption, using the class field theory of CM curves and a number-field version of the Bombieri--Vinogradov theorem. Cojocaru~\cite{cojocaru} subsequently gave an even simpler proof with explicit error terms. Thus the positive-proportion conclusion was already known in the CM case. %Theorem~\ref{thm:main} is new for curves without complex multiplication, for which no unconditional positive-proportion result was previously known. For general elliptic curves, Gupta and Murty~\cite{gm} proved that cyclic reduction occurs at infinitely many primes whenever $K_2\ne\Q$. More precisely, their theorem gives the unconditional lower bound \[ C_E(X)\gg_E\frac{X}{(\log X)^2}. \] For non-CM curves, Cojocaru~\cite[Theorem~1.2]{cojocaru-qrh} proved that the asymptotic~\eqref{eq:expected} follows from the weaker hypothesis that the Dedekind zeta functions of $K_m$, for squarefree $m$, have no zeros in $\Re s>3/4$. The zero-free region available to us from Cureton and Thorner~\cite{ct} is $\Re s>31/32$, which is weaker and does not supply the hypothesis used by Cojocaru. Our purpose is to obtain the positive-proportion lower bound~\eqref{eq:positive-density} for every curve with $K_2\ne\Q$ using this narrower zero-free region. The analytic framework comes from our earlier works on Artin's primitive root problem~\cite{artin} and on primitive points on elliptic curves~\cite{primitive}. The varying-cofactor sieve developed there, using the marked Type~II estimates of OpenAI~\cite{pd,openai}, produces primes whose predecessor has the form \begin{equation}\label{eq:strategy-factorization} p-1=crQ,\qquad r\le x^\epsilon,\qquad Q>x^{0.9}\text{ prime}, \qquad q\mid r\Longrightarrow q>Y, \end{equation} where $x0$ and $Y$ are fixed before $x$ tends to infinity. In a suitable fixed arithmetic progression, the number of these primes is at least a constant times \[ \frac{\epsilon}{\log Y}\frac{x}{\log x}. \] Allowing the cofactor $r$ to vary supplies the additional logarithm needed for a positive proportion. The uniformity in $\epsilon$ and $Y$ will also be important. To use these primes, recall that $E(\F_p)$ fails to be cyclic precisely when $p$ splits completely in $K_\ell$ for some prime $\ell\ne p$. Such an $\ell$ divides $p-1$ and satisfies $\ell^2\mid\#E(\F_p)$. We choose the progression to exclude complete splitting in $K_2$. Hasse's bound excludes the distinguished large prime $Q$ in~\eqref{eq:strategy-factorization}. Every remaining obstruction therefore comes from a prime \[ Y<\ell\le x^\epsilon. \] This observation makes the predecessor $p-1$ useful for arbitrary elliptic curves, even though their group orders need not have any fixed form. The degree of $K_\ell$ is $\gg_E\ell^2$, and its logarithmic root discriminant is $\ll_E\log\ell$. We apply the explicit formula for its Dedekind zeta function with a nonnegative smooth weight that is at least one on the interval being counted. Every completely split prime $p$ in this interval contributes at least $[K_\ell:\Q]\log p$ to the resulting nonnegative sum, so a zero-free half-plane gives an upper bound for the number of such primes. We count these exceptional primes among all primes and subtract them from the candidate set. Thus the argument needs no joint distribution statement for the cofactor condition and the division fields. Both the cofactor construction and this smoothed prime-ideal bound are taken from~\cite{primitive}; we give the predecessor version of the construction and the division-field deduction explicitly. We retain the width of the zero-free half-plane as a parameter in order to make its effect on the lower bound explicit. The quantitative result from which Theorem~\ref{thm:main} follows is the following. \begin{theorem}\label{thm:quantitative} Let $E/\Q$ be an elliptic curve with $\Q(E[2])\ne\Q$. Suppose that, for some fixed real $N\ge2$, every Dedekind zeta function has no zeros in the half-plane \begin{equation}\label{eq:zerofree} \Re s>1-\frac1N. \end{equation} Then there is a constant $c_E>0$, depending only on $E$ and independent of $N$, such that \begin{equation}\label{eq:quantitative} C_E(2x)-C_E(x)\ge\frac{c_E}{N\log N}\frac{x}{\log x} \end{equation} for all sufficiently large $x$. The threshold may depend on $E$ and $N$, but $c_E$ does not depend on $N$. After decreasing $c_E$ if necessary, we also have \begin{equation}\label{eq:quantitative-density} \liminf_{X\to\infty}\frac{C_E(X)}{\pi(X)}\ge\frac{c_E}{N\log N}. \end{equation} \end{theorem} Cureton and Thorner~\cite[Theorem~1.1]{ct} prove that every Dedekind zeta function has no zeros in $\Re s>31/32$. Their theorem therefore supplies $N=32$ in Theorem~\ref{thm:quantitative}. This paper is organized as follows. In Section~\ref{sec:arithmetic}, we recall the division-field criterion for cyclicity and construct the required arithmetic progression. In Section~\ref{sec:candidates}, we deduce the prime-predecessor estimate from the cofactor sieve of~\cite{primitive}, recording the changes of sign and the required uniformity. In Section~\ref{sec:splitting}, we establish the division-field bounds and apply the smoothed prime-ideal bound to count completely split primes. Finally, in Section~\ref{sec:proof}, we remove the remaining obstructions and prove Theorems~\ref{thm:main} and~\ref{thm:quantitative}. \medskip \noindent {\it Notation.} Throughout the paper, the letters $p,q,\ell$ denote rational primes unless otherwise specified. We use $P^-(r)$ for the least prime divisor of an integer $r>1$, and set $P^-(1)=\infty$. All constants allowed to depend on $E$ may also depend on the fixed progression chosen for $E$. The parameters $N$, $\epsilon$, and $Y$ are fixed before $x$ tends to infinity. \section{Cyclicity and a fixed arithmetic progression}\label{sec:arithmetic} We begin with the standard criterion that connects cyclic reduction to complete splitting. Let $R_E$ denote the product of the primes of bad reduction of $E$. \begin{lemma}\label{lem:cyclicity} Let $p\ge3$ be a prime of good reduction for $E$. The group $E(\F_p)$ is noncyclic if and only if $p$ splits completely in $K_\ell=\Q(E[\ell])$ for some prime $\ell\ne p$. Every such $\ell$ satisfies \begin{equation}\label{eq:obstruction} \ell\mid p-1,\qquad \ell^2\mid\#E(\F_p),\qquad \ell\le\sqrt p+1. \end{equation} \end{lemma} \begin{proof} A noncyclic finite abelian group contains a subgroup isomorphic to $(\Z/\ell\Z)^2$ for some prime~$\ell$. Hasse's bound gives \[ \#E(\F_p)\le(\sqrt p+1)^20$, $\epsilon_0>0$, and $Y_0\ge3$, depending only on this fixed progression, with the following property. For every fixed $0<\epsilon<\epsilon_0$ and $Y\ge Y_0$, the set \begin{equation}\label{eq:candidate-set} \mathcal C(x;\epsilon,Y)=\{xx^{0.9}\;\mbox{\em prime},\;\,P^-(r)>Y\} \end{equation} satisfies \begin{equation}\label{eq:candidate-bound} \#\mathcal C(x;\epsilon,Y)\ge A\frac{\epsilon}{\log Y}\frac{x}{\log x} \end{equation} for all sufficiently large $x$. The threshold may depend on $\epsilon$ and $Y$, but $A$, $\epsilon_0$, and $Y_0$ do not. \end{proposition} \begin{proof} Proposition~4 of~\cite{primitive} is the corresponding statement for prime successors, with $p+1=crQ$ and $u+1$ in the progression conditions. We record the changes in its proof, which is given in Section~3 of that paper. Use the same family of cofactors, marked weight $\mathcal W$, and invariant selector $F_x$. If $\mathcal P$ is the set of marked primes and $h_{\mathcal P}$ is the largest divisor of $h$ supported on $\mathcal P$, the selector has the form \[ F_x(h)=\one_{\{h/h_{\mathcal P}=cr_0Q\text{ for some }r_0\in\mathcal R_x, \ Q>x^{0.9}\text{ prime}\}}, \] where $\mathcal R_x$ is the cofactor family constructed there. In particular, $F_x(\ell h)=F_x(h)$ for every marked prime $\ell$, including when $\ell\mid h$. Replace the weight on integers $d$ by \begin{equation}\label{eq:predecessor-weight} w(d)=\one_{d\equiv u\ (M)}\Psi(d/x)F_x(d-1)\mathcal W(d-1), \end{equation} where $0\le\Psi\le1$ is smooth, supported in $(1,2)$, and has $\int\Psi>0$. On its support, $d=crQ+1$, in place of $crQ-1$. The required marked replacement is~\cite[Proposition~5]{primitive} with $\sigma=1$, the original sign in~\cite{pd,openai}. Its constants are uniform over the invariant selectors and all dyadic intervals in the fixed exponent ranges used in the sieve. Put $M_0=M/c$. The progression for the prime variable $Q$ becomes \begin{equation}\label{eq:q-progression} Q\equiv ((u-1)/c)r^{-1}\pmod{M_0}. \end{equation} Take $Y_0$ larger than every prime divisor of $M$. Then $(r,M)=1$, and~\eqref{eq:q-progression} is a reduced residue class. For an odd prime $\ell\nmid Mr$, the condition $\ell\mid crQ+1$ excludes the single nonzero residue $Q\equiv-(cr)^{-1}\pmod\ell$. If $\ell\mid Mr$, no permitted residue is excluded. Thus the multiplicative sieve density remains \begin{equation}\label{eq:sieve-density} g_r(d)=\frac{\one_{(d,Mr)=1}}{\varphi(d)} \qquad(d\text{ odd and squarefree}). \end{equation} The distribution estimate of~\cite[Lemma~7]{primitive} follows unchanged from Bombieri--Vinogradov, which is uniform over reduced residue classes. The smooth main integral has $\log((xy-1)/(cr))$ in place of $\log((xy+1)/(cr))$ in its denominator; all comparisons used there are identical. In the rough-pair estimate of~\cite[Lemma~8]{primitive}, the congruence is now $mn\equiv1\pmod{cr}$, which has $\varphi(cr)$ solutions in pairs of residue classes. At an odd sieving prime $\ell\nmid cr$, the conditions $mn\equiv1\pmod\ell$ and $mn\equiv0\pmod\ell$ have, respectively, $\ell-1$ and $2\ell-1$ solutions, and these sets are disjoint. Hence the local counts and the resulting bound are unchanged, including the independence of its constant from the number of marked groups. The cofactor mass and tail estimates involve only the factorization of $d-1$ and are otherwise the same. Their full harmonic mass is $\gg_K\epsilon\log x/\log Y$, where $K$ is the number of marked groups. The cutoff $r\le x^\epsilon$ is imposed by discarding the negligible tail after the marked estimates; it is not inserted into $F_x$, since doing so would destroy its invariance. The block sieve, Buchstab subtraction, and removal of the remaining semiprimes therefore give the same lower bound as in~\cite[Proposition~4]{primitive}. As in the last subsection of its Section~3, first fix all sieve parameters and $K$ using only the progression, and then choose $\epsilon$ and $Y$. The boundedness of the marked weights converts the weighted lower bound into~\eqref{eq:candidate-bound}, with a constant independent of these two parameters. \end{proof} The proof uses only the analytic estimates and cofactor construction of~\cite{primitive}; the elliptic curve and rational point considered there play no role in Proposition~\ref{prop:candidates}. In particular, the proposition applies to the progression of Lemma~\ref{lem:progression} for an arbitrary elliptic curve satisfying $K_2\ne\Q$. \section{Completely split primes in division fields}\label{sec:splitting} For a prime $\ell$, put \[ n_\ell=[K_\ell:\Q],\qquad D_\ell=|\operatorname{disc}(K_\ell)|. \] The following familiar bounds allow us to treat CM and non-CM curves together. \begin{lemma}\label{lem:fields} For every prime $\ell$, \begin{equation}\label{eq:field-bounds} n_\ell\gg_E\ell^2,\qquad \frac{\log D_\ell}{n_\ell}\ll_E\log(2\ell). \end{equation} \end{lemma} \begin{proof} If $E$ has no complex multiplication, Serre's open image theorem~\cite[Th\'eor\`eme~2]{serre-open} gives \[ \Gal(K_\ell/\Q)=\mathrm{GL}_2(\F_\ell) \] for all sufficiently large $\ell$. Hence $n_\ell\asymp\ell^4$ in this case. If $E$ has complex multiplication by an order $\mathcal O$ in an imaginary quadratic field $F$, the main theorem of complex multiplication gives an image of bounded index, depending only on $E$, in $(\mathcal O/\ell\mathcal O)^\times$ over $F$; see~\cite[Chapter~II]{silverman-advanced}. Outside a fixed finite set of primes, this group has order $(\ell-1)^2$ or $\ell^2-1$. Since \[ [F(E[\ell]):F]=[K_\ell:K_\ell\cap F]\le n_\ell, \] we obtain $n_\ell\gg_E\ell^2$. Enlarging the implied constant accommodates the finitely many remaining primes in either case. For the discriminant, the N\'eron--Ogg--Shafarevich criterion gives \[ \rad(D_\ell)\mid\ell R_E, \] and the faithful action on $E[\ell]$ gives $n_\ell\le|\mathrm{GL}_2(\F_\ell)|<\ell^4$. The general discriminant bound for a Galois extension~\cite[Proposition~6]{serre-chebotarev} is \[ \log D_\ell\le(n_\ell-1)\log\rad(D_\ell)+n_\ell\log n_\ell. \] Consequently, \[ \frac{\log D_\ell}{n_\ell}\le\log R_E+5\log\ell, \] which proves the second bound. \end{proof} We next recall the consequence of the smoothed explicit formula needed here. For a number field $T$, let $\Lambda_T$ be the von Mangoldt function on its nonzero integral ideals: $\Lambda_T(\mathfrak p^j)=\log\Nm\mathfrak p$ for a prime ideal $\mathfrak p$ and $j\ge1$, and $\Lambda_T$ is zero otherwise. We choose a nonnegative smooth weight, so that discarding unwanted prime ideals can only decrease the sum. \begin{lemma}[Smoothed prime-ideal bound]\label{lem:explicit} Let $T$ be a number field of degree $n$ and absolute discriminant $D_T$. Suppose that all nontrivial zeros of $\zeta_T$ have real part at most $1-\delta$, where $0<\delta\le1/2$. Fix a nonnegative smooth function $f$ supported in $(1/2,3)$ and at least one on $[1,2]$. Then \begin{equation}\label{eq:explicit} \sum_{\mathfrak a}\Lambda_T(\mathfrak a)f(\Nm\mathfrak a/x) \ll_f x+x^{1-\delta}(\log D_T+n) \qquad(x\ge2), \end{equation} with an implied constant independent of $T$ and $\delta$. \end{lemma} \begin{proof} This is~\cite[Lemma~10]{primitive}. We recall why its uniformity does not cost a factor depending on $1/\delta$. If $\widehat f$ is the Mellin transform of $f$, the smoothed explicit formula gives a pole term $x\widehat f(1)$, a zero term \[ -\sum_\rho x^\rho\widehat f(\rho), \] and a remaining contribution $O_f(\log D_T+n)$ for $x\ge2$. Smoothness and the usual zero count give \[ \sum_\rho|\widehat f(\rho)|\ll_f\log D_T+n. \] The zero-free hypothesis bounds each $|x^\rho|$ by $x^{1-\delta}$, proving~\eqref{eq:explicit} with the asserted uniformity. \end{proof} \begin{proposition}\label{prop:split} Let $N\ge2$ be real, and suppose that every Dedekind zeta function has no zeros in $\Re s>1-1/N$. Let \[ B_\ell(x)=\#\{xY}\frac1{\ell^2}\ll\frac1{Y\log Y}, \qquad \sum_{\ell\le z}\log(2\ell)\ll z \] give~\eqref{eq:split-sum}. The first follows by partial summation from $\pi(t)\ll t/\log t$, and the second is Chebyshev's bound. \end{proof} The factor $n_\ell$ contributed by a completely split prime is essential: it leaves only the logarithmic root discriminant in the error term. We have used the explicit formula for the Dedekind zeta function itself, so no separate effective Chebotarev theorem is required. \section{Proof of the main theorems}\label{sec:proof} Let $E/\Q$ satisfy $K_2\ne\Q$, and fix the progression of Lemma~\ref{lem:progression}. We may decrease $\epsilon_0$ in Proposition~\ref{prop:candidates} so that $\epsilon_0<1/10$. Fix, for the moment, $0<\epsilon<\epsilon_0$ and $Y\ge Y_0$. Suppose $p\in\mathcal C(x;\epsilon,Y)$ and $E(\F_p)$ is noncyclic. By Lemma~\ref{lem:cyclicity}, $p$ splits completely in $K_\ell$ for some prime $\ell\ne p$ satisfying~\eqref{eq:obstruction}. The progression excludes $\ell=2$. Since \[ \ell\mid p-1=crQ \] and $c$ is a power of two, either $\ell\mid r$ or $\ell=Q$. For all sufficiently large $x$, the latter is impossible, because \[ Q>x^{0.9}>\sqrt{2x}+1\ge\sqrt p+1. \] Thus $\ell\mid r$ and \begin{equation}\label{eq:short-obstructions} Y<\ell\le r\le x^\epsilon. \end{equation} Suppose that every Dedekind zeta function has no zeros in $\Re s>1-1/N$, for a fixed real $N\ge2$. Proposition~\ref{prop:split} therefore shows that the number of noncyclic candidates is at most \begin{equation}\label{eq:bad-candidates} C_1\frac{x}{Y\log Y\log x} +C_2\frac{x^{1-1/N+\epsilon}}{\log x}, \end{equation} where $C_1,C_2$ depend only on $E$. Combining~\eqref{eq:candidate-bound} and~\eqref{eq:bad-candidates}, we obtain \begin{equation}\label{eq:before-choice} C_E(2x)-C_E(x)\ge \left(\frac{A\epsilon}{\log Y}-\frac{C_1}{Y\log Y} -C_2x^{-1/N+\epsilon}\right)\frac{x}{\log x} \end{equation} for all sufficiently large $x$, with the threshold permitted to depend on the fixed parameters. We now choose these parameters, keeping the dependence on $N$ explicit. Fix \[ 0<\alpha<\min(1,2\epsilon_0) \] and then fix $B\ge2$, depending only on $E$, so large that \[ 2B\ge Y_0,\qquad \frac{C_1}{B}\le\frac{A\alpha}{4}. \] For each fixed $N\ge2$, put \begin{equation}\label{eq:choice} \epsilon=\frac{\alpha}{N},\qquad Y=BN. \end{equation} These choices are admissible in Proposition~\ref{prop:candidates}. The second term in parentheses in~\eqref{eq:before-choice} is at most one quarter of the first. Moreover, \[ x^{-1/N+\epsilon}=x^{-(1-\alpha)/N}\longrightarrow0 \qquad(x\to\infty), \] so for all sufficiently large $x$ the third term is also at most one quarter of the first. We conclude that \begin{equation}\label{eq:after-choice} C_E(2x)-C_E(x)\ge \frac{A\alpha}{2N\log(BN)}\frac{x}{\log x}. \end{equation} Since $N\ge2$, \[ \log(BN)\le\left(1+\frac{\log B}{\log2}\right)\log N. \] The constant \[ d_E=\frac{A\alpha}{2(1+\log B/\log2)}>0 \] is independent of $N$, and~\eqref{eq:after-choice} proves~\eqref{eq:quantitative} with $d_E$ in place of $c_E$. For the lower proportion, apply this bound with $x=X/2$ and use the prime number theorem. It gives \[ \liminf_{X\to\infty}\frac{C_E(X)}{\pi(X)} \ge\frac{d_E}{2N\log N}. \] Taking $c_E=d_E/2$ proves both assertions of Theorem~\ref{thm:quantitative}. The zero-free half-plane $\Re s>31/32$ of Cureton and Thorner now proves Theorem~\ref{thm:main}. The argument isolates a set of primes on which every obstruction to cyclicity lies in the short range~\eqref{eq:short-obstructions}. It does not evaluate the full inclusion-exclusion sum in~\eqref{eq:expected}, or prove an asymptotic with that constant. Its conclusion is a positive lower proportion, uniformly expressed in terms of the available zero-free width. \paragraph{Formal verification.} The accompanying Lean development verifies the positive-proportion argument for integral Weierstrass models of elliptic curves from explicit analytic and arithmetic inputs. It proves the construction of the fixed progression and shows that, among the candidate primes, every obstruction to cyclicity---a subgroup $(\mathbb Z/\ell\mathbb Z)^2$ in $E(\mathbb F_p)$, corresponding to complete splitting in $K_\ell$---has $Y<\ell\le x^\epsilon$. The bound for these exceptional primes, their subtraction, and the final parameter choice are proved within the development. The formal theorem gives $c_E/(N\log N)$, with $c_E>0$ chosen before $N$, including the lower-proportion conclusion and its specialization to~$N=32$. The analytic inputs are the zero-free hypothesis supplied by~\cite{ct}, the candidate-prime estimate from~\cite{artin,primitive}, the prime number theorem, the elementary prime-sum estimates, and the smoothed prime-ideal bound of Lemma~\ref{lem:explicit}. The last bound is proved in~\cite[Lemma~10]{primitive} from Mellin inversion, the Dedekind zeta functional equation, and the standard zero count, with a constant independent of the field and the zero-free width. It is an explicit hypothesis in Lean because that analytic derivation has not been formalized. The arithmetic inputs are standard facts about torsion, reduction, and division fields. These inputs are supplied as explicit hypotheses; Lean checks the deductions from them. The development records its assumptions and references explicitly, and its completed build has no proof placeholders or added global axioms. The Lean sources for \cite{artin}, \cite{primitive}, and the current article are available at \url{https://github.com/bhargavamanjul/FormalizedProofs/} . \subsection*{Acknowledgments} I thank Peter Sarnak, Paul Pollack, and Jesse Thorner for helpful conversations. GPT-6 was used to help write and formalize the arguments. The author was supported by the National Science Foundation (Grant DMS-1001828). \begin{thebibliography}{99} \bibitem{artin} M. Bhargava, Every nonsquare integer not equal to $-1$ is a primitive root modulo a positive lower density of primes, Hexagon preprint 2610.00228v1, October 2026. \href{https://hexagonmath.org/2610.00228v1}{Preprint}. \bibitem{primitive} M. Bhargava, Rational points on elliptic curves that are primitive modulo a positive proportion of primes, Hexagon preprint 2610.00294v1, October 2026. \href{https://hexagonmath.org/2610.00294v1}{Preprint}. \bibitem{bmp} I. Borosh, C. J. Moreno, and H. Porta, Elliptic curves over finite fields. II, \emph{Math. Comp.} \textbf{29} (1975), no.~131, 951--964. \href{https://www.ams.org/journals/mcom/1975-29-131/S0025-5718-1975-0404264-3/}{Article}. \bibitem{cojocaru-qrh} A. C. Cojocaru, On the cyclicity of the group of $\F_p$-rational points of non-CM elliptic curves, \emph{J. Number Theory} \textbf{96} (2002), no.~2, 335--350. \href{https://doi.org/10.1006/jnth.2002.2789}{doi:10.1006/jnth.2002.2789}. \bibitem{cojocaru} A. C. Cojocaru, Cyclicity of CM elliptic curves modulo $p$, \emph{Trans. Amer. Math. Soc.} \textbf{355} (2003), no.~7, 2651--2662. \href{https://doi.org/10.1090/S0002-9947-03-03283-5}{doi:10.1090/S0002-9947-03-03283-5}. \bibitem{cojocaru-murty} A. C. Cojocaru and M. Ram Murty, Cyclicity of elliptic curves modulo $p$ and elliptic curve analogues of Linnik's problem, \emph{Math. Ann.} \textbf{330} (2004), no.~3, 601--625. \href{https://doi.org/10.1007/s00208-004-0562-x}{doi:10.1007/s00208-004-0562-x}. \bibitem{ct} D. Cureton and J. Thorner, A quasi-Riemann hypothesis for Dedekind zeta functions, Hexagon preprint 2610.00200v2, October 2026. \href{https://hexagonmath.org/2610.00200v2}{Preprint}. \bibitem{gm} R. Gupta and M. Ram Murty, Cyclicity and generation of points mod $p$ on elliptic curves, \emph{Invent. Math.} \textbf{101} (1990), no.~1, 225--235. \href{https://doi.org/10.1007/BF01231502}{doi:10.1007/BF01231502}. \bibitem{hooley} C. Hooley, On Artin's conjecture, \emph{J. Reine Angew. Math.} \textbf{225} (1967), 209--220. \bibitem{murty} M. Ram Murty, On Artin's conjecture, \emph{J. Number Theory} \textbf{16} (1983), no.~2, 147--168. \href{https://doi.org/10.1016/0022-314X(83)90039-2}{doi:10.1016/0022-314X(83)90039-2}. \bibitem{pd} OpenAI, The Poisson--Dirichlet law for prime predecessors, preprint, 24 September 2026, Theorem~3.1 and Sections~3--5; version consulted: repository commit \texttt{1581d4cbdd69}. \href{https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026/paper.pdf}{Preprint}. \bibitem{openai} OpenAI, Primitive roots for every admissible integer base, preprint, 4 October 2026, Lemma~10.2, Proposition~10.3, and Section~12; version consulted: repository commit \texttt{1581d4cbdd69}. \href{https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Primitive-roots-for-every-admissible-integer-base-October-4-2026/primitive-roots-all-integer-bases.pdf}{Preprint}. \bibitem{serre-open} J.-P. Serre, Propri\'et\'es galoisiennes des points d'ordre fini des courbes elliptiques, \emph{Invent. Math.} \textbf{15} (1972), 259--331. \href{https://doi.org/10.1007/BF01405086}{doi:10.1007/BF01405086}. \bibitem{serre-courses} J.-P. Serre, R\'esum\'e des cours de 1977--1978, \emph{Annuaire du Coll\`ege de France} (1978), 67--70. \href{https://www.college-de-france.fr/sites/default/files/media/document/2023-03/1977-1978_serre.pdf}{Original course summary}. \bibitem{serre-chebotarev} J.-P. Serre, Quelques applications du th\'eor\`eme de densit\'e de Chebotarev, \emph{Publ. Math. IHES} \textbf{54} (1981), 123--201. \href{https://www.numdam.org/item/PMIHES_1981__54__123_0/}{Numdam}. \bibitem{silverman} J. H. Silverman, \emph{The Arithmetic of Elliptic Curves}, second edition, Graduate Texts in Mathematics \textbf{106}, Springer, 2009. \bibitem{silverman-advanced} J. H. Silverman, \emph{Advanced Topics in the Arithmetic of Elliptic Curves}, Graduate Texts in Mathematics \textbf{151}, Springer, 1994. \end{thebibliography} \end{document}