Birch and Swinnerton-Dyer Conjecture

Birch and Swinnerton-Dyer Conjecture

OpenAI's claim

Mathematical statement of the claimed result

Manuscript 1.

Manuscript 2.

Manuscript 3.

Manuscript 4.

Manuscript 5.

Manuscript 6.

Outline of the argument

For manuscript 3 (family 002; 2026-09-24), the proof compares integral determinant lattices with Siegel-unit periods and central Kummer lattices. Separate residual and character-division arguments establish primitivity at two, and the rank-one comparison uses a squared Heegner logarithm rather than only rational period identities. For manuscript 4 (family 004; 2026-09-24), binary coefficient systems detect central values or Heegner points. Integral interpolation and arithmetic contraction identities isolate one address in a network of twists, transferring a nonvanishing witness back to the original curve.

For manuscript 5 (family 006; 2026-09-23), finite cubes of twists preserve the required local classes. A central determinant or Heegner coordinate is nonzero at the noncentral cube vertices, and bounded integral interpolation recovers the missing vertex; the Selmer distribution then supplies the density assertion. For manuscript 6 (family 006; 2026-09-23), block mollifiers compare twist families with a finite independent model. Poisson summation and an auxiliary square multiplier send dual twists to smaller height, allowing induction on logarithmic second moments and control of the contribution from large ranks.

Formal verification

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

Sources

• OpenAI, Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank, 2026-10-03; citation key OAI:Exact-Birch-Swinnerton-Dyer-Formula-from-Low-Selmer-Corank-October-3-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main, eq:bsd-main.
• OpenAI, The Selmer converse for elliptic curves at every prime, 2026-09-24; citation key OAI:The-Selmer-converse-for-elliptic-curves-at-every-prime-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI, The two-primary Birch–Swinnerton-Dyer formula in Selmer corank at most one, 2026-09-24; citation key OAI:The-two-primary-Birch-Swinnerton-Dyer-formula-in-Selmer-corank-at-most-one-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI, A pointwise 2-converse for elliptic curves with rational two-torsion, 2026-09-24; citation key OAI:A-pointwise-2-converse-for-elliptic-curves-with-rational-two-torsion-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI, Goldfeld's analytic density conjecture and the 2-converse for elliptic curves, 2026-09-23; citation key OAI:Goldfelds-analytic-density-conjecture-and-the-2-converse-for-elliptic-curves-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main-converse.
• OpenAI, The mean analytic rank of quadratic twists of elliptic curves, 2026-09-23; citation key OAI:The-mean-analytic-rank-of-quadratic-twists-of-elliptic-curves-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:mean.
• OpenAI catalogue entry.

Birch and Swinnerton-Dyer Conjecture

Definitions and mathematical statement

Formulation and concept references: [S1], [E1].

Short English statement

Research attempt

Scope and source checkpoint.

The attempted route is to construct two independent certificates, one algebraic and one analytic, and ask what would make the procedure terminate in arbitrary rank. It yields explicit inequalities and an exact conditional certificate. It also exposes two reasons why extending successful low-rank computations is not a general proof. Standard descent, height and modular form inputs are taken from [E2], Chapters IV and V; the estimates below are derived here.

Algebraic side: isolate the descent defect.

Suppose $P_1,\ldots,P_R$ are rational points with a positive definite Néron--Tate Gram matrix. A rational linear dependence modulo torsion would have canonical height zero and contradict positive definiteness. Hence \begin{equation}\label{wsref-0-63-6f-6e-74-36-3a-73-61-6e-64-77-69-63-68} R\le r\le s_\ell-t_\ell. \end{equation} In particular, equality of the two computed endpoints proves $r=R$. This needs no assertion that the supplied points generate the entire Mordell--Weil group; finite index does not change rank. Conversely, a finite point search with no additional points does not prove the lower endpoint is the rank. Certified height intervals can prove independence if they certify positive definiteness, but an approximate positive determinant without error bounds is not such a certificate.

Analytic side: a rapidly convergent central expansion.

An explicit truncation bound.

Let $D_{k,M}$ be the sum in (cont6:derivative) truncated to $n\le M$, including its parity factor. Since $\log t\le t$ for $t\ge1$, repeated integration by parts gives the rigorous bound \begin{align} |\Lambda_E^{(k)}(1)-D_{k,M}| &\le 2\sum_{n>M}n^2\int_1^\infty e^{-cnt}t^k\,dt\\ &=2k!\sum_{n>M}n^2e^{-cn} \sum_{j=0}^{k}\frac{1}{(k-j)!(cn)^{j+1}}. \label{wsref-0-63-6f-6e-74-36-3a-74-61-69-6c} \end{align} This is already an explicit convergent majorant. A simpler closed upper bound follows from $n\ge1$. Set $q=e^{-c}$ and $C_k(c)=2k!\sum_{j=0}^k((k-j)!c^{j+1})^{-1}$. Then \begin{equation}\label{wsref-0-63-6f-6e-74-36-3a-63-6c-6f-73-65-64-74-61-69-6c} |\Lambda_E^{(k)}(1)-D_{k,M}| \le C_k(c)q^{M+1} \left(\frac{M+1}{1-q}+\frac{q}{(1-q)^2}\right). \end{equation} Indeed $n^2/n^{j+1}=n^{1-j}\le n$, and the remaining series is $\sum_{n>M}nq^n$. No unspecified implied constant depends on the curve or on the truncation. For large conductor the bound can be slow because $c$ is small, but it still tends to zero for each fixed $N,k$.

If certified quadrature and rounding enclose $D_{k,M}$ in an interval $I$, enlarging $I$ by the bound in (cont6:closedtail) gives a certified enclosure of the derivative. An interval excluding zero proves nonvanishing. It is essential to include quadrature and rounding errors, in addition to the Fourier-tail estimate. No such per-curve numerical certificate is asserted in this writeup.

A finite certificate and its precise hypothesis.

Proof. Equation (cont6:sandwich) gives $r=R$. The exact zeros and certified nonzero derivative give analytic order $R$. The completion factor is nonzero at the centre, so $\operatorname{ord}_{s=1} L(E,s)=R=r$.$\square$

The proposition is a sufficient certificate, not a new criterion known to be obtainable for every curve. It does not require the leading-term formula, a conjectural order for $\operatorname{Sha}$, or a probabilistic interpretation of a small computed value. Its analytic nonvanishing component has a fully explicit error bound above.

Stress test I: parity is only part of the vanishing data.

For a concrete logical test, take any integer $R\ge2$ and consider \[ F_\varepsilon(z)=z^R+\varepsilon z^{R-2}. \] All these entire functions have the same parity $(-1)^R$. They converge uniformly on every compact set to $z^R$ as $\varepsilon\to0$, but for $\varepsilon\ne0$ their order at zero is $R-2$. Thus parity and any fixed positive tolerance on function values do not certify the order. These polynomials are not proposed elliptic-curve $L$-functions; they disprove the purely analytic inference that an unqualified precision argument would be making. Extra arithmetic structure might give exact zeros, but it must actually be supplied.

Stress test II: increasing descent is not a termination proof.

Verification and outcome.

Outcome: Conditional certification method with explicit analytic error bounds; UNRESOLVED. The remaining work is to supply exact same-parity central vanishings and sufficiently sharp algebraic rank bounds in arbitrary rank. This attempt does not establish either a uniform termination theorem or a solution of the universal conjecture.

Sources

• S1 Clay Mathematics Institute, The Millennium Prize Problems. https://www.claymath.org/library/monographs/MPPc.pdf. Formulation source.
• S2 Birch and Swinnerton-Dyer Conjecture. https://www.claymath.org/millennium/birch-and-swinnerton-dyer-conjecture/. Further reference; not a proof endorsement. Consulted 24 September 2026: Institutional overview only.
• S3 Introduction to the Birch and Swinnerton-Dyer Conjecture — Fabio Ferrari Ruffino. https://arxiv.org/abs/2608.25975. Further reference; not a proof endorsement.
• S4 Proof of the Birch and Swinnerton-Dyer Conjecture — Yoshinori Shimizu. https://zenodo.org/records/17010555. Further reference; not a proof endorsement.
• E1 Andrew Wiles, The Birch and Swinnerton-Dyer Conjecture, official Clay Mathematics Institute problem description, pages 1–2. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf. Added primary source: Elliptic curves, the Hasse–Weil L-function, and the rank formulation; the leading-coefficient refinement is not added to this entry.. Consulted 24 September 2026.
• E2 J. S. Milne, Elliptic Curves, author text, Chapter IV, Sections 2, 5 and 6, and Chapter V (descent, heights and modular forms). https://www.jmilne.org/math/Books/ectext6.pdf. Primary author text consulted 27 September 2026. The explicit truncation estimates are derived in this attempt.

Birch and Swinnerton-Dyer Conjecture

Definitions and mathematical statement

Formulation and concept references: [S1], [E1].

Short English statement

Research attempt

Scope, provenance, and outcome.

Final outcome of every pass: no verified counterexample was found. Neither a proof of BSD nor a Lean formalization was produced. Exact-arithmetic certificate claims, numerical diagnostics, and computer-assisted interval claims are kept distinct throughout. The historical correction to the second pass is retained rather than silently removing the unsuccessful strategy. [A1][A2][A3][A4]

Reading the record.

Statements such as "rechecked", "performed in this turn", or "the current run" in a reproduced pass describe the checks reported by that pass, not a new execution during this export. This export does not turn saved logs into formal proofs, nor parsing a JSON result into a fresh numerical integration. The export date is 27 September 2026; the third report itself is dated 14 September 2026. Dates and public-claim checks inherited from those records are historical attributions, not fresh web verification.

The user's research trajectory.

Evidence conventions.

Notation used across the passes.

For conductor $N$, put \[ c=\frac{2\pi}{\sqrt N},\qquad \Lambda_E(s)=c^{-s}\Gamma(s)L(E,s),\qquad D_k=c\Lambda_E^{(k)}(1). \] The numerical files generally store $D_k$, not raw $L^{(k)}(E,1)$. Completion preserves the first nonzero derivative order. For the positive-sign central-zero cases, $D_2=L''(E,1)$; $D_4$ must not automatically be identified with $L^{(4)}(E,1)$. The detailed normalizations are preserved below. [E8][A5]

Pass I: broad congruent-number screen

Result

No counterexample was found in this computation. This package is a bounded search, not a proof of the Birch--Swinnerton-Dyer conjecture, and not a rigorous verification of analytic ranks. It does not assert that counterexamples do not exist.

The target in the uploaded Wiles problem statement is

\[\operatorname{rank}E(\mathbb Q)\ne\operatorname{ord}_{s=1}L(E,s).\]

The family examined was $E_n:y^2=x^3-n^2x$, with odd squarefree $1\le n\le 1{,}000{,}000$. This is the congruent-number family in the attachment.

Scope and actual results

An exact preliminary screen covered 405,286 parameters n. It computed ternary representation counts and pure 2-Selmer dimensions. A bounded rational-point search used primitive Pythagorean parameters $1\le v<u\le10{,}000$. It did NOT search every rational point on those curves.

For 311 curves the point-search lower bound and 2-Selmer upper bound agreed at an arithmetic rank of at least two:

\setlength{\tabcolsep}{4pt}

\noalign{}

\noalign{}

\noalign{}

All 311 were tested by a separate numerical L-function computation. Three low-rank controls were also evaluated. There were no numerical disagreements in those 314 evaluations. This does NOT say that all 405,286 curves received a full arithmetic-rank computation or an analytic-order computation.

The two rank-four parameters are n = 57,715 and n = 752,115.

Exact arithmetic computations

The script search.py uses exact integer representation counts

\[T_c(n)=\#\{(x,y,z)\in\mathbb Z^3:2x^2+y^2+cz^2=n\}.\]

for $c=8,32$, and computes the Monsky matrix over $\mathbb F_2$. If $n$ has $k$ odd prime factors, the pure 2-Selmer dimension is $s_2(n)=2k-\operatorname{rank}_{\mathbb F_2}M_n$. This gives an UPPER BOUND for the Mordell--Weil rank, not the rank itself.

Primitive Pythagorean parameters give \[ u v(u^2-v^2)=nt^2,\qquad P=\left(\frac{nu}{v},\frac{n^2t}{v^2}\right)\in E_n(\mathbb Q). \] The squareclasses of $(x,x-n)$, together with the two rational 2-torsion classes, give an independently computed rank lower bound. An exact arithmetic rank is reported only when this equals the Selmer upper bound.

The supplied verifier independently rebuilds the Monsky matrix, verifies each point on its curve with rational arithmetic, verifies its claimed squareclasses, and checks equality of the two rank bounds. It needs only the Python standard library. Its output in the performed run was:

PASS: 311 exact arithmetic rank certificates; no BSD assumptions.

The mathematical inputs to these certificates are standard 2-descent and Monsky's matrix theorem. This is not a proof-assistant formalization of those theorems.

Important distinctions:

\tightlist
• $T_8(n)=2T_{32}(n)$ is not, by itself, an unconditional positive-rank proof.
• Positive Selmer dimension need not equal arithmetic rank.
• Failing to find a point in a bounded search is not a rank-zero certificate.
• The $s_2=0$ portion of the preliminary screen lies in an already known BSD case and should be understood as a consistency/implementation check.

Independent numerical L-function diagnostic

The script analytic_scan.py evaluates quadratic twists of the modular form $\eta(4z)^2\eta(8z)^2$ through a truncated Mellin integral. Its Fourier coefficients are generated from the CM theta series and independently checked against an exact eta-product expansion and finite-field point counts for small primes.

For the odd squarefree twists, $N=32n^2$, $c=2\pi/\sqrt N$, and

\[\Lambda(s)=c^{-s}\Gamma(s)L(E_n,s).\]

The reported derivatives are $c\Lambda^{(k)}(1)$, not raw $L^{(k)}(E_n,1)$. The two have the same first nonzero derivative order. The numerical routine examines the functional-equation-compatible orders through order six; it does not use the arithmetic rank to decide which derivatives to calculate or classify as zero.

Two evaluations use 128 versus 256 Gauss--Legendre nodes and Fourier exponential cutoffs 55 versus 70. Both use float64. The absolute numerical-zero threshold is 1e-8 on the scaled completed derivatives. The source and result files disclose these choices explicitly.

This is NOT a rigorous analytic-zero certification. An extremely small nonzero value could be mistaken for zero. Agreement between two quadrature settings is a numerical check, not a proof of vanishing, and no rigorous interval arithmetic or certified derivative-zero argument is claimed. The displayed analytic ranks are therefore estimates throughout.

The computation uses the standard finite L-function; Wiles's problem statement omits finitely many Euler factors. These factors are nonzero at $s=1$ for this family, so this distinction does not change the target vanishing order.

Additional complete-screen summary.

\nolinkurl{summary.json}

Pass II: Cassels pairing, covering searches, and engineered twists

Historical correction notice.

\hyperref[pass3]{Pass III}

Result and scope

No counterexample was found. This pass replaced the old, easy-point-biased comparison with an exact Cassels-pairing calculation, a descent-directed point search, and 40 deliberately high-Selmer twists above the old parameter range. It is not a proof of BSD and not a verification of all analytic vanishing orders.

The curve family is

\[E_n:\quad y^2=x^3-n^2x,\qquad n>0\ \text{odd and squarefree}.\]

The uploaded Wiles statement asks whether arithmetic rank equals the order of vanishing of $L(E_n,s)$ at $s=1$. This search concentrates on one sufficient way to refute that assertion:

\[L(E_n,1)=0\qquad\text{and}\qquad\operatorname{rank}E_n(\mathbb Q)=0.\]

Such a curve would be a genuine counterexample. Failure of this particular test does not rule out other discrepancies, for example arithmetic rank two and analytic order four.

The arithmetic computation uses no L-values, analytic ranks, BSD, or assumed finiteness of the Tate--Shafarevich group. Higher analytic derivatives are computed separately and numerically only.

The different search strategy

Write

\begin{align*} T_8(n)&=\#\{(x,y,z)\in\mathbb Z^3:2x^2+y^2+8z^2=n\},\\ T_{32}(n)&=\#\{(x,y,z)\in\mathbb Z^3:2x^2+y^2+32z^2=n\}. \end{align*}

For the odd squarefree twists here, Tunnell's theorem gives the unconditional central-value test

\[L(E_n,1)=0\quad\Longleftrightarrow\quad T_8(n)=2T_{32}(n).\]

This statement about the L-value does not assume BSD. The further implication from a zero central value to positive arithmetic rank is exactly what the search tries to contradict. See Top--Yui, Theorem 3.6 and its proof, cited below.

The earlier Monsky computation supplied the pure 2-Selmer dimension $s_2$, an upper bound for the arithmetic rank. "Pure" means that the two-dimensional rational 2-torsion contribution has been quotiented out. The ordinary 2-Selmer dimension is $s_2+2$ for this family.

This pass computes the Cassels pairing C on that pure space. The image of the rational-point group lies in its radical, so the improved upper bound is

\[\operatorname{rank}E_n(\mathbb Q)\le s_2(n)-\operatorname{rank}_{\mathbb F_2}C_n.\]

The exact counterexample trigger is consequently

\[T_8(n)=2T_{32}(n)\quad\text{and}\quad s_2(n)-\operatorname{rank}_{\mathbb F_2}C_n=0.\]

Instead of blindly increasing the size of rational x-coordinates, the new point search takes basis classes in the radical of C_n, parameterizes one of their covering conics by rational lines, and searches the resulting binary quartic for square values. Modular square-residue sieves precede an exact integer-square check. Each returned elliptic-curve point is then checked by rational arithmetic. The point search is bounded and does not certify insolubility on failure.

These are established tools, combined and implemented for this search. There is no claim that the algorithms are new or that the individual curves have never previously been studied.

Pass A: deeper descent in the old range

From the original 405,286 odd squarefree parameters n

\textless

Every pairing certificate was rechecked by the independent standard-library verifier. The old 311 rank certificates were rechecked as well. The original ternary counts for all 4,923 parameters were independently recomputed using the binary-norm factorization method described below.

\setlength{\tabcolsep}{4pt}

\noalign{}

\noalign{}

\noalign{}

The complete deep-target distribution is:

\setlength{\tabcolsep}{4pt}

\noalign{}

\noalign{}

\noalign{}

The 1,494 exact-central-zero targets therefore leave rank upper bound two in 1,443 cases and four in 51 cases. None has been certified rank zero.

All six $s_2=6$ cases in the old range

The targeted covering search now resolves the arithmetic ranks of these six curves. Five have matching independent point lower bounds and pairing upper bounds of two; the sixth has upper bound zero.

\setlength{\tabcolsep}{4pt}

\end{quote}

\noalign{}

\begin{minipage}[b]{\linewidth}\raggedleft n \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Old point lower bound \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Old upper \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft New exact rank \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft $T_8$ \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft $T_{32}$ \end{minipage}

\noalign{}

\noalign{}

Two radical-basis classes were searched on each of the five zero-central-value curves. All ten needed points were found with chart parameters $|a|\le64$ and $1\le b\le64$. This is a bound in the specific covering-conic chart, not a bound on every rational point of the elliptic curve.

Explicit example: n=952561

Here $n=17\cdot137\cdot409$. The old point search found no non-torsion point. The new Cassels matrix, in the saved basis, is

\[ C_{952561}=\begin{pmatrix} 0&1&1&1&0&1\\1&0&0&1&0&0\\1&0&0&1&1&0\\ 1&1&1&0&1&1\\0&0&1&1&0&0\\1&0&0&1&0&0 \end{pmatrix}. \]

Its rank over $\mathbb F_2$ is four, giving arithmetic rank at most 6-4=2. The new covering-directed search found

\begin{align*} P&=\left(\frac{700813729}{64},\frac{18482232821745}{512}\right),\\ Q&=\left(\frac{5701974113}{4624},\frac{273426800389743}{314432}\right). \end{align*}

Both points satisfy $y^2=x^3-952561^2x$ exactly. Their descent squareclasses, written in the order $(x-n,x+n,x)$, are respectively

\[(17,6953,409),\qquad(409,137,56033).\]

Their Kummer images are independent modulo the rational torsion contribution. Thus they give arithmetic rank at least two; together with the pairing bound, this certifies arithmetic rank exactly two. This is a resolution of a gap in our previous search, not a claim that the curve's rank was unknown to mathematics.

The exact Tunnell equality is 2048=2*1024, hence $L(E_n,1)=0$. The separate numerical calculation gives L' '($E_n$,1) approximately 153.67672450649, indicating analytic order two. This derivative is not accompanied by a rigorous interval bound.

Pass B: engineered twists above the old range

Choose four distinct primes below 5000, all 1 modulo 8, such that each pair is a pair of quadratic residues. Select the 40 smallest products within this finite construction. For these choices the Monsky matrix is zero, so every target has pure 2-Selmer dimension eight (ordinary dimension ten), independently of BSD. The construction does not say that the rational-point rank is eight.

These 40 parameters range from 259,173,449 to 1,123,727,617. They are a selected set, not an exhaustive scan of the interval between those endpoints.

Two exact algorithms computed each central-value count: direct signed-triple enumeration, and the independent binary-norm-factorization computation. All 40 pairs of counts agree.

\setlength{\tabcolsep}{4pt}

\end{quote}

\noalign{}

\begin{minipage}[b]{\linewidth} Exact central value \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Point lower bound \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Pairing upper bound \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Curves \end{minipage}

\noalign{}

\noalign{}

All 23 central-zero curves have pairing rank six and hence arithmetic rank at most two. The 17 central-nonzero curves never triggered a conflict; twelve have an independent descent-certified rank of zero. For the remaining five, the arithmetic descent calculation only gives upper bound two, although the known analytic-rank-zero theorem in Wiles's attachment gives arithmetic rank zero. These two sources of knowledge are deliberately distinguished in the data.

The two large curves with newly matching arithmetic bounds of two are

\[n=299018729\qquad\text{and}\qquad n=669561329.\]

For the 23 central-zero curves, two radical-basis classes were each searched with chart bounds 64 and then 256. Fourteen curves yielded one independent point and seven yielded none. No finite failure is used as a rank-zero certificate.

The seven central-zero curves still lacking a point in this bounded search are:

\setlength{\tabcolsep}{4pt}

\end{quote}

\noalign{}

\begin{minipage}[b]{\linewidth}\raggedleft n \end{minipage}

\begin{minipage}[b]{\linewidth} Prime factors \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft $T_8$ \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft $T_{32}$ \end{minipage}

\begin{minipage}[b]{\linewidth} Certified bounds from this search \end{minipage}

\noalign{}

\noalign{}

This is a list of unfinished cases in this computation, not a list of suspected counterexamples or a claim that these ranks are unknown in the literature.

Numerical follow-up: what was and was not certified

For the six old-range $s_2=6$ curves, L-function derivatives were reevaluated using quadratic-twist modular-form coefficients, separately from the arithmetic rank. Run A used float64 and global 256-node Gauss quadrature with cutoff 70. Run B used long-double exponential evaluations and sums, with composite 24-node Gauss quadrature on intervals of length at most one, and cutoff 90. The platform's long-double significand has 64 bits; these are not 64-digit calculations.

On the five exact-central-zero curves the new numerical estimates of $L^{\prime\prime}(1)$ are:

\setlength{\tabcolsep}{4pt}

\noalign{}

\noalign{}

\noalign{}

The saved raw derivative values are derivatives of the scaled completed Mellin transform $c\Lambda(s)$, with $c=\pi/(\sqrt8\,n)$. At a central zero on these even-sign curves, its second derivative at one agrees with the ordinary $L^{\prime\prime}(1)$. Away from that setting, higher derivatives in the raw file are not simply ordinary L-function derivatives. The constant term is $L(1)$.

The two numerical settings agree to the displayed precision in the table. Their difference is not a rigorous error bound. Tunnell's counts certify only the exact zero/nonzero status at the center; they do not certify a higher vanishing order. The 40 engineered large curves did not receive numerical higher-derivative scans.

Certificate design and mathematical inputs

\nolinkurl{new/verify_pairings.py}

\tightlist
• prime factors and a full basis of the Monsky kernel;
• primitive integral points on each of the three conics and their tangent forms;
• exact local square-root identities, Hensel congruences, and nonzero tangent values;
• every local Hilbert symbol, the global pairing matrix, and its $\mathbb F_2$ rank;
• rational point equations and independence of their squareclasses, when supplied.

At odd primes, certified residues determine the local square roots by ordinary Hensel lifting. At 2, the verification requires one extra bit in the square congruence to certify the claimed root precision, plus three unit bits when computing Hilbert symbols. Contributions at infinity are trivial because the second arguments are positive. At primes outside 2n, primitive conic points and good reduction allow Cassels's good-reduction lemma to remove the local factors.

Both directions of the pairing were computed rather than imposing symmetry. Alternation and symmetry were checked. The search also recalculated using two different local-point choices. The stored certificate records one fully checked choice per basis vector and place.

The verifier rests on standard mathematical inputs: Monsky's theorem, Cassels's pairing formula and good-reduction lemma, local Hilbert-symbol formulas, and the Kummer map. It is not a Lean or other proof-assistant formalization.

For the independent Tunnell count check, sum the signed representations by $X^2+2Y^2$ of $n-8z^2$. For positive m the binary count is

\[r(m)=2\sum_{d\mid m}\chi_{-8}(d),\qquad m>0,\]

and $r(0)=1$. Trial factorization computes this sum. Keeping only even z gives the $T_{32}$ count. This is a different algorithm from enumerating x and z and testing whether the residual is an exact square. Floating square roots in the direct C++ program propose an integer root only; integer corrections and equality make the final decision.

Pass III: strategy correction and genuine higher-order screens

1. Scope and public claim check

The target is the rank equality in Andrew Wiles's attached Millennium problem description: $\operatorname{rank}E(\mathbb Q)=\operatorname{ord}_{s=1}L(E,s)$. This pass continues to study $E_n:y^2=x^3-n^2x$ for positive odd squarefree n. It does not test all elliptic curves or every part of the refined leading-coefficient conjecture.

The public searches performed in this turn did not locate a curve equation, paper, or formalization substantiating the rumored Claude BSD counterexample. Anthropic's 4 September announcement concerns formalizing Fermat's Last Theorem, a different assertion. Clay's BSD page still labels the problem "Unsolved." Neither observation establishes what a private research team may have found.

2. Correction to the previous counterexample strategy

The previous pass sought a simultaneous exact central zero and a nondegenerate pure Cassels pairing, which would certify arithmetic rank zero. That was a poor counterexample target for this CM family.

Burungale and Tian's rank-zero p-converse gives, for a CM elliptic curve over Q and any prime p,

\[\operatorname{corank}_{\mathbb Z_p}\operatorname{Sel}_{p^\infty}(E/\mathbb Q)=0\quad\Longrightarrow\quad L(E,1)\ne0.\]

Here is the additional deduction used in this report. The kernel of the Cassels pairing on $\operatorname{Sel}_2$ is the image of $\operatorname{Sel}_4$. Nondegeneracy after removing rational 2-torsion therefore forces rank zero and eliminates elements of order 4 from $\operatorname{Sha}[2^\infty]$. Its remaining 2-primary part is finite, so $\operatorname{Sel}_{2^\infty}$ has corank zero. Taking p=2 in the published theorem excludes our former proposed trigger.

Thus this is a correction to the search design, not evidence against the published theorem. A central-zero/nondegenerate-pairing output from these implementations would first be a consistency failure to investigate. This deduction does not exclude all higher-rank BSD mismatches.

3. Genuine higher-order screen with tight arithmetic bounds

Selected all 1,443 old-range records with exact central zero, pure 2-Selmer dimension at least four, and Cassels rank upper bound two. All 1,443 arithmetic certificates were independently reverified in this turn.

A curve in this set with analytically certified order at least four would violate BSD, since its arithmetic rank is at most two. The initial diagnostic computed the second derivative with 64 Gauss-Legendre nodes and exponential cutoff 45. The flagging threshold was absolute value less than 0.05. This threshold is a numerical screening rule, not a proof of vanishing or nonvanishing.

Result: zero flags. The numerical estimates ranged from approximately 15.3928147362 to 644.9577627003. All eight order-four numerical controls were correctly flagged by the same coarse rule.

The twenty smallest second-derivative estimates were reevaluated with 128 nodes/cutoff 55 and 256 nodes/cutoff 70. The smallest was

\[n=399041:\qquad L^{\prime\prime}(E_n,1)\approx15.392814808351593.\]

Among these twenty, the maximum discrepancy between the two finer settings was 2.31e-13. The maximum discrepancy between the coarse and fine estimates was 1.13e-7. Agreement between quadratures is not an interval error bound.

4. Higher-Selmer controls and exact rank-four resolutions

Independently scanned all 51 earlier central-zero curves whose Cassels upper bound is four. The same modular-form Mellin method, with 128 versus 256 nodes, numerically indicated order two on 43 curves and order four on eight.

A new bounded search examined 622 descent classes on these 51 curves. It used exact conic parametrizations and integer square tests. A multi-projection follow-up found the remaining fourth independent point for n=330881.

The eight numerical order-four targets now all have exact arithmetic rank four:

\[ \begin{gathered} n\in\{57715,328321,330881,526921,\\ 648091,752115,804601,918769\}. \end{gathered} \]

The computed absolute second derivatives on these eight were below 1.4e-13, and their scaled completed fourth derivatives were substantial. These are numerical diagnostics, not rigorous order-four certificates. Four independent Kummer images and the independent upper bound four certify the arithmetic ranks without BSD.

For the other 43 curves, the bounded search established $2\le r\le4$ in 29 cases; $1\le r\le4$ in 11; and $0\le r\le4$ in three. These are NOT 43 certified arithmetic-rank-two computations. No arithmetic lower bound exceeded the numerically estimated analytic order in this set.

5. Resolving the earlier large-parameter point-search gaps

The previous pass's 23 large central-zero curves all had Cassels rank upper bound two. Their earlier exact/lower-bound breakdown was 2 exact rank two, 14 with lower bound one, and seven with lower bound zero.

This turn enlarged the original chart search to height 4096, then tried all three conic projections and different omitted coordinates. A heuristic reduction using approximate quartic roots chose integral coordinate changes; every coordinate substitution, square test, curve equation, and independence decision was subsequently exact. This is a computational improvement, not a claim of a historically new method.

The new breakdown is:

\setlength{\tabcolsep}{4pt}

\noalign{}

\noalign{}

\noalign{}

The last four are n=700302641 (lower bound zero) and n=743852833, 999964633, 1089143641 (lower bound one). A finite failed point search is never a rank-zero certificate.

Former headline candidate n=259173449

Here $n=17\cdot137\cdot257\cdot433$. The exact central counts remain $T_8=98304,\quad T_{32}=49152$. Two explicit points now found are:

\[ P=\left(\frac{58429931845358025}{12931216}, -\frac{14100596620347634742289285}{46500652736}\right), \] \[\delta(P)=(2329,59321,7361).\]

\[ Q=\left(\frac{2334310538755264353}{8999937424}, -\frac{138692151936732705371816943}{853806063540032}\right), \] \[\delta(Q)=(1891777,259173449,137).\]

Both lie on $y^2=x^3-n^2x$ exactly. Their independent Kummer images give lower bound two; the reverified pairing gives upper bound two. Thus the exact arithmetic rank is two. This eliminates its status as a rank-zero candidate in this search, but is not a certification of its full analytic vanishing order.

6. Verification performed in this turn

The final independent standard-library verifier passed on 1,534 distinct Cassels certificates: 1,443 tight-bound targets, 51 higher-order targets, and all 40 large engineered curves (including the 17 central-nonzero controls).

It checked 142 saved rational-point witnesses across 74 curves, including exact equations, squareclasses, and independence modulo rational torsion. The 142 witnesses are not all newly discovered; some were inherited and rechecked.

Two exact counting programs were freshly rerun on all 1,517 central-zero targets $1,443 + 51 + 23$. One directly enumerates the two ternary quadratic forms; the other counts binary norm representations using factorization. Their results agree exactly in all 1,517 cases. The Tunnell theorem is the external mathematical input translating these counts into central L-value statements.

The independent verifier does not import the Cassels-pairing producer. However it relies on mathematical theorems (Monsky's matrix, Cassels' formula and good-reduction lemma, and the Kummer injection) rather than formalizing those theorems itself. No Lean kernel was run. No numerical analytic rank is promoted to an exact one.

Research significance of the correction.

Pass IV: non-CM rank-four curves and interval falsification

1. Target of the search

Wiles's attached Millennium problem asks for equality between the rational-point rank and the order of vanishing of the L-function at $s=1$. This pass sought a curve with independently certified arithmetic rank four but a nonzero second completed derivative. Such a derivative would force analytic order at most two and hence give a counterexample.

This is a falsification test, not an attempt to prove BSD. Nonvanishing is amenable to a finite interval certificate; exact vanishing is not obtained merely by increasing numerical precision.

The new curves have the form

\[ E_{a,b}:y^2=x(x-a)(x+b),\qquad 16\mid a,\quad b\equiv1\pmod4,\quad\gcd(a,b)=1. \]

They have full rational 2-torsion, allowing explicit descent. All 135 selected curves are semistable and non-CM; minimal-model invariants, nonintegral j-invariants, conductors and root numbers were checked independently.

2. Actual scope and counts

The parameters satisfy 16

\textless

\textless

\textless

\textless

\setlength{\tabcolsep}{4pt}

\end{quote}

\noalign{}

\begin{minipage}[b]{\linewidth} Stage \end{minipage}

\begin{minipage}[b]{\linewidth}\raggedleft Number \end{minipage}

\noalign{}

\noalign{}

The selected conductors are distinct and range from 83,306,670 to 4,942,926,222. Only these 135 selected curves had their L-functions evaluated in this pass. This is not a complete search of every elliptic curve below the conductor bound, nor a complete identification of the rank-four curves in the parameter rectangle. The integral-point cutoff can miss points and entire candidate curves.

Raw selection:

\nolinkurl{noncm_wide_candidates.jsonl}

\nolinkurl{noncm_wide_summary.json}

\nolinkurl{noncm_selected.json}

3. Exact arithmetic ranks, with no BSD input

For E:y\^{}2=x$x-a$$x+b$, away from 2-torsion the Kummer map is

\[ P=(x,y)\longmapsto(x,x-a)\in(\mathbb Q^*/\mathbb Q^{*2})^2. \]

The third coordinate x+b is determined by their product, since the product of all three is a square. The images of $0,0$ and $a,0$ are respectively (-ab,-a) and $a,a(a+b)$. Global squareclasses are represented using -1 and the primes dividing 2ab$a+b$.

For each target the four saved point classes and two torsion classes have combined $\mathbb F_2$ rank six; the torsion classes have rank two. This proves an arithmetic lower bound four. Every one of the 540 point equations and its squareclass coordinates was rechecked with exact integers/rationals. Independence is modulo torsion, not merely the fact that the points have different coordinates. The points are not claimed to be a saturated Mordell-Weil basis.

The separate upper-bound computation imposes all local Kummer conditions. At an odd prime, $E(\mathbb Q_p)/2E(\mathbb Q_p)$ has dimension two because all 2-torsion is rational; at p=2 it has dimension three. This follows from the index of multiplication by 2 on the p-adic Lie group: the index is $\#E(\mathbb Q_p)[2]/|2|_p$. At the real place its dimension is one, since the cubic has three real roots and the real group has two components.

At each necessary place the certificate contains actual local-point witnesses giving that full dimension. A witness is either rational 2-torsion or a rational x whose cubic value is a square in the local field. The verifier checks the local square criterion directly. Once independent witnesses attain the known local dimension, their span is the complete local image; no bounded local search is being mistaken for a proof of local insolvability.

Imposing those local image conditions on the globally supported squareclasses gives a 2-Selmer space of dimension six on every target. At primes outside 2ab$a+b$, the required conditions are the unramified ones already enforced by the squareclass support. The injection $E(\mathbb Q)/2E(\mathbb Q)$ -

\textgreater{}

\textless

\[ \operatorname{rank}E_{a,b}(\mathbb Q)=4\quad\text{for all 135 targets.} \]

The framework is standard two-descent, not a new theorem; see Cremona, Algorithms for Modular Elliptic Curves, section 3.6. The specific witness/linear-system implementation and its independent verifier are included here.

Files:

\nolinkurl{noncm_descent.py}

\nolinkurl{noncm_descent_certificates.json}

\nolinkurl{verify_final.py}

\nolinkurl{verification.log}

4. Models, conductors, and exact L-series inputs

The integral minimal model is

\[ Y^2+XY=X^3+\frac{b-a-1}{4}X^2-\frac{ab}{16}X, \]

obtained using x=4X, y=8Y+4X. Its invariants are

\[ c_4=a^2+ab+b^2,\qquad \Delta_{\min}=\frac{(ab(a+b))^2}{256}. \]

At every discriminant prime $c_4$ is a unit, so reduction is multiplicative and this integral model is minimal. The conductor is the product of those primes. The nonintegrality of $j=c_4^3/\Delta_{\min}$ excludes complex multiplication. The global root number is -1 times the product of the local multiplicative root numbers -$a_p$.

At odd bad primes the trace is $b/p$ for p

\textbar

\textbar

\textbar

At good primes

\nolinkurl{semistable_coefficients.cpp}

Cross-checks actually performed:

\tightlist
• On the first target, every prime through 145267 (13443 primes) was checked against literal finite-field enumeration. The complete coefficient file needed for that target, through index 145265, agrees byte-for-byte with the corresponding prefix of this fresh computation.
• On all 135 targets, all primes through 251 were independently re-enumerated by the Python verifier: 7290 prime-trace checks.
• All 135 coefficient arrays were reconstructed from their compressed prime traces, and every reconstructed SHA-256 hash matched the original array used by the interval calculation.

The complete coefficient arrays occupy hundreds of megabytes. To keep the archive compact, it contains lossless gzip-compressed signed-16-bit prime traces, a manifest with limits and hashes, and a restoration script. Restoration does not itself independently recount points;

\nolinkurl{semistable_coefficients.cpp}

5. Analytic enclosure results

Let $c=2\pi/\sqrt N,\quad \Lambda(s)=c^{-s}\Gamma(s)L(E,s),\quad D_k=c\Lambda^{(k)}(1)$. Completion does not change vanishing order. We evaluated $D_2$ and $D_4$ from the modular Mellin integral using 256-bit MPFR directed rounding.

The implementation uses sixteen unit panels and 32-point Gauss-Legendre quadrature on each. It verifies the quadrature nodes by interval sign changes, includes q-series truncation tails at every node, adds an explicit Bernstein-ellipse quadrature error, and adds the tail of the integral after u=16. The uniform error allowances are $2^{-90}$ for $D_2$ and $2^{-80}$ for $D_4$, plus $2^{-400}$ for the integration tail.

\nolinkurl{INTERVAL_METHOD.md}

For all 135 targets:

\[ |D_2|<8.08\times10^{-28},\qquad D_4>0. \]

The largest absolute $D_2$ interval endpoint was

\nolinkurl{8.07800082132170775214160635423423075509074568091522586851617989870e-28}

Every interval contains zero. None establishes the nonvanishing needed for our counterexample trigger. The $D_4$ lower endpoints range down to approximately 1383.5444; all $D_4$ intervals are well away from zero.

For these positive-rank curves, the analytic-rank-zero theorem quoted in the attached statement already implies $L(E,1)=0$, and root number +1 implies $L^{\prime}(E,1)=0$. Therefore $D_2$ equals $L^{\prime\prime}(E,1)$. Root number +1 and $D_4\ne0$ imply that the analytic order is either two or four. The computation does not distinguish those two possibilities when the $D_2$ interval contains zero.

In particular, the statement $|D_2|<8.08\times10^{-28}$ does not exclude a much smaller nonzero value and is not a proof of analytic order four. No curve in this pass is being advertised as a full BSD verification merely on the basis of these intervals.

Files:

\nolinkurl{certified_moments.cpp}

\nolinkurl{mpfr_minimal_abi.h}

\nolinkurl{gauss32_nodes.txt}

\nolinkurl{run_intervals.py}

\nolinkurl{certified_intervals.json}

\nolinkurl{noncm_analytic_results.json}

6. Concrete rank-four example

The smallest-conductor target is

\[ E:y^2=x(x-3200)(x+3649),\qquad N=83,306,670. \]

Four independent points modulo torsion are

\[ (-3645,9990),\quad(-3560,46280),\quad(-3528,53592),\quad(-3280,88560). \]

For this curve the global squareclass calculation has fourteen variables, constraint rank eight, and Selmer dimension six. It gives arithmetic rank exactly four.

The computed interval results imply the outward-rounded statements

\[ -8.08\times10^{-28}<D_2<8.08\times10^{-28}, \]

\[ 3523.03977896542029048128<D_4<3523.03977896542029048130. \]

The exact decimal interval endpoints are in

\nolinkurl{interval_3200_3649.json}

\nolinkurl{certified_intervals.json}

7. Positive control

The same enclosure program was tested on

\[ y^2=x(x-48)(x+17),\qquad N=3315. \]

The points $-16,32$ and $-12,60$, together with a separate full 2-descent upper bound, certify exact arithmetic rank two. The independent verifier checks this additional control certificate. Its second-derivative enclosure is strictly positive, around

\[ D_2=4.554571172739648387582614119\ldots. \]

Thus the routine is capable of excluding zero rather than mechanically returning a zero-containing interval. This successful control is a software check, not a substitute for the analytic error analysis. The control is additional to the 135 rank-four targets and their 540 point witnesses.

Files:

\nolinkurl{control_rank.json}

\nolinkurl{build_control.py}

\nolinkurl{control_intervals.json}

\nolinkurl{control_coefficients.bin}

8. Audit of the previous pass

Before the new search, the previous package's verifier was freshly rerun, including both exact Tunnell-count algorithms. It rechecked 1534 distinct Cassels-pairing certificates and 142 rational-point witnesses, and recomputed both counting algorithms on all 1517 central-zero targets. Those checks passed. This is a rerun of the supplied certificates, not a claim that every underlying theorem or implementation has been formally audited.

Its log is

\nolinkurl{prior_reverification.log}

9. What is and is not established

Established by the supplied computation and stated mathematical algorithms: exact arithmetic rank four on 135 selected non-CM curves; the reported analytic derivative enclosures; a working rank-two nonzero-derivative control; and the enumerated cross-checks.

Not established: a counterexample; exact analytic order four on the 135 targets; a general proof of BSD; completeness outside the explicitly bounded point search; historical novelty of any listed curve; or Lean formalization. The new code has not been independently peer-reviewed. The independent arithmetic verifier and exact rounding/error analysis make the evidence inspectable, but do not eliminate the need to review the implementation and the mathematical inputs before relying on a claimed research discovery.

A fresh unpacking of the distribution also passed the arithmetic verifier. Its C++ sources compiled, the first coefficient array was restored with its matching hash, and the first analytic enclosure was recomputed exactly matching the saved JSON. These packaging checks are recorded in

\nolinkurl{package_verification.log}

\nolinkurl{package_build.log}

\nolinkurl{package_restore_test.log}

\nolinkurl{package_interval_test.json}

The final counterexample test found no certified mismatch.

Counterexample direction in the final pass.

Final analytic method: complete error-bound derivation

This note documents the error bounds used by

\nolinkurl{certified_moments.cpp}

1. Normalization and integral

Let $E/\mathbb Q$ have conductor $N\le5{,}000{,}000{,}000$ and root number +1. Let $a_n$ be the coefficients of its standard L-function, including the finite Euler factors at bad primes. Define

\[ c=2\pi/\sqrt N,\qquad \Lambda(s)=c^{-s}\Gamma(s)L(E,s),\qquad D_k=c\Lambda^{(k)}(1). \]

The modular Mellin transform and the functional equation give

\[ \Lambda(s)=\int_1^\infty f(it/\sqrt N)(t^{s-1}+t^{1-s})\,dt, \quad f(it/\sqrt N)=\sum_{n\ge1}a_n e^{-cnt}. \]

Thus, for even k,

\[ D_k=2c\int_0^\infty e^u u^k\sum_{n\ge1}a_n e^{-cn e^u}\,du. \]

This is a change of variables and differentiation of an absolutely convergent integral, not a use of BSD. The prefactor $c^{-s}\Gamma(s)$ is nonzero at $s=1$, so completion does not alter the analytic order. Wiles's attached statement omits some finite Euler factors; those factors are nonzero at $s=1$ and also do not change the order.

For our rank-four targets the analytic-rank-zero theorem quoted in Wiles's description implies $L(E,1)=0$: otherwise their arithmetic rank would be zero. Root number +1 then implies $L^{\prime}(E,1)=0$. Consequently $D_2=L^{\prime\prime}(E,1)$. In contrast, $D_4$ is not automatically $L^{(4)}(E,1)$, since we have not proved $L^{\prime\prime}(E,1)=0$.

Reference: John Cremona, Algorithms for Modular Elliptic Curves, section 2.8, equations $2.8.1$-$2.8.6$, https://johncremona.github.io/book/fulltext/chapter2.pdf ; Andrew Wiles, The Birch and Swinnerton-Dyer Conjecture, attached problem description, pp. 2 and 4.

2. Exact coefficients and the universal majorant

At good primes the coefficients are obtained by counting $E(\mathbb F_p)$, with $a_p=p+1-\#E(\mathbb F_p)$. At multiplicative primes $a_p$ is +1 or -1. The Euler recurrences determine the remaining $a_n$. Hasse's bound and these recurrences give

\[ |a_n|\le d(n)\sqrt n\le 2n. \]

Indeed $d(p^j)=j+1$ bounds the corresponding normalized prime-power coefficient, and $d(n)\le2\sqrt n$ by pairing divisors around $\sqrt n$. This deliberately loose bound is sufficient.

For any real $0<q<1$ and any truncation $m\ge0$,

\[ \left|\sum_{n>m}a_n q^n\right| \le 2\sum_{n>m}nq^n =2q^{m+1}\frac{(m+1)-mq}{(1-q)^2}. \]

The program adds this tail interval at each quadrature node. Its heuristic choice of m is only a speed optimization: correctness of the bound does not depend on that heuristic.

3. Quadrature error on $[0,16]$

Write

\[ F_k(u)=2c e^u u^k\sum_{n\ge1}a_n e^{-cn e^u}. \]

Divide $[0,16]$ into the sixteen intervals $[j,j+1]$. On each interval use the 32-point Gauss-Legendre rule. Map it from $[-1,1]$ by $u=j+\frac12+\frac z2$. On the Bernstein ellipse of parameter $\rho=4$ for z, every resulting u satisfies

\[ \Re u\ge-9/16,\quad |\Im u|\le15/16,\quad |u|<18. \]

In particular $\exp(-\Re u)<2$ and $\cos(\Im u)>\frac12$. Also $c>1/20000$, since $N\le5\times10^9$, $\pi>3$, and $\sqrt N<75000$.

Put $\alpha=c\exp(\Re u)\cos(\Im u)>0$. The elementary inequality

\[ \sum_{n\ge1}n e^{-\alpha n} =\frac1{4\sinh^2(\alpha/2)}\le\frac1{\alpha^2} \]

yields

\[ |F_k(u)|\le\frac{32\cdot18^k}{c}\le M_k, \qquad M_k=640000\cdot18^k. \]

The Fourier/Laurent representation under $z=(w+w^{-1})/2$ bounds the degree-l Chebyshev coefficient of an analytic function bounded by M on this ellipse by $2M\rho^{-l}$. Hence its degree-63 Chebyshev truncation has uniform error at most

\[ \frac{2M\rho^{-64}}{1-\rho^{-1}}=\frac83 M2^{-128}. \]

The 32-point Gauss rule is exact through degree 63, its weights are positive and sum to 2, and integration over $[-1,1]$ has norm 2. The quadrature error is therefore at most four times that uniform approximation error. Account for the half-width 1/2 and sum over all sixteen panels:

\[ |\text{total quadrature error}|\le \frac{256}{3}M_k2^{-128}. \]

For $k=2$ this is strictly less than $2^{-90}$; for $k=4$ it is strictly less than $2^{-80}$. These inequalities are checked by exact rational arithmetic in

\nolinkurl{verify_final.py}

The estimates apply to the full analytic integrand, not merely the polynomial truncation evaluated in the implementation. The separate per-node series tails cover the difference between that integrand and its computed finite sums.

4. Infinite tail $u\ge16$

Let $B=c\exp(16)$. A finite positive Taylor sum proves $\exp(16)>8{,}000{,}000$, hence $B>400$. Substitute $t=c\exp(u)$, then $t=B+v$. Since $e^{-t}<1/4$, the coefficient majorant gives

\[ \left|2\int_B^\infty\log(t/c)^k\sum_{n\ge1}a_n e^{-nt}\,dt\right| \le8e^{-B}\int_0^\infty e^{-v}(16+v/B)^k\,dv. \]

The logarithmic bound uses $\log(1+v/B)\le v/B$. Expanding the polynomial and integrating $v^je^{-v}$ gives

\[ \sum_{j=0}^k {k\choose j}16^{k-j}\frac{j!}{B^j}<2\cdot16^k \]

for $k=2,4$. It follows that the tail is less than $16\cdot16^k\exp(-400)$. As $e>8/3$ and $16\cdot16^k(3/4)^{400}<1$, this is less than $2^{-400}$. All the rational inequalities, including the polynomial integral bound, are checked in

\nolinkurl{verify_final.py}

5. Directed rounding and validation of nodes

The implementation uses MPFR 4.2.2 at 256 bits, with lower endpoints rounded toward negative infinity and upper endpoints toward positive infinity. Arithmetic, exp, sqrt, powers, and pi are enclosed. No ordinary floating-point quadrature residual is used as an error certificate. MPFR's documented rounding guarantees are in https://www.mpfr.org/mpfr-current/mpfr.html , section 4.4.

The decimal approximations in

\nolinkurl{gauss32_nodes.txt}

The $10^{-60}$ bracket width need not be specially optimized. It is small enough to make its propagated uncertainty negligible relative to the explicit quadrature bound in this run.

6. Trust boundary and interpretation

These are computer-assisted enclosures based on the mathematics above and the supplied C++ implementation. They are not Lean proofs and have not undergone external peer review. The arithmetic verifier independently recomputes rank certificates; when checking the JSON analytic results it only checks their recorded endpoints. To recompute the analytic enclosures, build and run

\nolinkurl{certified_moments.cpp}

\nolinkurl{run_intervals.py}

The input Fourier coefficients are exact integers calculated separately from ranks. All their values are recoverable from the compressed prime-trace data and checked against SHA-256 hashes. For the first target all prime traces through 145267 were independently compared against literal finite-field point enumeration. All primes through 251 were independently enumerated for every target. The remaining good-prime calculations use the exact Hasse-interval algorithm documented in the report and source.

An interval excluding zero certifies nonvanishing within these stated trust assumptions. An interval containing zero does not certify vanishing. All 135 target $D_2$ intervals contain zero. All 135 target $D_4$ intervals are strictly positive. This leaves the analytic order in $\{2,4\}$, rather than establishing that it is 4.

Inherited methodological note from the supplied example

Editorial scope of the retained note.

Scope and source checkpoint.

The attempted route is to construct two independent certificates, one algebraic and one analytic, and ask what would make the procedure terminate in arbitrary rank. It yields explicit inequalities and an exact conditional certificate. It also exposes two reasons why extending successful low-rank computations is not a general proof. Standard descent, height and modular form inputs are taken from [E2], Chapters IV and V; the estimates below are derived here.

Algebraic side: isolate the descent defect.

Suppose $P_1,\ldots,P_R$ are rational points with a positive definite Néron--Tate Gram matrix. A rational linear dependence modulo torsion would have canonical height zero and contradict positive definiteness. Hence \begin{equation}\label{wsref-0-63-6f-6e-74-36-3a-73-61-6e-64-77-69-63-68} R\le r\le s_\ell-t_\ell. \end{equation} In particular, equality of the two computed endpoints proves $r=R$. This needs no assertion that the supplied points generate the entire Mordell--Weil group; finite index does not change rank. Conversely, a finite point search with no additional points does not prove the lower endpoint is the rank. Certified height intervals can prove independence if they certify positive definiteness, but an approximate positive determinant without error bounds is not such a certificate.

Analytic side: a rapidly convergent central expansion.

An explicit truncation bound.

Let $D_{k,M}$ be the sum in (cont6:derivative) truncated to $n\le M$, including its parity factor. Since $\log t\le t$ for $t\ge1$, repeated integration by parts gives the rigorous bound \begin{align} |\Lambda_E^{(k)}(1)-D_{k,M}| &\le 2\sum_{n>M}n^2\int_1^\infty e^{-cnt}t^k\,dt\\ &=2k!\sum_{n>M}n^2e^{-cn} \sum_{j=0}^{k}\frac{1}{(k-j)!(cn)^{j+1}}. \label{wsref-0-63-6f-6e-74-36-3a-74-61-69-6c} \end{align} This is already an explicit convergent majorant. A simpler closed upper bound follows from $n\ge1$. Set $q=e^{-c}$ and $C_k(c)=2k!\sum_{j=0}^k((k-j)!c^{j+1})^{-1}$. Then \begin{equation}\label{wsref-0-63-6f-6e-74-36-3a-63-6c-6f-73-65-64-74-61-69-6c} |\Lambda_E^{(k)}(1)-D_{k,M}| \le C_k(c)q^{M+1} \left(\frac{M+1}{1-q}+\frac{q}{(1-q)^2}\right). \end{equation} Indeed $n^2/n^{j+1}=n^{1-j}\le n$, and the remaining series is $\sum_{n>M}nq^n$. No unspecified implied constant depends on the curve or on the truncation. For large conductor the bound can be slow because $c$ is small, but it still tends to zero for each fixed $N,k$.

If certified quadrature and rounding enclose $D_{k,M}$ in an interval $I$, enlarging $I$ by the bound in (cont6:closedtail) gives a certified enclosure of the derivative. An interval excluding zero proves nonvanishing. It is essential to include quadrature and rounding errors, in addition to the Fourier-tail estimate. No such per-curve numerical certificate is asserted in this writeup.

A finite certificate and its precise hypothesis.

Proof. Equation (cont6:sandwich) gives $r=R$. The exact zeros and certified nonzero derivative give analytic order $R$. The completion factor is nonzero at the centre, so $\operatorname{ord}_{s=1} L(E,s)=R=r$.$\square$

The proposition is a sufficient certificate, not a new criterion known to be obtainable for every curve. It does not require the leading-term formula, a conjectural order for $\operatorname{Sha}$, or a probabilistic interpretation of a small computed value. Its analytic nonvanishing component has a fully explicit error bound above.

Stress test I: parity is only part of the vanishing data.

For a concrete logical test, take any integer $R\ge2$ and consider \[ F_\varepsilon(z)=z^R+\varepsilon z^{R-2}. \] All these entire functions have the same parity $(-1)^R$. They converge uniformly on every compact set to $z^R$ as $\varepsilon\to0$, but for $\varepsilon\ne0$ their order at zero is $R-2$. Thus parity and any fixed positive tolerance on function values do not certify the order. These polynomials are not proposed elliptic-curve $L$-functions; they disprove the purely analytic inference that an unqualified precision argument would be making. Extra arithmetic structure might give exact zeros, but it must actually be supplied.

Stress test II: increasing descent is not a termination proof.

Verification and outcome.

Outcome: Conditional certification method with explicit analytic error bounds; UNRESOLVED. The remaining work is to supply exact same-parity central vanishings and sufficiently sharp algebraic rank bounds in arbitrary rank. This attempt does not establish either a uniform termination theorem or a solution of the universal conjecture.

Supplementary result catalogues

Initial screen: all Selmer/central-value categories.

\nolinkurl{bsd_search/summary.json}

All 311 initially certified higher-rank parameters.

\nolinkurl{rank_certificates.json}

\nolinkurl{analytic_results.json}

41, 65, 145, 161, 219, 265, 291, 299, 323, 371, 465, 561, 609, 651, 721, 731, 777, 915, 987, 1081, 1105, 1113, 1131, 1155, 1185, 1241, 1419, 1659, 1705, 1785, 1995, 2035, 2139, 2145, 2379, 2465, 2849, 2945, 3003, 3289, 3355, 3705, 4179, 4305, 4641, 5115, 5185, 5865, 6545, 7395, 7449, 7611, 7689, 7995, 8385, 8547, 8835, 8931, 9345, 9401, 9579, 9867, 10545, 11193, 11715, 12155, 12331, 12369, 12435, 13195, 13299, 13395, 13515, 13585, 13795, 14385, 14763, 14835, 15249, 15771, 16089, 16185, 17017, 17459, 17985, 18705, 18921, 20235, 21385, 21585, 21945, 24395, 25707, 26715, 27555, 28329, 28905, 31065, 32505, 32745, 33649, 33915, 34881, 35931, 37185, 38049, 38985, 39435, 41041, 42315, 43617, 44115, 45115, 45339, 45771, 45849, 47355, 47859, 51051, 52059, 60819, 61761, 62491, 62601, 67065, 72345, 72611, 74195, 79779, 80619, 83265, 84315, 85785, 86955, 88689, 88939, 90321, 90915, 92345, 92939, 94395, 95865, 96441, 97905, 102201, 103785, 104995, 105995, 107835, 112497, 112931, 113505, 113529, 115995, 117705, 130011, 130065, 130305, 130515, 131835, 135915, 145299, 145761, 148155, 151305, 152691, 159915, 160545, 172515, 172601, 173355, 178035, 179265, 184569, 185339, 190785, 190995, 194649, 195891, 196185, 210795, 213465, 214305, 223307, 224315, 227715, 233761, 235235, 237705, 249555, 250305, 254265, 260715, 269841, 279609, 296835, 316545, 318801, 319865, 321321, 323169, 331851, 333465, 345345, 349305, 352905, 355971, 358545, 372099, 373065, 383019, 386745, 389235, 395241, 397155, 400155, 401289, 403995, 406065, 408595, 412665, 423291, 424235, 435435, 435643, 435651, 439185, 452049, 453009, 465905, 477411, 497211, 508515, 509795, 527345, 533577, 533715, 541443, 549841, 550715, 551361, 569985, 577995, 591745, 596505, 625865, 633795, 647745, 647801, 656121, 667337, 687291, 688755, 692265, 692835, 698145, 703185, 705705, 721259, 769769, 770385, 795795, 820155, 825945, 844305, 866235, 887281, 894355, 899745, 919555, 948441, 951555, 953771.

4199, 4669, 4895, 9015, 10549, 11005, 13317, 14965, 26565, 29055, 33117, 40885, 41151, 41943, 59415, 70941, 70959, 76245, 95095, 99645, 105735, 132405, 134805, 141141, 142071, 159999, 234255, 243165, 257439, 260015, 269535, 388245, 697965, 791245, 821541, 901901.

57715, 752115.

All 40 engineered twists, before and after the third pass.

\setlength{\tabcolsep}{3pt}

All 51 higher-Selmer follow-ups.

\setlength{\tabcolsep}{5pt}

The twenty smallest tight-bound numerical signals, refined.

All 135 final rank-four curves and all 540 point witnesses.

The last column below is a rounded display approximation to the midpoint of the saved $D_4$ interval. It is not an interval endpoint. All original decimal endpoints, including the $D_2$ endpoints, are preserved in

\nolinkurl{bsd_final/certified_intervals.json}

\setlength{\tabcolsep}{4pt}

\begin{tabular}[t]{@{}l@{}}$(-3645,9990)$\\$$-3560,46280$$\\$$-3528,53592$$\\$$-3280,88560$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1008,2016$$\\$$-972,11988$$\\$$-900,19620$$\\$$-676,28860$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3528,30744$$\\$$-3492,38412$$\\$$-3468,42636$$\\$$-2500,95700$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-396,5940$$\\$$-384,7104$$\\$$-324,10476$$\\$$-196,12180$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2220,15540$$\\$$-2196,19764$$\\$$-2028,35724$$\\$$-1681,48216$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1808,41584$$\\$$-1768,47736$$\\$$-1469,73450$$\\$$-1088,83776$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4312,32648$$\\$$-3960,83160$$\\$$-3880,89240$$\\$$-3492,108252$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6144,83712$$\\$$-6084,103428$$\\$$-5920,142080$$\\$$-5772,167388$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-784,9520$$\\$$-752,15792$$\\$$-712,20648$$\\$$-648,25704$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2548,9828$$\\$$-2300,40020$$\\$$-1936,52800$$\\$$-1053,47502$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-348,1044$$\\$$-232,9048$$\\$$-25,4770$$\\$$2900,33060$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5120,7680$$\\$$-4840,123640$$\\$$-4552,168424$$\\$$-4096,209920$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7956,119340$$\\$$-7488,198432$$\\$$-7252,222740$$\\$$-3825,257040$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3420,10260$$\\$$-3364,35380$$\\$$-2740,101380$$\\$$-2205,115290$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3420,44460$$\\$$-3364,59972$$\\$$-3240,83160$$\\$$-2952,115128$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6348,150420$$\\$$-6100,174460$$\\$$-5476,209716$$\\$$-5424,211536$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6900,40020$$\\$$-6396,159900$$\\$$-6292,172172$$\\$$-4225,246740$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2940,45780$$\\$$-2880,56160$$\\$$-2500,91500$$\\$$-2025,108000$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4620,13860$$\\$$-4225,115700$$\\$$-3885,147630$$\\$$-3840,150720$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-592,30192$$\\$$-512,31488$$\\$$-225,27060$$\\$$7400,404040$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4640,32480$$\\$$-4608,46848$$\\$$-4480,80640$$\\$$-4060,133980$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7128,30888$$\\$$-6369,216546$$\\$$-6348,218868$$\\$$-6241,229890$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2809,6254$$\\$$-2784,16704$$\\$$-2688,33600$$\\$$-2541,47124$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-729,4050$$\\$$-612,20196$$\\$$-408,26520$$\\$$-204,23460$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6408,61944$$\\$$-6241,102384$$\\$$-5120,195840$$\\$$-2888,182856$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1160,12760$$\\$$-1125,18600$$\\$$-928,33408$$\\$$-828,36708$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4500,33300$$\\$$-4356,71676$$\\$$-4188,96324$$\\$$-2601,154836$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1452,11484$$\\$$-1445,12750$$\\$$-1372,21364$$\\$$-756,36540$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7056,45360$$\\$$-7008,77088$$\\$$-6208,242112$$\\$$-4056,326040$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7992,55944$$\\$$-7812,132804$$\\$$-6696,287928$$\\$$-5832,328536$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3256,29304$$\\$$-3168,52800$$\\$$-2888,88920$$\\$$-1628,122100$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1216,10336$$\\$$-1089,28116$$\\$$-988,34580$$\\$$-961,35836$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6120,59160$$\\$$-5548,149796$$\\$$-4000,201600$$\\$$-2920,183960$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3108,46620$$\\$$-2809,68794$$\\$$-2744,71736$$\\$$-2688,73920$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-976,16592$$\\$$-969,17442$$\\$$-912,22800$$\\$$-192,24960$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2809,21942$$\\$$-2440,65880$$\\$$-2312,72488$$\\$$-1805,83980$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3564,5148$$\\$$-3528,31080$$\\$$-3380,67340$$\\$$-2728,122760$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-784,12432$$\\$$-676,22620$$\\$$-576,26880$$\\$$-81,16650$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7688,55800$$\\$$-7524,117876$$\\$$-7436,138996$$\\$$-7400,146520$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2989,46116$$\\$$-2888,58520$$\\$$-2809,65826$$\\$$-2548,81900$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1272,21624$$\\$$-1225,29050$$\\$$-1180,34220$$\\$$-1060,43460$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1444,27132$$\\$$-1352,32760$$\\$$-900,41820$$\\$$-121,18942$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3584,26880$$\\$$-3208,99448$$\\$$-3125,107250$$\\$$-2520,138600$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1216,12160$$\\$$-969,34884$$\\$$-841,38860$$\\$$-584,40296$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7168,134400$$\\$$-6936,186456$$\\$$-5184,324864$$\\$$-3549,321594$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6845,106190$$\\$$-6520,176040$$\\$$-6480,182160$$\\$$-5000,287000$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6912,99648$$\\$$-6889,105742$$\\$$-6032,217152$$\\$$-3625,250850$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4900,28700$$\\$$-4840,52360$$\\$$-4320,126720$$\\$$-2940,166740$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1464,7320$$\\$$-1404,25740$$\\$$-1369,31450$$\\$$-1176,49224$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1300,29380$$\\$$-1256,33912$$\\$$-961,49042$$\\$$-572,49764$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5041,74550$$\\$$-4896,114240$$\\$$-4664,153912$$\\$$-3816,222600$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3072,28416$$\\$$-2916,62532$$\\$$-2268,109620$$\\$$-2209,111390$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4232,75624$$\\$$-3136,184128$$\\$$-2992,188496$$\\$$-2056,191208$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5184,100800$$\\$$-5041,123966$$\\$$-3916,199716$$\\$$-100,39420$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2700,4860$$\\$$-2688,17472$$\\$$-2664,29304$$\\$$-2601,47430$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4161,108186$$\\$$-4056,123864$$\\$$-3724,158004$$\\$$-3364,179916$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3528,102312$$\\$$-3500,107100$$\\$$-3388,123508$$\\$$-2268,186732$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4864,109440$$\\$$-4624,142800$$\\$$-4484,156940$$\\$$-4336,169104$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1580,20540$$\\$$-1372,38220$$\\$$-1316,40796$$\\$$-940,47940$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3600,18720$$\\$$-3564,41580$$\\$$-3364,93380$$\\$$-2009,172200$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3600,38160$$\\$$-3388,81620$$\\$$-3364,84796$$\\$$-3276,95004$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3520,93280$$\\$$-3028,142316$$\\$$-2940,147420$$\\$$-660,115500$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5292,122220$$\\$$-4796,158268$$\\$$-4332,174420$$\\$$-4225,176540$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3204,54468$$\\$$-2984,80568$$\\$$-2116,114172$$\\$$-729,82782$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4840,154440$$\\$$-3888,194832$$\\$$-1080,120600$$\\$$-240,52560$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6720,77280$$\\$$-6540,124260$$\\$$-6292,164164$$\\$$-4160,255840$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3428,113124$$\\$$-2916,123876$$\\$$-2088,117624$$\\$$-640,60480$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4860,49140$$\\$$-4332,135204$$\\$$-3872,164736$$\\$$-3480,177480$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2349,7830$$\\$$-2172,49956$$\\$$-1392,86304$$\\$$-49,21840$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3364,64380$$\\$$-1776,111888$$\\$$-1188,97020$$\\$$-592,69264$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4225,148200$$\\$$-3840,178560$$\\$$-1080,153720$$\\$$-40,30360$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4884,170940$$\\$$-3600,203040$$\\$$-1332,131868$$\\$$-768,95424$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4725,117810$$\\$$-1728,135936$$\\$$-448,61824$$\\$$-168,35784$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2520,24360$$\\$$-2500,31500$$\\$$-2268,70812$$\\$$-700,90300$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1924,25012$$\\$$-1776,53280$$\\$$-1716,60060$$\\$$-1600,69920$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4928,49280$$\\$$-4784,81328$$\\$$-4624,103632$$\\$$-3220,164220$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5000,63000$$\\$$-4840,106040$$\\$$-4056,191880$$\\$$-3481,214760$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2160,39600$$\\$$-1936,61424$$\\$$-1828,67636$$\\$$-1520,77520$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2401,70070$$\\$$-2280,75240$$\\$$-2052,81396$$\\$$-1500,83100$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1992,13944$$\\$$-1952,23424$$\\$$-1944,24840$$\\$$-1369,59570$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2748,79692$$\\$$-2652,92820$$\\$$-2448,112608$$\\$$-1681,140220$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7260,151140$$\\$$-5808,346368$$\\$$-4500,384300$$\\$$-2160,315360$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6241,61778$$\\$$-6192,80496$$\\$$-6084,109980$$\\$$-5776,162032$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6912,47232$$\\$$-6760,100360$$\\$$-6728,107880$$\\$$-4165,243950$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1740,15660$$\\$$-1573,38038$$\\$$-1369,49580$$\\$$-1040,56160$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5880,7560$$\\$$-3072,244224$$\\$$-2160,219600$$\\$$-256,76800$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7225,258570$$\\$$-7056,283920$$\\$$-5776,387600$$\\$$-3481,391170$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7344,34272$$\\$$-6724,194012$$\\$$-6400,228160$$\\$$-6321,234780$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7800,54600$$\\$$-7512,187800$$\\$$-4800,422400$$\\$$-2496,364416$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6845,95460$$\\$$-6760,119080$$\\$$-6264,198360$$\\$$-4489,278050$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5832,70632$$\\$$-5484,137100$$\\$$-4116,214620$$\\$$-3025,210870$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3724,36708$$\\$$-3184,105072$$\\$$-3116,109060$$\\$$-2500,128100$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4900,89180$$\\$$-4732,122668$$\\$$-3996,193140$$\\$$-3721,205570$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3580,139620$$\\$$-3060,172380$$\\$$-833,134946$$\\$$-5,10920$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3136,40320$$\\$$-408,64872$$\\$$4352,189312$$\\$$14739,1742670$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6804,67284$$\\$$-6724,91676$$\\$$-6588,120780$$\\$$-2888,202920$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4332,36252$$\\$$-3840,104640$$\\$$-2940,135660$$\\$$-2704,136448$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4212,51012$$\\$$-4032,79968$$\\$$-3844,98580$$\\$$-2900,133980$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4800,74880$$\\$$-4312,134904$$\\$$-4096,148992$$\\$$-1944,154440$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5704,51336$$\\$$-5476,102564$$\\$$-4508,177100$$\\$$-3100,184140$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4900,7980$$\\$$-4576,137280$$\\$$-3712,228288$$\\$$-2552,252648$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1332,37740$$\\$$-1312,39360$$\\$$-1112,50040$$\\$$-392,46200$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1792,40768$$\\$$-1628,53724$$\\$$-1232,66528$$\\$$-1036,67340$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5832,6696$$\\$$-5800,38280$$\\$$-4901,175682$$\\$$-4408,198360$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5632,25344$$\\$$-4232,259256$$\\$$-3960,270600$$\\$$-1152,205824$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3468,92820$$\\$$-2349,148770$$\\$$-1392,136416$$\\$$4332,74100$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6936,46920$$\\$$-6561,179820$$\\$$-6000,260400$$\\$$-1920,272640$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6292,54340$$\\$$-6264,64728$$\\$$-4900,203980$$\\$$-4524,212628$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7560,88200$$\\$$-7420,126140$$\\$$-7000,191800$$\\$$-6724,218612$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1700,16660$$\\$$-1573,46332$$\\$$-1292,71060$$\\$$-884,80444$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6216,217560$$\\$$-4332,277932$$\\$$-4225,277290$$\\$$-4053,275604$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-4949,50904$$\\$$-4608,120960$$\\$$-4456,138136$$\\$$-3636,185436$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6764,223212$$\\$$-6460,251940$$\\$$-5760,291840$$\\$$-169,57018$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7056,199248$$\\$$-6561,253368$$\\$$-6272,274176$$\\$$-4624,314160$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2600,14040$$\\$$-2548,30940$$\\$$-2424,50904$$\\$$-1809,85626$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5488,25872$$\\$$-4536,234360$$\\$$-3864,274344$$\\$$-2688,284928$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-2392,50232$$\\$$-2025,92070$$\\$$-1725,106260$$\\$$-828,101844$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5304,26520$$\\$$-4232,176088$$\\$$-2504,187800$$\\$$-832,111488$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6300,97020$$\\$$-6084,157716$$\\$$-4608,298368$$\\$$-3388,311388$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-8112,74256$$\\$$-6936,328440$$\\$$-6561,359640$$\\$$-1920,303360$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1224,21624$$\\$$-800,50880$$\\$$-748,51612$$\\$$-729,51786$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6897,171798$$\\$$-6000,244800$$\\$$-5329,265282$$\\$$-2565,208620$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6396,44772$$\\$$-6292,82940$$\\$$-5476,188108$$\\$$-4992,212160$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6241,107282$$\\$$-5832,178200$$\\$$-5652,197820$$\\$$-4312,261800$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6728,315752$$\\$$-4840,376200$$\\$$-4489,373860$$\\$$4232,61272$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6292,7436$$\\$$-5952,130944$$\\$$-5776,157168$$\\$$-5425,193130$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-3856,77120$$\\$$-3604,104516$$\\$$-3264,125664$$\\$$4131,232254$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-7776,118368$$\\$$-7749,129150$$\\$$-6176,352032$$\\$$-5488,380240$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5292,145404$$\\$$-3844,206460$$\\$$-3672,206856$$\\$$-1176,124488$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-988,20748$$\\$$-884,34476$$\\$$-196,36540$$\\$$15300,1359660$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-1372,106428$$\\$$-400,65280$$\\$$-297,56628$$\\$$-192,45792$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5200,71760$$\\$$-1836,180540$$\\$$-961,132990$$\\$$-624,106704$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-5832,8424$$\\$$-5577,130416$$\\$$-5016,215688$$\\$$-4312,264264$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}$$-6728,25752$$\\$$-5776,235600$$\\$$-4312,298760$$\\$$-1408,205568$$\end{tabular}

\begin{tabular}[t]{@{}l@{}}

\end{tabular}

Reproducibility, file maps, and source preservation

First archive: file map and reproduction.

Files

\tightlist
• triangles.cpp: bounded primitive-Pythagorean point search.
• triangle_points.csv: witnesses from the performed search.
• search.py: exact preliminary screen and arithmetic rank bounds.
• summary.json: screen counts, scope, and limitations.
• exact_screen_arrays.npz: compressed arrays from the screen.
• exact_rank_ge2.json: 311 higher-rank records and triangle witnesses.
• make_certificates.py: converts those witnesses into rational coordinates.
• rank_certificates.json: directly checkable rational-point certificates.
• verify_rank_certificates.py: independent exact verifier.
• verification.txt: captured verification result.
• analytic_scan.py: independent numerical L-function calculation.
• analytic_results.json: every numerical result, settings, and caveats.

Reproduction

Requirements: Python 3.10 or newer, NumPy, and a C++17 compiler. The certificate verifier needs only Python; NumPy and a compiler are needed to rerun the search. Run from this directory:

g++ -O3 -std=c++17 triangles.cpp -o triangles
./triangles 10000 1000000 > triangle_points.csv
python search.py
python make_certificates.py
python verify_rank_certificates.py
OPENBLAS_NUM_THREADS=1 python analytic_scan.py

To check just the supplied exact arithmetic rank certificates:

python verify_rank_certificates.py

Do not run Python with -O: these research scripts use assertions for validation. Numerical last digits can depend on platform and NumPy version. The supplied results document the actual run rather than guaranteeing bitwise portability.

Second archive: reproduction and file map.

Reproduction

Run from this archive's

\nolinkurl{bsd_push2}

python new/verify_all.py

Do not use python -O, because the verifiers use assertions. The command checks all 311 old rank certificates, 4,923 old-range pairing certificates, 40 large pairing certificates, all new saved point sets, and agreement of the two sets of saved count outputs. To rerun the count algorithms themselves:

g++ -O3 -std=c++17 new/tunnell_counts.cpp -o /tmp/bsd_tunnell_counts
g++ -O3 -std=c++17 new/tunnell_norm_check.cpp -o /tmp/bsd_tunnell_norm
/tmp/bsd_tunnell_counts < new/engineered_n.txt > new/engineered_counts.csv
/tmp/bsd_tunnell_norm < new/engineered_n.txt > new/engineered_norm_counts.csv
/tmp/bsd_tunnell_norm < new/old_deep_n.txt > new/old_deep_norm_counts.csv
python new/verify_all.py

Recomputing the pairings and point searches requires SymPy and NumPy. The numerical L-function pass additionally uses Numba. The versions actually used are recorded in

\nolinkurl{new/summary.json}

python new/run_pairings.py
python new/cover_search.py
python new/engineered_targets.py
python new/run_engineered.py
python new/analytic_followup.py
python new/verify_all.py

The included previous-range

\nolinkurl{.npz}

\nolinkurl{run_pairings.py}

File map

\nolinkurl{new/summary.json}

\nolinkurl{new/rank_bounds.csv}

\nolinkurl{new/directed_point_results.json}

\nolinkurl{new/engineered_point_results.json}

\nolinkurl{new/analytic_followup_results.json}

\nolinkurl{new/final_verification.txt}

\nolinkurl{previous/bsd_search}

Third archive: commands and stateful point-search extensions.

Verify

python verify_push3.py
python verify_push3.py --recount

The first command uses only the Python standard library. The second also requires g++ and recompiles/runs the two exact count algorithms. Do not run Python with -O.

\nolinkurl{verification.txt}

Reproduce numerical searches

python higher_order_scan.py
python higher_arithmetic.py
python finish_rank4.py
python tight_upper_scan.py
python refine_tight.py
python summarize_points.py

These overwrite their output files. Use a separate copy to preserve the supplied evidence. The numerical scans require NumPy and SymPy; the tight-bound scans use multiprocessing with Unix fork. Point search routines require NumPy and SymPy. The local tested environment was Python 3.13.5, NumPy 2.3.5, SymPy 1.14.0. No Sage, PARI/GP, or Lean was run in this pass.

Large point-search extensions

\nolinkurl{extend_points.py}

\nolinkurl{multichart_search.py}

\nolinkurl{reduce_search.py}

\nolinkurl{summarize_points.py}

The archive includes the completed outputs, so resuming the completed searches normally does no work. To regenerate from the original inputs, use a fresh copy without

\nolinkurl{extended_points.json}

\nolinkurl{multichart_points.json}

\nolinkurl{bsd_push2/new/engineered_point_results.json}

Limits

Exact arithmetic certificates rely on the cited descent theorems; they are not a formalization of those theorems. Numerical vanishing orders are estimates. Failure to find a point is not an upper bound. The number of curves whose arithmetic rank is exactly determined must not be confused with the number numerically screened. Full details and source references are in REPORT.md.

7. Files and reproducibility

Run python verify_push3.py for the saved certificate checks. Run python verify_push3.py -\/-recount to additionally compile and freshly execute both exact counting programs; this requires a C++17 compiler named g++.

\nolinkurl{current_point_certificates.json}

\nolinkurl{central_counts_all.csv}

\nolinkurl{tight_upper_results.json}

\nolinkurl{tight_upper_refined.json}

\nolinkurl{higher_order_results.json}

\nolinkurl{higher_arithmetic_results.json}

\nolinkurl{large_rank_results.json}

The

\nolinkurl{bsd_push2}

Final archive: complete reconstruction instructions.

Requirements

The tested environment was 64-bit little-endian GNU/Linux, Python 3.13.5, g++, GMP and MPFR 4.2.2. The primary arithmetic verifier, descent producer and coefficient restoration use only the Python standard library. MPFR/GMP libraries and a C++17 compiler are needed to recompute the interval integrals. Official MPFR development headers are preferable; a minimal ABI declaration fallback for LP64 GNU/Linux is supplied because that header was absent in the execution environment. No library binaries, Sage, PARI, Lean, or font files are included.

Do not use Python

\nolinkurl{-O}

\nolinkurl{NDEBUG}

\nolinkurl{-ffast-math}

Quick exact-arithmetic verification

From this directory:

python3 verify_final.py

This freshly checks the 135 rank-four arithmetic certificates, all 540 point equations and Kummer classes, all local image frames, the global Selmer dimensions, minimal models and root numbers, the exact rational error-bound constants, and the rank-two positive control. It also parses the saved interval summaries. Parsing a saved interval summary is not rerunning the integration.

Restore all exact analytic inputs

python3 restore_coefficients.py --jobs 4
python3 verify_final.py --sample-primes

This reconstructs every required $a_n$ from the losslessly compressed prime traces and compares all 135 array hashes to

\nolinkurl{COEFFICIENTS_MANIFEST.json}

The stored trace arrays are signed 16-bit little-endian, in increasing order of all primes

\textless

Recompute the analytic enclosures

bash build.sh
python3 run_intervals.py
./certified_moments 3315 control_coefficients.bin gauss32_nodes.txt > control_intervals.json
python3 verify_final.py --sample-primes

\nolinkurl{run_intervals.py}

\nolinkurl{certified_intervals.json}

Every target's second-derivative interval contains zero; none proves an exact zero. Every fourth completed-derivative interval excludes zero. This leaves analytic order two or four, rather than proving order four.

Recompute the Euler coefficients directly from the curves

Instead of trusting and restoring the compressed input traces, run the C++ exact point-counting program. For the first target:

mkdir -p coefficients
OMP_NUM_THREADS=4 ./semistable_coefficients 3200 3649 83306670 145265 coefficients/E_3200_3649.bin check

The optional final

\nolinkurl{check}

\nolinkurl{check}

For all targets, read the four parameters a, b, conductor, limit from

\nolinkurl{COEFFICIENTS_MANIFEST.json}

Repeat the bounded curve and rank search

OMP_NUM_THREADS=4 ./noncm_search 8192 8192 131072 5000000000 > fresh_candidates.jsonl 2> fresh_grid_summary.json
python3 - <<'PY'
import json
rows=[json.loads(s) for s in open('fresh_candidates.jsonl')]
rows.sort(key=lambda r:r['conductor'])
assert len(rows)==135
assert rows==json.load(open('noncm_selected.json'))
print('Selection reproduces all 135 saved records.')
PY
python3 noncm_descent.py
python3 verify_final.py

Output order from the parallel grid search may differ; compare after sorting. The grid search is a bounded search for integral points, not a proof that no further candidates or rational points exist.

\nolinkurl{noncm_analytic.py}

Principal result files

\nolinkurl{noncm_selected.json}

\nolinkurl{noncm_descent_certificates.json}

\nolinkurl{certified_intervals.json}

\nolinkurl{verification.log}

\nolinkurl{restoration_verification.log}

\nolinkurl{prior_reverification.log}

\nolinkurl{FILES_SHA256.json}

This is a reproducible research attempt, not a peer-reviewed result or a formal proof-assistant development.

Software versions recorded by the experiments.

Do not use Python

\nolinkurl{-O}

\nolinkurl{NDEBUG}

\nolinkurl{-ffast-math}

Archive identities.

821e68b7afccffce1ad133946897e63de428df51f115d332effec209b9c3c85c

977b26644e1a1440c37a9ef6f7ebbf9881e01b5c9795b615b6194605c408b3ca

e20245f3c6873c89291dff6d0b9513f7a23eccfac75455b972d138ac501a4586

3cf93f661d19d562adc347d460153e1040371863fa497137d12f39996f39b392

Final status and unresolved obligations

What the record establishes within its stated trust boundaries.

The remaining arithmetic gaps.

The remaining analytic distinction.

What is not claimed.

Outcome: documented counterexample searches, exact arithmetic certificates and explicit analytic enclosures; UNRESOLVED.

Sources

Source-list provenance.

• S1 Clay Mathematics Institute, The Millennium Prize Problems. https://www.claymath.org/library/monographs/MPPc.pdf. Formulation source.
• S2 Birch and Swinnerton-Dyer Conjecture. https://www.claymath.org/millennium/birch-and-swinnerton-dyer-conjecture/. Further reference; not a proof endorsement. Consulted 24 September 2026: Institutional overview only.
• S3 Introduction to the Birch and Swinnerton-Dyer Conjecture — Fabio Ferrari Ruffino. https://arxiv.org/abs/2608.25975. Further reference; not a proof endorsement.
• S4 Proof of the Birch and Swinnerton-Dyer Conjecture — Yoshinori Shimizu. https://zenodo.org/records/17010555. Further reference; not a proof endorsement.
• E1 Andrew Wiles, The Birch and Swinnerton-Dyer Conjecture, official Clay Mathematics Institute problem description, pages 1–2. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf. Added primary source: Elliptic curves, the Hasse–Weil L-function, and the rank formulation; the leading-coefficient refinement is not added to this entry.. Consulted 24 September 2026.
• E2 J. S. Milne, Elliptic Curves, author text, Chapter IV, Sections 2, 5 and 6, and Chapter V (descent, heights and modular forms). https://www.jmilne.org/math/Books/ectext6.pdf. Primary author text consulted 27 September 2026. The explicit truncation estimates are derived in this attempt.

• E3 Shenxing Zhang, On non-congruent numbers with $8a\pm1$ type odd prime factors and tame kernels, arXiv:2111.11618, Section 2.1 (Monsky matrix), Section 2.2 (Cassels pairing), and Lemma 2.1 (good-reduction local factors). https://arxiv.org/abs/2111.11618. Reference carried forward from Pass II; the first README cites the same identifier under a shorter title. The export does not adjudicate title versions.

• E4 Jaap Top and Noriko Yui, Congruent number problems and their variants, Theorem 3.6 and its proof. https://pub.math.leidenuniv.nl/~stevenhagenp/ANTproc/old/19yuiold.pdf. Reference carried forward for modular forms, twists, and the unconditional central-value formulation of the Tunnell relation.

• E5 J. Tunnell, A classical diophantine problem and modular forms of weight $3/2$, Inventiones Mathematicae 72 $1983$, 323--334. Primary theorem cited by Wiles and the experimental reports.

• E6 Ashay A. Burungale and Ye Tian, A rank zero $p$-converse to a theorem of Gross--Zagier, Kolyvagin and Rubin, Annals of Mathematics 203 $2026$, 1--13. https://annals.math.princeton.edu/2026/203-1/p01. Reference and theorem statement inherited from Pass III; used there to correct the earlier CM rank-zero search target.

• E7 Tom Fisher, Edward F. Schaefer, and Michael Stoll, The yoga of the Cassels--Tate pairing, Section 3. https://arxiv.org/abs/0710.2079. Reference carried forward for the Selmer-lifting interpretation of the pairing kernel.

• E8 John Cremona, Algorithms for Modular Elliptic Curves, Chapter 2, Section 2.8, equations $2.8.1$--$2.8.6$. https://johncremona.github.io/book/fulltext/chapter2.pdf. Mellin transform, finite Euler factors, and completed functional equation; reference used by the final report and error-bound note.

• E9 John Cremona, Algorithms for Modular Elliptic Curves, Chapter 3, Section 3.6. https://johncremona.github.io/book/fulltext/chapter3.pdf. Two-descent and Selmer upper bounds; reference carried forward from the final computation.

• E10 GNU MPFR 4.2.2 manual, Section 4.4. https://www.mpfr.org/mpfr-current/mpfr.html. Directed and correct rounding. Version 4.2.2 is the version recorded by the experiment, not a newly checked latest-version claim.

• E11 SymPy documentation, Diophantine equations, rational ternary conic solving. https://docs.sympy.org/latest/modules/solvers/diophantine.html. Reference from Pass II; returned conic points were checked by exact substitution in the reported computation.

• E12 Anthropic, Formalizing Fermat's Last Theorem, 4 September 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem. Public-source claim and date carried forward from the historical 14 September 2026 report. Not a fresh verification, and not evidence of a BSD counterexample.

• A0 User-supplied LaTeX example,

  \nolinkurl{Pasted text$20260927-132934$.txt}

  . Basis for the four-subsection structure, preserved formulation, methodological note, and original source list. The attached

  \nolinkurl{birchswin.pdf}

  is Wiles's primary problem description, cited as E1.

• A1 First conversation research response and

  \nolinkurl{bsd_counterexample_search.zip}

  . The

  \nolinkurl{bsd_search}

  directory contains the complete README,

  \nolinkurl{summary.json}

  , the 311 rank certificates, numerical outputs, scripts, and verification record. These are conversation-generated research materials, not an external publication.

• A2 Second conversation response,

  \nolinkurl{bsd_counterexample_push2_report.md}

  , and

  \nolinkurl{bsd_counterexample_push2.zip}

  . Cassels pairings, 40 engineered twists, exact witnesses and count checks. The rank-zero search strategy in this report is superseded by A3; its data and certificates are preserved.

• A3 Third conversation response,

  \nolinkurl{bsd_counterexample_push3_report.md}

  , and

  \nolinkurl{bsd_counterexample_push3.zip}

  . Report dated 14 September 2026: theoretical correction, 1,443 tight-bound numerical scans, 51 higher-Selmer follow-ups, and consolidated large-curve point certificates.

• A4 Final conversation response,

  \nolinkurl{bsd_counterexample_final_report.md}

  , and

  \nolinkurl{bsd_counterexample_final.zip}

  . The

  \nolinkurl{bsd_final}

  directory contains 135 non-CM rank-four targets, local-descent certificates, exact prime-trace inputs, interval results, independent-verifier source, controls, recorded checks, and reproduction instructions.

• A5 Final technical note,

  \nolinkurl{bsd_counterexample_final_interval_method.md}

  ; also

  \nolinkurl{bsd_final/INTERVAL_METHOD.md}

  . Full normalization, coefficient majorant, Bernstein-ellipse quadrature bound, infinite-tail bound, directed-rounding procedure, node validation, and mathematical/software trust assumptions.