% Standalone LaTeX source: main proof, Appendices A--G, references, and all verifier listings. % Compile twice with: pdflatex -interaction=nonstopmode -halt-on-error fermat433_hexagon.tex % Standalone source containing the proof, appendices, bibliography, and verifier listings. % Public problem reference: arXiv:2404.08518v9, 30 August 2026, Table 4, p. 4. \RequirePackage{fix-cm} \documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[a4paper,margin=0.85in]{geometry} \usepackage{amsmath,amssymb,amsthm,booktabs,hyperref,microtype,longtable,array,listings,xcolor,textcomp,needspace} \hypersetup{colorlinks=false,pdfborder={0 0 0},bookmarksnumbered=true, pdftitle={Primitive Integer Solutions of x^4 + 4y^3 + z^3 = 0}, pdfsubject={Exact certificates and complete verifier source}} \definecolor{linegray}{gray}{0.48} \lstdefinestyle{source}{language=Python,basicstyle=\fontsize{8.4}{10.1}\selectfont\ttfamily, keywordstyle=\bfseries,commentstyle=\itshape,showstringspaces=false,upquote=true, columns=fullflexible,keepspaces=true,breaklines=true,breakatwhitespace=false, numbers=left,numberstyle=\fontsize{6.5}{8}\selectfont\color{linegray},numbersep=7pt, xleftmargin=1.8em,frame=none,tabsize=4, postbreak=\mbox{\textcolor{linegray}{\ensuremath{\hookrightarrow}}\space}, aboveskip=8pt,belowskip=8pt} \lstdefinestyle{plain}{basicstyle=\fontsize{8.4}{10.1}\selectfont\ttfamily, columns=fullflexible,keepspaces=true,breaklines=true,showstringspaces=false,upquote=true, postbreak=\mbox{\textcolor{linegray}{\ensuremath{\hookrightarrow}}\space}, aboveskip=6pt,belowskip=6pt} \newcommand{\code}[1]{\texttt{\detokenize{#1}}} \newcommand{\NP}{\mathop{N}} \newtheorem*{theorem}{Theorem} \newtheorem*{lemma}{Quartic-point lemma} \newcommand{\Q}{\mathbb Q} \newcommand{\Z}{\mathbb Z} \newcommand{\F}{\mathbb F} \newcommand{\eps}{\varepsilon} \setlength{\parindent}{0pt} \setlength{\parskip}{5pt} \title{Primitive Integer Solutions of $x^4+4y^3+z^3=0$} \author{} \date{} \begin{document} \maketitle \vspace{-1.5em} \begin{abstract} We determine all primitive integer solutions of the generalized Fermat equation \[ x^4+4y^3+z^3=0. \] Here primitive means $\gcd(x,y,z)=1$. We prove that the only primitive solutions are \[ (x,y,z)=(1,0,-1),\qquad(-1,0,-1). \] The proof begins with a fourth-power descent in the pure cubic field $\mathbb Q(\sqrt[3]{2})$, reducing the problem to the rational points on two explicit smooth plane quartics of genus $3$. These quartics admit maps to elliptic curves over $\mathbb Q(\sqrt[3]{2})$. Exact $2$-descent determines the relevant Mordell--Weil ranks and finite-index subgroups. A complete reduction sieve at $127$ leaves four residue disks, and an elliptic Chabauty calculation proves that each disk contains exactly one rational point. Reconstruction of the original variables then leaves precisely the two stated primitive solutions. The finite computations are exact and reproducible from the certificates and verifier source included in the appendices, and the argument applies at all heights. \end{abstract} \vspace{0.5em} \begin{theorem} The primitive integer solutions of $x^4+4y^3+z^3=0$ are exactly \[ (x,y,z)=(1,0,-1),\quad(-1,0,-1). \] Here primitive means $\gcd(x,y,z)=1$, as in \cite[Table~4]{Grechuk}. \end{theorem} Set $K=\Q(\theta)$, $\theta^3=2$, and $\eps=1+\theta+\theta^2$. For $j\in\{0,2\}$, let $C_j\subset\mathbb P^2$ be the curve on which the coefficient of $\theta$ in $\eps^j(a+b\theta+c\theta^2)^4$ vanishes. Appendices A--G reproduce the finite computations and complete verification source. The resulting argument is unconditional and applies at all heights. \begin{lemma} \[ C_0(\Q)=\{(1:0:0),(0:0:1),(0:2:-1)\},\qquad C_2(\Q)=\{(1:0:-1)\}. \] \end{lemma} The certificate-based proof of this lemma is given below. \subsection*{Reduction of the theorem to the lemma} Write $X=x$, $Y=-y$, $Z=-z$, so $Z^3+4Y^3=X^4$. Primitivity gives $X\ne0$ and $\gcd(Y,Z)=1$. If $Z$ were even, the left side would have 2-adic valuation $2$; hence $Z,X$ are odd. If $3\mid X$, the unit cubes $Y^3,Z^3$ would give $Z^3+4Y^3\in\{\pm3,\pm5\}\pmod9$, a contradiction. Thus $\gcd(X,6)=1$. We use $\mathcal O_K=\Z[\theta]$, class number one, and $\mathcal O_K^\times=\{\pm\eps^n:n\in\Z\}$. These field facts have small certificates: $T^3-2$ is Eisenstein at $2$, and the polynomial of $1+\theta$ is Eisenstein at $3$; the discriminant is $-108$. The Minkowski bound is $(4/\pi)(3!/3^3)\sqrt{108}<3$, and the prime of norm $2$ is $(\theta)$. Finally, $\eps(\theta-1)=1$. A positive unit $1<\rho<\eps<4$ would, by Fourier inversion of its three embeddings, have all three coefficients in $\{0,1\}$; the eight norms exclude such a unit. This proves the unit assertion. Now $\alpha=Z+\theta^2Y$ has norm $X^4$ and is a unit above $2,3$. If a prime ideal above $p>3$ divides $\alpha$, its residue satisfies $\theta=-2Y/Z\in\F_p$. Hence there is exactly one such prime above $p$, its residue degree is one, and its valuation on $\alpha$ is $4v_p(X)$. Unique ideal factorization and class number one give \[ Z+\theta^2Y=\eps^j\beta^4,\qquad \beta=a+b\theta+c\theta^2,\quad j\in\{0,1,2,3\}. \] The negative unit sign is excluded by the norm. Since $a$ is odd, $\beta^4=1$ modulo $2\mathcal O_K$; the missing $\theta$ coefficient then forces $j$ even. Moreover $\gcd(a,b,c)=1$. The lemma therefore leaves only the following primitive representatives: \[ \begin{array}{c|c|r|l} j&(a,b,c)&N\beta&\eps^j\beta^4\\\hline 0&(1,0,0)&1&1\\ 0&(0,0,1)&4&4\theta^2\\ 0&(0,2,-1)&12&96-60\theta^2\\ 2&(1,0,-1)&-3&-3+3\theta^2 \end{array} \] Since $|X|=|N\beta|$ and $\gcd(X,6)=1$, only the first row survives. Thus $(X,Y,Z)=(\pm1,0,1)$, proving the theorem.\hfill$\square$ \subsection*{Proof of the quartic-point lemma} \textbf{1. Elliptic maps and descent.} For a point of $C_j$, put \[ \beta=a+b\theta+c\theta^2,\quad n=N\beta,\quad v=n/\beta^3,\quad s=\frac{\theta^2Y-Z}{\theta^2Y+Z},\quad \eps^j\beta^4=Z+\theta^2Y. \] Taking norms gives $4v^4=\eps^{3j}(1+3s^2)$. Thus \[ \phi_j:C_j\longrightarrow E_j:\ V^2=U^3-36\eps^jU, \qquad (U,V)=(12\eps^{-j}v^2,36sv). \] Writing $h=n/\beta$, its homogeneous coordinates are \[ [12\eps^{-j}h^2\beta^2:36\eps^{-j}(\theta^2Y-Z)h:\beta^6]. \] They have no common zero modulo $127$: if a conjugate of $\beta$ vanishes, no second conjugate can vanish, and the middle coordinate is nonzero. The quartics are smooth modulo $127$, as checked by computing the Gr\"obner basis $[1]$ for each chart's ideal generated by the equation and its partial derivatives. Full $2$-descent on $V^2=U(U-r)(U+r)$ uses $(U,U-r)$ modulo squares. Only the square classes generated by $-1,\eps,\theta,1+\theta$ can occur. The $256$ candidate pairs are tested at $2,3,\infty$. Above $2$, the local image has dimension $5$ and is certified by unit-square enumeration modulo $8$ and five independent local point classes. Above $3$ its dimension is $2$, generated by torsion; at infinity the two signs agree. Exactly $16$ and $8$ global pairs survive for $E_0$ and $E_2$ respectively. Together with full $2$-torsion, these classes are spanned by \[ \begin{split} P&=(12,36),\quad R=(4+2\theta+\theta^2,\,6+6\theta^2)\quad\text{on }E_0,\\ Q&=(-3,\,15+12\theta+6\theta^2)\quad\text{on }E_2. \end{split} \] With masks ordered by $(-1,\eps,\theta,1+\theta)$, their classes are \[ \begin{array}{c|cccc} &T_0&T_+&P\text{ or }Q&R\\\hline E_0&(1,15)&(14,4)&(10,14)&(0,2)\\ E_2&(1,13)&(12,4)&(11,1)&- \end{array} \] The Kummer injection, local quotient dimensions and Mordell--Weil theorem therefore give ranks $2,1$ and finite odd index for these generated subgroups. The finite odd-index subgroups obtained here suffice for the reduction argument. \textbf{2. The complete residue sieve.} The roots of $T^3-2$ modulo $127$ are $32,100,122$. Each elliptic reduction has $128$ points. In their threefold product, the generated subgroups have orders $4096$ and $128$. Their quotients are $2$-groups, so odd global index implies that these subgroups are the complete global reduction images. Exhaustive projective enumeration gives $128$ points on each $C_j(\F_{127})$; only \[ C_0:\ (1:0:0),(0:1:63),(0:0:1),\qquad C_2:\ (1:0:126) \] map into the appropriate subgroup. Every rational point is in one of these four residue disks. \textbf{3. One rational point in each disk.} Use $\omega=dU/(2V)$ and the three elliptic logarithms at $127$. Normalized generator logarithms modulo $127$ are \[ P:(97,97,97),\qquad R:(82,59,46),\qquad Q:(115,40,83). \] Exact logarithms give integral annihilators of the full global groups reducing to $c_0=(9,63,55)$ and $c_2=(0,83,87)$. Existence follows by taking cross products; the displayed residues prove these annihilators primitive. The logarithms are certified using $\log G=\log([128]G)/128$ and $\log(\tau)=\tau+O(\tau^5)$, $\tau=-U/V$, computed modulo $127^3$. The exact pullback is $\phi_j^*\omega=\eps^{-j}dv/(3s)$. Its coefficients are \[ \begin{array}{c|c|c|c} &\text{point}&\text{parameter}&\text{combined derivative mod }127\\\hline C_0&(1:0:0)&c/a&3\\ C_0&(0:2:-1)&c/b+1/2&97\\ C_0&(0:0:1)&a/c&82\\ C_2&(1:0:-1)&c/a+1&55 \end{array} \] All four charts and maps are integral and regular, with unit dependent-coordinate partials and unit elliptic $V$-coordinates at their centers. Consequently the annihilating logarithm on each disk, centered at its known point, has expansion \[ F(T)=uT+\sum_{n\ge2}\frac{a_{n-1}}nT^n, \quad u\in\Z_{127}^{\times},\quad a_{n-1}\in\Z_{127},\quad T\in127\Z_{127}. \] It vanishes at every rational point. If $T\ne0$, then $n v_{127}(T)-v_{127}(n)>v_{127}(T)$ for every $n\ge2$; the linear term strictly dominates the convergent tail. Hence $F(T)=0$ forces $T=0$. Each surviving disk contains just its known rational point, proving the lemma. \hfill$\square$ \subsection*{Certificates} Appendices A--F give the data, checking procedures, and explicit theorem inputs; Appendix G prints the complete verifier source. All four verifiers were rerun successfully for this edition. The proof combines the stated standard theorems with these exact finite checks. \begin{thebibliography}{G} \setlength{\itemsep}{2pt} \bibitem[S]{Stoll} M. Stoll, \emph{Implementing 2-descent for Jacobians of hyperelliptic curves}, Acta Arith. \textbf{98} (2001), 245--277, especially Lemmas 4.1--4.4. \bibitem[B]{Bruin} N. Bruin, \emph{Chabauty methods using elliptic curves}, J. Reine Angew. Math. \textbf{562} (2003), 27--49. \bibitem[G]{Grechuk} B. Grechuk, \emph{A systematic approach to Diophantine equations: open problems}, arXiv:2404.08518v9 [math.GM], 30 August 2026, Table~4, p.~4. \url{https://arxiv.org/abs/2404.08518v9}. DOI: \href{https://doi.org/10.48550/arXiv.2404.08518}{10.48550/arXiv.2404.08518}. \end{thebibliography} \clearpage \appendix \section{Scope, dependencies, and reading guide}\label{app:scope} This appendix supplies all witnesses, finite checking rules, and \emph{complete verifier source}. The code regenerates its three certificates directly from the printed constants. All listings are inline in the standalone LaTeX source. The distributed PDF's ZIP attachment is an optional byte-exact copy. \begin{center} \begin{tabular}{@{}p{0.12\linewidth}p{0.69\linewidth}r@{}} \toprule Appendix & Contents & Page\\\midrule B & Cubic-field arithmetic, quartic equations, and smoothness & \pageref{app:algebra}\\ C & Local witnesses and complete $2$-descent certificates & \pageref{app:descent}\\ D & Full reduction sieve at $127$: finite groups and enumeration & \pageref{app:sieve}\\ E & Logarithm, differential, and residue-disk certificates & \pageref{app:adic}\\ F & Reproduction instructions, checksums, and execution record & \pageref{app:repro}\\ G & Complete source for the arithmetic module and four verifiers & \pageref{app:source}\\ \bottomrule \end{tabular} \end{center} \subsection*{Standard mathematical inputs} The document is computationally self-contained relative to the following standard results, which provide the theoretical framework for the finite calculations. The references [S] and [B] are the Stoll and Bruin papers identified on page 3. \textbf{Number-field arithmetic.} Unique factorization of ideals in the ring of integers, the norm formula for principal ideals, and Minkowski's ideal-class bound. The specific ring of integers, class number, and unit group are justified in the main proof, with their finite checks in Appendix B. At the ramified primes the indicated Eisenstein generators are uniformizers and generate the local integer rings. \textbf{Elliptic descent.} Mordell--Weil finite generation and the split-cubic Kummer injection \[ E(F)/2E(F)\hookrightarrow(F^\times/F^{\times2})^2,\qquad (U,V)\longmapsto(U,U-r) \] for $E:V^2=U(U-r)(U+r)$, with the special torsion values in Appendix C. For a finite extension $F/\Q_p$ and full rational $2$-torsion, the dimension of $E(F)/2E(F)$ is $2$ when $p\ne2$ and $[F:\Q_2]+2$ when $p=2$. These are the Kummer and local quotient results used from [S, Lemmas 4.1--4.4]. The local points in Appendix C give images of exactly these dimensions. \textbf{Local lifting and reduction.} Hensel's lemma, reduction as a group homomorphism at good primes, and the local analytic parametrization of a smooth point with a unit partial derivative. A square root modulo $8$ of the units used below lifts because $v_\theta(8)=9>2v_\theta(2)=6$. \textbf{Elliptic logarithms.} At a good prime the formal elliptic logarithm extends to a homomorphism to the local field and kills torsion. Its derivative is the invariant differential. The three embeddings at the completely split prime $127$ give the elliptic Chabauty construction of [B]. Appendix E gives the exact precision calculation and the elementary zero-count argument used here. \subsection*{Verification framework} The verifier checks exact identities, finite lists, group arithmetic, and the specified truncations of formal logarithms using Python exact integers and fractions together with SymPy symbolic polynomial arithmetic. The written proof combines these checks with the standard results listed above. The argument is unconditional and all-heights, and the Kummer mask of $R$ used throughout is $(0,2)$. \clearpage \section{Cubic-field and plane-curve certificates}\label{app:algebra} Represent $a+b\theta+c\theta^2\in K$, $\theta^3=2$, by $(a,b,c)$, with rational coefficients. All field operations in the listings use \begin{align*} (a,b,c)(d,e,f)&=(ad+2bf+2ce,\ ae+bd+2cf,\ af+be+cd),\\ \NP(a,b,c)&=a^3+2b^3+4c^3-6abc,\\ (a,b,c)^{-1}&=\frac{(a^2-2bc,\ 2c^2-ab,\ b^2-ac)}{\NP(a,b,c)}. \end{align*} The last formula is used only for a nonzero element. Multiplying by the numerator checks it directly. The determinant of the multiplication matrix independently gives the norm formula. Set $\varpi=1+\theta$ (called \code{PI3} in the code). The finite field facts are \[ \operatorname{disc}(T^3-2)=-108,\quad \varpi^3=3\eps,\quad \NP\theta=2,\quad\NP\varpi=3, \quad \eps(\theta-1)=1,\quad\NP\eps=1. \] The rational inequalities $\pi>25/8$ and $\sqrt{108}<52/5$ yield the bound \[ \frac4\pi\frac6{27}\sqrt{108}<\frac{3328}{1125}<3. \] The eight norms used in the fundamental-unit check are \[ \begin{array}{c|rrrrrrrr} (a,b,c)&(0,0,0)&(0,0,1)&(0,1,0)&(0,1,1)&(1,0,0)&(1,0,1)&(1,1,0)&(1,1,1)\\\hline \NP(a,b,c)&0&4&2&6&1&5&3&1 \end{array} \] Only $1$ and $\eps$ have norm one in this list. Together with the embedding bounds explained in the main proof, this is the unit certificate. \subsection*{The two quartics and explicit coefficient formulas} The coefficient of $\theta$ in $\eps^j\beta^4$, for $\beta=a+b\theta+c\theta^2$, is twice the following form: \begin{align*} f_0={}&2a^3b+6a^2c^2+12ab^2c+b^4+8bc^3,\\ f_2={}&2a^4+10a^3b+12a^3c+18a^2b^2+48a^2bc+30a^2c^2\\ &+16ab^3+60ab^2c+72abc^2+32ac^3\\ &+5b^4+24b^3c+48b^2c^2+40bc^3+12c^4. \end{align*} The verifier expands the fourth power independently modulo $T^3-2$ and checks these two coefficient identities and $\NP(\eps^j\beta^4)=\NP(\beta)^4$. \subsection*{Geometric smoothness} For each $j=0,2$ and each of the three charts $a=1$, $b=1$, $c=1$, form the ideal generated over $\F_{127}$ by $f_j$ and its three partial derivatives, restricted to that chart. The six Gr\"obner basis computations all return $[1]$. Thus no geometric singularity exists in any chart, even over an extension of $\F_{127}$. The exact commands are printed in \code{verify_algebra.py}, Appendix~\ref{src:algebra}. The maps in the main proof use \[ h=\frac{\NP\beta}{\beta} =(a^2-2bc)+(2c^2-ab)\theta+(b^2-ac)\theta^2. \] The same module checks the norm, adjugate, curve, elliptic-map, and final reconstruction identities symbolically. Appendix D describes the reduction of the maps even at a vanishing conjugate of $\beta$. \clearpage \section{Complete local and global 2-descent data}\label{app:descent} Write $r_j=6\eps^{j/2}$, so $E_j:V^2=U(U-r_j)(U+r_j)$. For $T_0=(0,0)$ and $T_+=(r_j,0)$, the Kummer pairs are \[ \delta(T_0)=(-r_j^2,-r_j),\qquad \delta(T_+)=(r_j,2r_j^2). \] Away from $2,3$, differences of the three root factors are units; their valuations are even. If $v(U)<0$, the curve equation likewise makes $v(U)$ even. Class number one and the unit group therefore leave the $16$ square classes generated, in this order, by \[ (-1,\eps,\theta,\varpi). \] A mask $m=\sum_{i=0}^3m_i2^i$ represents the corresponding product with exponents $m_i\in\{0,1\}$. There are $256$ ordered candidate pairs. \subsection*{Square classes above 2 and 3} In $R_8=(\Z/8\Z)[T]/(T^3-2)$, a triple is a unit exactly when its constant coefficient is odd. Enumerate all $256$ units and square each one. There are $16$ distinct unit squares. The units \[ 1+\theta^2,\quad1+2\theta^2,\quad1+\theta,\quad\eps \] give disjoint square cosets, encoded by bits $1,2,4,8$; the $16$ cosets cover every unit. Append valuation parity as bit $16$. A Kummer pair with local labels $c,d$ is encoded as $c+32d$. These conventions are fixed throughout. Above $3$ use uniformizer $\varpi$ and residue field $\F_3$. A nonsquare unit has label $1$ and odd valuation has label $2$; encode pairs as $c+4d$. The global basis has the following local labels and sign bits: \[ \begin{array}{c|rrrr} &-1&\eps&\theta&\varpi\\\hline K_2&15&8&16&4\\ K_3&1&0&1&2\\ \text{negative real sign}&1&0&0&0 \end{array} \] Products of square classes are bitwise exclusive-or. For exact valuation extraction, with the usual convention $v_p(0)=+\infty$, use \begin{align*} v_\theta(a+b\theta+c\theta^2) &=\min\{3v_2(a),3v_2(b)+1,3v_2(c)+2\},\\ v_\varpi(a+b\theta+c\theta^2) &=\min\{3v_3(a-b+c),3v_3(b-2c)+1,3v_3(c)+2\}. \end{align*} Finite entries cannot tie because they have different residues modulo $3$. The source also checks these formulas against repeated uniformizer division. \subsection*{Actual local points: all six square-root witnesses} For each listed $U$, put $F_j(U)=U(U^2-r_j^2)$ and $e=v_\theta(F_j(U))$. The table gives triples modulo $8$ for $F_j(U)/\theta^e$ and its square root. Every $e$ is even, so Hensel's lemma produces a point of $E_j(K_2)$ with that $U$-coordinate. \begin{center}\small \begin{tabular}{@{}crrrrl@{}} \toprule $j$ & $U\text{ as a triple}$ & $e$ & Unit mod $8$ & Root mod $8$ & Pair label\\\midrule 0 & $(-8,-10,-4)$ & 10 & $(1,6,5)$ & $(1,3,2)$ & 716\\ 0 & $(-8,-10,-3)$ & 6 & $(1,4,4)$ & $(1,2,0)$ & 320\\ 0 & $(-8,-8,-3)$ & 6 & $(5,4,7)$ & $(1,1,3)$ & 227\\ 2 & $(-10,2,2)$ & 16 & $(1,6,6)$ & $(1,2,1)$ & 853\\ 2 & $(-8,-4,-7)$ & 6 & $(1,2,5)$ & $(1,1,2)$ & 130\\ 2 & $(-6,10,2)$ & 20 & $(1,6,6)$ & $(1,2,1)$ & 347\\\bottomrule \end{tabular} \end{center} \clearpage \subsection*{Complete local images and global survivors} Together with the torsion labels, the preceding points span all $32$ local classes at $2$. Explicit spanning lists are \[ E_0:\ (623,540,716,320,227),\qquad E_2:\ (879,532,853,130,347). \] Each has binary rank $5$, equal to the local dimension $[K_2:\Q_2]+2$. Their complete exclusive-or spans are as follows: \begin{align*} \mathcal L_{0,2}=\{&0,51,64,115,144,163,208,227,\\ &256,307,320,371,400,419,464,483,\\ &540,559,604,623,652,703,716,767,\\ &796,815,860,879,908,959,972,1023\},\\[2pt] \mathcal L_{2,2}=\{&0,26,32,58,130,152,162,184,\\ &321,347,353,379,451,473,483,505,\\ &526,532,558,564,652,662,684,694,\\ &847,853,879,885,973,983,1005,1015\}. \end{align*} At $3$, for both curves the torsion labels $9,7$ are independent and supply all four classes: \[ \mathcal L_{0,3}=\mathcal L_{2,3}=\{0,7,9,14\}. \] At the real place, the two signs of $(U,U-r_j)$ agree. For a global mask $m$, let $\lambda_2(m)$ and $\lambda_3(m)$ be the exclusive-or sums of the labels in the preceding basis table. Test each $(m,n)\in\{0,\ldots,15\}^2$ by \[ \lambda_2(m)+32\lambda_2(n)\in\mathcal L_{j,2},\qquad \lambda_3(m)+4\lambda_3(n)\in\mathcal L_{j,3},\qquad m\equiv n\pmod2. \] The surviving global pairs are exactly \[ \begin{array}{c|rrrr} E_0&(0,0)&(0,2)&(1,13)&(1,15)\\ &(4,8)&(4,10)&(5,5)&(5,7)\\ &(10,12)&(10,14)&(11,1)&(11,3)\\ &(14,4)&(14,6)&(15,9)&(15,11)\\\hline E_2&(0,0)&(1,13)&(6,8)&(7,5)\\ &(10,12)&(11,1)&(12,4)&(13,9) \end{array} \] The actual global points have masks \[ \begin{array}{c|rrrr} &T_0&T_+&P\text{ or }Q&R\\\hline E_0&(1,15)&(14,4)&(10,14)&(0,2)\\ E_2&(1,13)&(12,4)&(11,1)&- \end{array} \] and their spans are exactly these lists. The local map on the four global basis classes is injective at $2$ (its image has size $16$), so the local labels uniquely identify their global masks. The Kummer injection and Mordell--Weil finite generation now give ranks $2,1$. The displayed points together with the full $2$-torsion generate modulo $2E_j(K)$, and hence a subgroup of finite odd index. These finite odd-index subgroups suffice for the reduction argument. All enumeration and spanning checks are printed in \code{verify_descent.py}, Appendix~\ref{src:descent}. \clearpage \section{Complete reduction sieve at 127}\label{app:sieve} The three roots of $T^3-2$ modulo $127$ are ordered as $(32,100,122)$. For a root $t$, put $e_t=1+t+t^2$ and \[ B_{j,t}=-36e_t^j\pmod{127}. \] The corresponding elliptic curve is $V^2=U^3+B_{j,t}U$. Each of the four distinct coefficients below gives a group of order $128$. The listed $S,T$ have orders $64,2$ and give a bijection $(n,e)\mapsto nS+eT$ from $\Z/64\Z\times\Z/2\Z$ onto the whole group. \begin{center} \begin{tabular}{@{}ccrrr@{}} \toprule $j$ & Root $t$ & $B_{j,t}$ & $S$ & $T$\\\midrule 0 & $32,100,122$ & 91 & $(4,38)$ & $(0,0)$\\ 2 & 32 & 63 & $(4,58)$ & $(0,0)$\\ 2 & 100 & 33 & $(1,62)$ & $(0,0)$\\ 2 & 122 & 126 & $(4,21)$ & $(0,0)$\\\bottomrule \end{tabular} \end{center} The verifier enumerates every affine point and the point at infinity. It checks every ordered pair in each group against both chord-and-tangent and Jacobian-projective addition, using the displayed cyclic coordinates. \subsection*{Global generators in the product of the three reductions} Each row below is a six-tuple $(n_1,e_1,n_2,e_2,n_3,e_3)$ in the preceding bases. Thus the complete generated subgroups can be reconstructed by integer addition modulo $(64,2,64,2,64,2)$ alone. \[ \begin{array}{c|c|rrrrrr|r} j&\text{point}&n_1&e_1&n_2&e_2&n_3&e_3&\text{order}\\\hline 0&T_0&0&1&0&1&0&1&2\\ 0&T_+&32&1&32&1&32&1&2\\ 0&P&51&1&51&1&51&1&64\\ 0&R&4&0&42&0&44&0&32\\\hline 2&T_0&0&1&0&1&0&1&2\\ 2&T_+&32&1&32&1&32&1&2\\ 2&Q&61&0&59&0&5&0&64 \end{array} \] The affine generator reductions, providing a separate check on the encoding, are \[ \begin{array}{c|c|ccc} j&\text{point}&t=32&t=100&t=122\\\hline 0&T_0&(0,0)&(0,0)&(0,0)\\ 0&T_+&(6,0)&(6,0)&(6,0)\\ 0&P&(12,36)&(12,36)&(12,36)\\ 0&R&(76,54)&(44,62)&(19,29)\\\hline 2&T_0&(0,0)&(0,0)&(0,0)\\ 2&T_+&(119,0)&(27,0)&(126,0)\\ 2&Q&(124,66)&(124,1)&(124,105) \end{array} \] Enumerating the coefficient ranges determined by the final column gives $|H_0|=4096$ and $|H_2|=128$. An independent construction by successive subgroup cosets produces the same subsets and the same orders. Both ambient groups have order $128^3$. If $I$ is the odd index obtained from descent, every global reduction has class killed by $I$ in the quotient by $H_j$. That quotient is a $2$-group, so multiplication by $I$ is invertible. Thus $H_j$ is the \emph{full} global reduction image. \clearpage \subsection*{Exhaustive projective enumeration and map evaluation} Use exactly these $127^2+127+1=16257$ projective representatives: \[ (1,b,c)\ (0\le b,c<127),\qquad (0,1,c)\ (0\le c<127),\qquad(0,0,1). \] For each representative evaluate $f_j$ modulo $127$. There are exactly $128$ zeros for each $j$. For each zero, compute its image in the three elliptic curves and test membership in $H_j$, including every projective representative. Here is a complete field-coordinate rule for the image. Compute \[ \alpha=\eps^j\beta^4=Z+\theta^2Y, \quad n=\NP\beta, \quad b_t=a+bt+ct^2, \quad e_t=1+t+t^2 \] in the residue fields. When all $b_t$ are nonzero, set \[ v_t=n b_t^{-3},\qquad s_t=(t^2Y-Z)(Z+t^2Y)^{-1},\qquad \phi_{j,t}=(12e_t^{-j}v_t^2,36s_tv_t). \] All inverses in this display are taken modulo $127$. \textbf{Zero conjugates are included.} At most one $b_t$ can vanish: two vanishing conjugates of $\alpha$ force $Y=Z=0$, and then every conjugate of $\beta$ vanishes, contrary to the projective point condition. If $b_t=0$, its image is the elliptic point at infinity; at the other two embeddings, $n=0$ and the image is $(0,0)$. This rule is also verified directly by the homogeneous map \[ [12\eps^{-j}h^2\beta^2: 36\eps^{-j}(\theta^2Y-Z)h: \beta^6]. \] At a zero conjugate of $\beta$, the corresponding $h$ is nonzero and $\theta^2Y-Z=2\theta^2Y\ne0$, so these three coordinates never vanish simultaneously. When $\beta\ne0$, the last coordinate is nonzero. This is why the map can be reduced without losing a rational point at an apparent pole. For another independent image calculation, let $\alpha_t=e_t^j b_t^4$. Interpolate \[ Y=\frac{\alpha_{100}-\alpha_{32}}{100^2-32^2},\qquad Z=\alpha_{32}-32^2Y \] and verify $\alpha_t=Z+t^2Y$ at all three embeddings. Then use the same elliptic formulas with $n=b_{32}b_{100}b_{122}$. The field multiplication, interpolation, and homogeneous-coordinate methods agree at every curve point. \begin{center} \begin{tabular}{@{}ccl@{}} \toprule Curve & Total zeros & Zeros whose image belongs to $H_j$\\\midrule $C_0$ & 128 & $(1:0:0),\ (0:1:63),\ (0:0:1)$\\ $C_2$ & 128 & $(1:0:126)$\\\bottomrule \end{tabular} \end{center} Appendix~\ref{src:sieve} prints \code{verify_finite_sieve.py} in full, including all additions and exceptional cases. It regenerates all $256$ point images in \code{finite_sieve_certificate.json}. This large derived list is generated directly by the verifier. \clearpage \section{Logarithm and local completeness certificates}\label{app:adic} Put $p=127$ and $M=p^3=2048383$. Newton lifting and digit-by-digit lifting of the three simple roots give the same values: \[ \begin{array}{c|rrr} \text{modulus}&\text{first root}&\text{second root}&\text{third root}\\\hline 127&32&100&122\\ 127^2&2699&100&13330\\ 127^3&1422051&403325&223007 \end{array} \] For a root correct modulo $m=p^k$, the update is \[ r\longmapsto r-m\left(\frac{r^3-2}{m}\right)(3r^2)^{-1} \pmod{mp}, \] where the inverse multiplying the quotient is taken modulo $p$. The second algorithm tests all $p$ candidates $r+dm$ for the next digit. \subsection*{Why the stated precision suffices} On $V^2=U^3+BU$, take $\tau=-U/V$ at infinity. Direct differentiation gives \[ \frac{dU}{2V}=\frac{d\tau}{\sqrt{1-4B\tau^4}}, \qquad \log(\tau)=\tau+O(\tau^5). \] Each finite elliptic group has order $128$, so $\log G=\log([128]G)/128$. For $[128]G$ the parameter $\tau$ is divisible by $p$. Therefore $\tau$ modulo $p^3$ determines $\log G/p$ modulo $p^2$. The higher terms have valuation greater than three. Equivalently, the formal series is obtained by integrating $\sum_{n\ge0}\binom{2n}{n}B^n\tau^{4n}$; every omitted term is $\binom{2n}{n}B^n\tau^{4n+1}/(4n+1)$ with $n\ge1$. \subsection*{Two computations of \texorpdfstring{$[128]G$}{[128]G}} The first uses seven doublings in Jacobian projective coordinates $(X:Y:Z)$, with affine coordinates $(X/Z^2,Y/Z^3)$. At each step set \[ S=4XY^2,\quad D=3X^2+BZ^4,\quad X'=D^2-2S,\quad Y'=D(S-X')-8Y^4,\quad Z'=2YZ. \] The source checks $Y'^2=X'^3+BX'Z'^4$ modulo $M$ after every doubling, then uses $\tau=-XZ/Y$. The second computation uses the division-polynomial recurrences, printed in full in Appendix~\ref{src:chabauty}; all nine resulting values agree. The normalized logarithms are \[ \begin{array}{c|rrr|c} G&\multicolumn{3}{c|}{\log(G)/127\pmod{127^2}}&\pmod{127}\\\hline P&15210&15210&15210&(97,97,97)\\ R&1479&8949&7539&(82,59,46)\\ Q&12688&14137&3766&(115,40,83) \end{array} \] Take the cross product of the \emph{exact} normalized logarithm vectors of $P,R$, or of $Q$ and $(1,0,0)$. The resulting integral annihilators reduce to \[ c_0=(9,63,55),\qquad c_2=(0,83,87). \] They are primitive because their reductions are nonzero. Their exact vectors, annihilate the global logarithm spaces exactly. The ranks and finite-index assertions proved in Appendix C justify that last statement for every global point. \clearpage \subsection*{The four local derivatives} In each chart, the free coordinate centered at the indicated rational point is a local parameter $T$; the unit dependent-coordinate partial derivative ensures this by the implicit function theorem. Tangents are listed as triples $(da/dT,db/dT,dc/dT)$. \[ \begin{array}{c|c|c|c|r|c} j&(a,b,c)&\text{chart}&T&\partial f_j/\partial\text{(dependent)}&\text{tangent}\\\hline 0&(1,0,0)&a=1&c&2\ (b)&(0,0,1)\\ 0&(0,1,-1/2)&b=1&c+1/2&-6\ (a)&(1,0,1)\\ 0&(0,0,1)&c=1&a&8\ (b)&(1,0,0)\\ 2&(1,0,-1)&a=1&c+1&-6\ (b)&(0,0,1) \end{array} \] For $n=\NP\beta$ and $v=n/\beta^3$, differentiate in $K$: \[ dv=v\left(\frac{dn}{n}-3\frac{d\beta}{\beta}\right),\qquad \phi_j^*\omega=\eps^{-j}\frac{dv}{3s}. \] The exact coefficients, their three embeddings, and their dot products with the appropriate annihilator are \[ \begin{array}{c|c|c|c|r} j&(a:b:c)&\text{exact coefficient in }K&\text{embeddings mod }127&c_j\cdot\text{embeddings}\\\hline 0&(1:0:0)&\theta^2&(8,94,25)&3\\ 0&(0:2:-1)&(2-\theta)/3&(117,52,87)&97\\ 0&(0:0:1)&-\theta/2&(111,77,66)&82\\ 2&(1:0:-1)&(2\theta-\theta^2)/3&(61,120,73)&55 \end{array} \] Implicit differentiation and symbolic differentiation of the field-valued rational map give the same coefficients. The code also checks that every conjugate of $\beta$ and every elliptic $V$-coordinate at these centers is a unit modulo $127$. Thus the maps and differentials are integral and regular throughout the four residue disks. \subsection*{The analytic implication in full} Compose the three elliptic logarithms with the exact integral annihilator. On a disk centered at its known rational point, this function vanishes at the center and at every other rational point. The integral pullback differential has a unit constant coefficient, so its integral has the expansion \[ F(T)=uT+\sum_{n\ge2}\frac{a_{n-1}}nT^n,\qquad u\in\Z_{127}^\times,\quad a_{n-1}\in\Z_{127},\quad T\in127\Z_{127}. \] For $T\ne0$ and $n\ge2$, \[ v_{127}\!\left(\frac{a_{n-1}}nT^n\right) \ge n\,v_{127}(T)-v_{127}(n)>v_{127}(T). \] These valuations also tend to infinity, proving convergence. The ultrametric inequality then implies that the sum of the higher terms has strictly larger valuation than $uT$. Consequently $F(T)\ne0$ whenever $T\ne0$. Each disk contains only its center. Appendix D exhausts the possible disks, so the two rational-point classifications in the main proof follow. All finite arithmetic for this section is in \code{verify_chabauty.py}. The general existence and homomorphism properties of the logarithm, and its relation to the invariant differential, are the standard inputs stated in Appendix A, together with the exact computations recorded here. \clearpage \section{Reproduction and execution record}\label{app:repro} \subsection*{Files and running instructions} Appendix G prints all six Python files required to regenerate the checks. Save each listing under its stated filename in one directory. The environment needs Python 3.10 or later and SymPy 1.12 or later, as in the supplied package. This edition was rerun with Python 3.13.5 and SymPy 1.14.0. The sole line in \code{requirements.txt} is \begin{lstlisting}[style=plain] sympy>=1.12 \end{lstlisting} Run, with assertions enabled, \begin{lstlisting}[style=plain] python run_all.py \end{lstlisting} Do not use \code{python -O} or \code{python -OO}: the checks deliberately use \code{assert}. Each script can also be run separately. Successful runs regenerate \code{descent_certificate.json}, \code{finite_sieve_certificate.json}, and \code{chabauty_certificate.json}, plus the four stage logs. The distributed PDF has a ZIP attachment containing byte-exact source copies, regenerated certificates, logs, and a SHA-256 manifest. Recompiling the single LaTeX file reproduces the printed proof and listings without an attachment; all executable content is inline. The accompanying source archive contains an extraction utility, but saving the six listings by hand is sufficient. \subsection*{What was rerun for this edition} All four verifiers completed successfully. The code is unchanged from the supplied verification package; in particular, it already uses the corrected mask pair $(0,2)$ for $R$. The following excerpt records the successful execution: \begin{lstlisting}[style=plain] ALL ALGEBRAIC CERTIFICATE CHECKS PASSED. PASS E0: local-image sizes 32 and 4; 16 global survivors. generator square-class pairs: [('T0', (1, 15)), ('Tplus', (14, 4)), ('P', (10, 14)), ('R', (0, 2))] PASS E2: local-image sizes 32 and 4; 8 global survivors. ALL DESCENT CERTIFICATE CHECKS PASSED. PASS C0: all 16257 projective residue points checked; 128 lie on the curve. PASS E0: each finite elliptic group has 128 points; both subgroup methods give 4096. PASS E2: each finite elliptic group has 128 points; both subgroup methods give 128. ALL FINITE SIEVE CHECKS PASSED. ALL CHABAUTY FINITE CERTIFICATE CHECKS PASSED. ALL FOUR VERIFIERS PASSED. The primitive solutions are exactly (1,0,-1) and (-1,0,-1). \end{lstlisting} Long lines in this excerpt have been wrapped for display. The byte-exact full log is included with the sources. The arithmetic is repeated in independent implementations within the package as a consistency check. \clearpage \subsection*{SHA-256 checksums of the complete source listings} The six executable files printed in Appendix G have the following SHA-256 checksums. The companion archive and PDF attachment contain these exact bytes. The PDF adds only typographic line wrapping and printed line numbers to these byte-exact files. \textbf{\code{arith.py}} \begin{lstlisting}[style=plain] 5dbdfc5f6f5073ed2510d1f98c8fcd0663a4fa3e5a2672a460193ba5b0dc6cbd \end{lstlisting} \textbf{\code{verify_algebra.py}} \begin{lstlisting}[style=plain] f18dc239ad96c012d87e8ecfbeb5a82995b6fc79381308c62daf014d83905809 \end{lstlisting} \textbf{\code{verify_descent.py}} \begin{lstlisting}[style=plain] c5e5293b48343ee0d13f379382c4d2ab49de94a229406d3b4092a8f71ae3369e \end{lstlisting} \textbf{\code{verify_finite_sieve.py}} \begin{lstlisting}[style=plain] 4fafe55809d9a1f475ad7314a7515fe62f747cb7bcca1b02ecdb937ceac4206b \end{lstlisting} \textbf{\code{verify_chabauty.py}} \begin{lstlisting}[style=plain] fb54220131b7364678c29670318d4b50ea8399feb97e16a7457a58148b1878c9 \end{lstlisting} \textbf{\code{run_all.py}} \begin{lstlisting}[style=plain] fdc7d71ddcc118062f2912f07bb4c9d7f50fc211de3f07d6f243045323f762c0 \end{lstlisting} \subsection*{How the checks fit together} \begin{center} \begin{tabular}{@{}p{0.30\linewidth}p{0.64\linewidth}@{}} \toprule Module & Role\\\midrule \code{arith.py} & Exact $K$-arithmetic, valuations, local square-class encodings, quartic forms, and global elliptic points.\\[3pt] \code{verify_algebra.py} & Norm and power identities; field and unit witnesses; geometric smoothness in all charts; elliptic-map and final reconstruction checks.\\[3pt] \code{verify_descent.py} & All unit products; local square-root witnesses; local images; all $256$ global candidate pairs; spans from actual global points.\\[3pt] \code{verify_finite_sieve.py} & All finite group additions; both subgroup constructions; every projective residue point; all three map computations, including zero-conjugate cases.\\[3pt] \code{verify_chabauty.py} & Two root lifts; two multiplication/logarithm computations; exact and reduced pullback derivatives; unit checks.\\[3pt] \code{run_all.py} & Executes each verification stage, records its output, and stops on failure.\\\bottomrule \end{tabular} \end{center} The final implication is mathematical: fourth-power descent places every primitive integer solution on one of the two quartics; elliptic descent and finite reduction confine every rational quartic point to one of four disks; the local zero argument leaves only the four known points; and their norm values leave only $(1,0,-1)$ and $(-1,0,-1)$. The appendix records every finite computation in this chain, and the proof combines those exact checks with the standard theorems listed in Appendix A. \clearpage \section{Complete verification source}\label{app:source} These are the complete executable source files. They reproduce all finite tables and certificates from their own constants. Printed line numbers and wrap arrows are layout aids only. \subsection{\texorpdfstring{\texttt{arith.py}}{\detokenize{arith.py}}}\label{src:arith} % BEGIN VERIFIER FILE: arith.py \begin{lstlisting}[style=source] """Exact arithmetic in Q(theta), theta^3=2.""" from fractions import Fraction as F from itertools import product ZERO = (F(0), F(0), F(0)) ONE = (F(1), F(0), F(0)) THETA = (F(0), F(1), F(0)) EPS = (F(1), F(1), F(1)) PI3 = (F(1), F(1), F(0)) def elt(a=0, b=0, c=0): return (F(a), F(b), F(c)) def add(x, y): return tuple(a+b for a,b in zip(x,y)) def neg(x): return tuple(-a for a in x) def sub(x, y): return add(x, neg(y)) def scale(x, k): return tuple(a*k for a in x) def mul(x, y): a,b,c=x; d,e,f=y return (a*d+2*(b*f+c*e), a*e+b*d+2*c*f, a*f+b*e+c*d) def norm(x): a,b,c=x return a**3+2*b**3+4*c**3-6*a*b*c def inv(x): a,b,c=x; n=norm(x) if n == 0: raise ZeroDivisionError('zero field element') return ((a*a-2*b*c)/n, (2*c*c-a*b)/n, (b*b-a*c)/n) def div(x,y): return mul(x,inv(y)) def power(x,n): if n < 0: return power(inv(x),-n) out=ONE while n: if n&1: out=mul(out,x) x=mul(x,x); n//=2 return out def ev(x, root, modulus): out=0 for i,a in enumerate(x): a=F(a) out += a.numerator*pow(a.denominator,-1,modulus)*pow(root,i,modulus) return out%modulus def residue(x,modulus): return tuple(F(a).numerator*pow(F(a).denominator,-1,modulus)%modulus for a in x) def bitspan(vectors): out={0} for v in vectors: out |= {a^v for a in list(out)} return out def image(mask, labels): out=0 for i,a in enumerate(labels): if (mask>>i)&1: out ^= a return out def rational_valuation(a,p): a=F(a) if not a: return 10**9 n,d=abs(a.numerator),a.denominator v=0 while n%p==0: n//=p; v+=1 while d%p==0: d//=p; v-=1 return v class LocalClasses: """Square classes in K_2 and K_3, with exhaustive mod-8 certificates.""" def __init__(self): self.units=[(a,b,c) for a in range(1,8,2) for b in range(8) for c in range(8)] self.square_roots={} for u in self.units: self.square_roots.setdefault(self.mm(u,u),u) self.squares=set(self.square_roots) self.unit_basis=[(1,0,1),(1,0,2),(1,1,0),(1,1,1)] self.labels={} for mask in range(16): rep=(1,0,0) for i,b in enumerate(self.unit_basis): if mask>>i&1: rep=self.mm(rep,b) for s in self.squares: u=self.mm(rep,s) assert u not in self.labels self.labels[u]=mask assert len(self.units)==256 and len(self.squares)==16 and len(self.labels)==256 @staticmethod def mm(a,b): return tuple(int(t)%8 for t in mul(a,b)) def normalize2(self,x): assert x!=ZERO v=min(3*rational_valuation(F(a),2)+i for i,a in enumerate(x)) unit=mul(x,power(THETA,-v)) u=residue(unit,8) assert u[0]%2 return v,u def class2(self,x): v,u=self.normalize2(x) return self.labels[u] | ((v%2)<<4) def class2_iterated(self,x): """Independent valuation extraction by repeatedly dividing by theta.""" x=tuple(map(F,x)); assert x!=ZERO v=0 while any(a.denominator%2==0 for a in x): x=scale(x,2); v-=3 while F(x[0]).numerator%2==0: a,b,c=x; x=(b,c,a/2); v+=1 return self.labels[residue(x,8)] | ((v%2)<<4) def square2_certificate(self,x): v,u=self.normalize2(x) assert v%2==0 and u in self.squares root=self.square_roots[u] assert self.mm(root,root)==u return {'valuation':v,'unit_mod8':list(u),'root_mod8':list(root)} @staticmethod def class3(x): assert x!=ZERO a,b,c=map(F,x) cs=(a-b+c,b-2*c,c) # coefficients in the uniformizer pi3=theta+1 v=min(3*rational_valuation(t,3)+i for i,t in enumerate(cs)) u=mul(tuple(map(F,x)),power(PI3,-v)) res=ev(u,2,3) assert res in (1,2) return ((v%2)<<1) | (res==2) @staticmethod def class3_iterated(x): x=tuple(map(F,x)); assert x!=ZERO v=0 while any(a.denominator%3==0 for a in x): x=scale(x,3);v-=3 ip=elt(F(1,3),F(-1,3),F(1,3)) while ev(x,2,3)==0: x=mul(x,ip);v+=1 return ((v%2)<<1) | (ev(x,2,3)==2) def curve_forms(): import sympy as s a,b,c=s.symbols('a b c') f0=2*a**3*b+6*a*a*c*c+12*a*b*b*c+b**4+8*b*c**3 f2=(2*a**4+10*a**3*b+12*a**3*c+18*a*a*b*b+48*a*a*b*c+30*a*a*c*c +16*a*b**3+60*a*b*b*c+72*a*b*c*c+32*a*c**3+5*b**4+24*b**3*c +48*b*b*c*c+40*b*c**3+12*c**4) return (a,b,c),{0:f0,2:f2} def rational_generators(j): if j==0: return [('P',(elt(12),elt(36))),('R',(elt(4,2,1),elt(6,0,6)))] if j==2: return [('Q',(elt(-3),elt(15,12,6)))] raise ValueError(j) \end{lstlisting} % END VERIFIER FILE: arith.py \Needspace{8\baselineskip} \subsection{\texorpdfstring{\texttt{verify\_algebra.py}}{\detokenize{verify_algebra.py}}}\label{src:algebra} % BEGIN VERIFIER FILE: verify_algebra.py \begin{lstlisting}[style=source] """Exact field, descent, curve, and final reconstruction identities.""" from fractions import Fraction as F from itertools import product import sympy as s from arith import * def run(): T=s.symbols('T');g=T**3-2 assert s.discriminant(g,T)==-108 assert s.expand(g.subs(T,T-1))==T**3-3*T*T+3*T-3 # Both relevant local orders are generated by Eisenstein uniformizers. for poly,p in [(g,2),(s.expand(g.subs(T,T-1)),3)]: cc=s.Poly(poly,T).all_coeffs() assert cc[0]==1 and all(int(c)%p==0 for c in cc[1:]) and int(cc[-1])%(p*p)!=0 assert norm(THETA)==2 and norm(PI3)==3 assert power(PI3,3)==scale(EPS,3) assert mul(EPS,sub(THETA,ONE))==ONE and norm(EPS)==1 assert F(4,1)/F(25,8)*F(6,27)*F(52,5)<3 assert F(52,5)**2>108 and F(13,10)**3>2 and 1+F(13,10)+F(13,10)**2<4 norm1=[q for q in product((0,1),repeat=3) if norm(q)==1] assert norm1==[(1,0,0),(1,1,1)] print('PASS: field discriminant, local Eisenstein generators, Minkowski bound <3, and unit certificate.') a,b,c=s.symbols('a b c') x=(a,b,c) matrix=s.Matrix.hstack(*(s.Matrix(mul(x,v)) for v in [ONE,THETA,power(THETA,2)])) assert s.expand(matrix.det()-norm(x))==0 adj=(a*a-2*b*c,2*c*c-a*b,b*b-a*c) assert all(s.expand(u-v)==0 for u,v in zip(mul(x,adj),(norm(x),0,0))) assert s.expand(s.rem((a+b*T+c*T*T)**4,g,T)-sum(power(x,4)[i]*T**i for i in range(3)))==0 for j in range(4): ej=power(EPS,j) assert int(ej[1])%2==j%2 print('PASS: multiplication-matrix norm and fourth-power expansion; odd unit twists are excluded modulo 2.') vars,forms=curve_forms() aa,bb,cc=vars for j in (0,2): alpha=mul(power(EPS,j),power(vars,4)) assert s.expand(alpha[1]-2*forms[j])==0 assert s.expand(norm(alpha)-norm(vars)**4)==0 for i in range(3): subchart={vars[i]:1} unknown=[v for k,v in enumerate(vars) if k!=i] equations=[forms[j].subs(subchart)]+[s.diff(forms[j],v).subs(subchart) for v in vars] gb=s.groebner(equations,*unknown,modulus=127) assert list(gb)==[1] print(f'PASS C{j}: defining quartic from the field identity; all three projective charts smooth over F_127-bar.') z,y=s.symbols('z y') assert norm((z,0,y))==z**3+4*y**3 vv,ss,e=s.symbols('v s e',nonzero=True) for j in (0,2): XX=12*e**(-j)*vv**2;YY=36*ss*vv diff=YY**2-XX**3+36*e**j*XX assert s.simplify(diff-432*vv**2*(1+3*ss**2-4*e**(-3*j)*vv**4))==0 print('PASS: both elliptic maps follow from 4v^4=eps^(3j)(1+3s^2).') expected=[(0,(1,0,0),1,(1,0,0)),(0,(0,0,1),4,(0,0,4)), (0,(0,2,-1),12,(96,0,-60)),(2,(1,0,-1),-3,(-3,0,3))] for j,beta,n,alpha in expected: assert forms[j].subs(dict(zip(vars,beta)))==0 assert norm(beta)==n and mul(power(EPS,j),power(beta,4))==alpha Z,zero,Y=alpha assert zero==0 and Z**3+4*Y**3==n**4 primitive=(abs(n)==1) print(f'PASS: C{j} beta={beta}: norm={n}, (Z,Y)=({Z},{Y}), primitive candidate={primitive}.') for X in (-1,1): assert X**4+4*0**3+(-1)**3==0 print('CONCLUSION after the certified rational-point classification: only (1,0,-1) and (-1,0,-1) are primitive.') if __name__=='__main__': run() print('ALL ALGEBRAIC CERTIFICATE CHECKS PASSED.') \end{lstlisting} % END VERIFIER FILE: verify_algebra.py \Needspace{8\baselineskip} \subsection{\texorpdfstring{\texttt{verify\_descent.py}}{\detokenize{verify_descent.py}}}\label{src:descent} % BEGIN VERIFIER FILE: verify_descent.py \begin{lstlisting}[style=source] """Finite certificates for rank E0(K)=2 and rank E2(K)=1. The accompanying proof supplies the standard Kummer and local-dimension theorems. """ import json from itertools import product from pathlib import Path from arith import * EXPECTED={ 0:[(0,0),(0,2),(1,13),(1,15),(4,8),(4,10),(5,5),(5,7),(10,12),(10,14),(11,1),(11,3),(14,4),(14,6),(15,9),(15,11)], 2:[(0,0),(1,13),(6,8),(7,5),(10,12),(11,1),(12,4),(13,9)]} WITNESSES={0:[(-8,-10,-4),(-8,-10,-3),(-8,-8,-3)], 2:[(-10,2,2),(-8,-4,-7),(-6,10,2)]} def run(): lc=LocalClasses() # Verify the whole finite unit-class homomorphism, not just chosen entries. for u in lc.units: for v in lc.units: assert lc.labels[lc.mm(u,v)]==lc.labels[u]^lc.labels[v] for a,b,c in product(range(-3,4),repeat=3): x=elt(a,b,c) if x==ZERO: continue for den in (1,2,3,6): xx=scale(x,F(1,den)) assert lc.class2(xx)==lc.class2_iterated(xx) assert lc.class3(xx)==lc.class3_iterated(xx) print('PASS: all 256 units, 16 unit squares, and all 65536 unit products checked.') print('PASS: two different uniformizer-valuation algorithms agree on 1368 test elements.') base=[elt(-1),EPS,THETA,PI3] bs2=[lc.class2(x) for x in base];bs3=[lc.class3(x) for x in base] signs=[1,0,0,0] # exact: -1<0, eps>0, theta>0, theta+1>0 assert bs2==[15,8,16,4] and bs3==[1,0,1,2] assert len(bitspan(bs2))==16 decode={image(mask,bs2):mask for mask in range(16)} print('PASS: S-unit basis (-1,eps,theta,theta+1) has local labels',bs2,bs3) report={} for j in (0,2): r=scale(EPS if j else ONE,6) tors=[('T0',(neg(power(r,2)),neg(r))),('Tplus',(r,scale(power(r,2),2)))] v2=[lc.class2(a)|(lc.class2(b)<<5) for _,(a,b) in tors] v3=[lc.class3(a)|(lc.class3(b)<<2) for _,(a,b) in tors] assert len(bitspan(v3))==4 witnesses=[] for xx in WITNESSES[j]: x=elt(*xx) fx=mul(x,sub(power(x,2),power(r,2))) cert=lc.square2_certificate(fx) pair=lc.class2(x)|(lc.class2(sub(x,r))<<5) v2.append(pair) witnesses.append({'x':list(xx),'square_certificate':cert,'kummer_label':pair}) local2=bitspan(v2);local3=bitspan(v3) assert len(local2)==32 survivors=[] for aa,bb in product(range(16),repeat=2): pair2=image(aa,bs2)|(image(bb,bs2)<<5) pair3=image(aa,bs3)|(image(bb,bs3)<<2) if pair2 in local2 and pair3 in local3 and image(aa,signs)==image(bb,signs): survivors.append((aa,bb)) assert survivors==EXPECTED[j] gens=[] for name,(a,b) in tors: gens.append((name,(decode[lc.class2(a)],decode[lc.class2(b)]))) for name,(x,y) in rational_generators(j): assert power(y,2)==mul(x,sub(power(x,2),power(r,2))) gens.append((name,(decode[lc.class2(x)],decode[lc.class2(sub(x,r))]))) global_span=bitspan([a|(b<<4) for _,(a,b) in gens]) assert global_span=={a|(b<<4) for a,b in survivors} expected_rank=2 if j==0 else 1 assert len(global_span)==2**(expected_rank+2) print(f'PASS E{j}: local-image sizes 32 and 4; {len(survivors)} global survivors.') print(' generator square-class pairs:',gens) print(f' rank={expected_rank}; displayed points and 2-torsion span E{j}(K)/2E{j}(K).') report[str(j)]={'local2_witnesses':witnesses,'local2_image':sorted(local2), 'local3_image':sorted(local3),'global_survivors':[list(s) for s in survivors], 'generators':[[n,list(pair)] for n,pair in gens], 'rank':expected_rank} return report if __name__=='__main__': report=run() Path('descent_certificate.json').write_text(json.dumps(report,indent=2)+'\n') print('ALL DESCENT CERTIFICATE CHECKS PASSED.') \end{lstlisting} % END VERIFIER FILE: verify_descent.py \Needspace{8\baselineskip} \subsection{\texorpdfstring{\texttt{verify\_finite\_sieve.py}}{\detokenize{verify_finite_sieve.py}}}\label{src:sieve} % BEGIN VERIFIER FILE: verify_finite_sieve.py \begin{lstlisting}[style=source] """Two representations verify the complete reduction sieve at 127. 1. Affine elliptic arithmetic and direct subgroup cosets. 2. Jacobian-projective arithmetic and complete Z/64 x Z/2 group tables. """ import json from itertools import product, chain from math import gcd,lcm from pathlib import Path from arith import * P=127 ROOTS=[r for r in range(P) if r**3%P==2] assert ROOTS==[32,100,122] INF=None JINF=(1,1,0) def oncurve(pt,B): return pt is None or (pt[1]**2-pt[0]**3-B*pt[0])%P==0 def affine_add(a,b,B): if a is None:return b if b is None:return a x,y=a;u,v=b if x==u: if (y+v)%P==0:return None slope=(3*x*x+B)*pow(2*y,-1,P)%P else: slope=(v-y)*pow(u-x,-1,P)%P xx=(slope*slope-x-u)%P return xx,(slope*(x-xx)-y)%P def jac_double(a,B): x,y,z=a if not z or not y:return JINF yy=y*y%P;S=4*x*yy%P;M=(3*x*x+B*pow(z,4,P))%P xx=(M*M-2*S)%P return xx,(M*(S-xx)-8*yy*yy)%P,2*y*z%P def jac_add(a,b,B): X,Y,Z=a;U,V,W=b if not Z:return b if not W:return a u1=X*W*W%P;u2=U*Z*Z%P s1=Y*W**3%P;s2=V*Z**3%P if u1==u2: return jac_double(a,B) if s1==s2 else JINF h=(u2-u1)%P;r=(s2-s1)%P xx=(r*r-h**3-2*u1*h*h)%P yy=(r*(u1*h*h-xx)-s1*h**3)%P return xx,yy,h*Z*W%P def jac_mul(n,a,B): out=JINF while n: if n&1:out=jac_add(out,a,B) a=jac_double(a,B);n//=2 return out def to_aff(a): x,y,z=a if not z:return None zi=pow(z,-1,P) return x*zi*zi%P,y*zi**3%P def to_jac(a): return JINF if a is None else(a[0],a[1],1) TABLE_CACHE={} def group_table(B): B%=P if B in TABLE_CACHE:return TABLE_CACHE[B] pts=[None]+[(x,y) for x in range(P) for y in range(P) if (y*y-x*x*x-B*x)%P==0] assert len(pts)==128 S=next(a for a in pts if a is not None and to_aff(jac_mul(64,to_jac(a),B)) is None and to_aff(jac_mul(32,to_jac(a),B)) is not None) cyc=[];a=JINF for n in range(64): cyc.append(to_aff(a));a=jac_add(a,to_jac(S),B) assert len(set(cyc))==64 and to_aff(a) is None T=next(a for a in pts if a is not None and a[1]==0 and a not in cyc) decode={};encode={} for n,a in enumerate(cyc): for e in (0,1): b=a if not e else to_aff(jac_add(to_jac(a),to_jac(T),B)) assert b not in encode encode[b]=(n,e);decode[n,e]=b assert set(pts)==set(encode) # Full addition table cross-check: every ordered pair, including torsion/O. for a in pts: na,ea=encode[a] for b in pts: nb,eb=encode[b] c=decode[((na+nb)%64,(ea+eb)%2)] assert affine_add(a,b,B)==c assert to_aff(jac_add(to_jac(a),to_jac(b),B))==c ans={'points':pts,'encode':encode,'decode':decode,'S':S,'T':T} TABLE_CACHE[B]=ans return ans def triple_add(a,b,Bs): return tuple(affine_add(x,y,B) for x,y,B in zip(a,b,Bs)) def primary_subgroup(gens,Bs): H={(None,)*3} for gen in gens: old=H;H=set(old);cur=gen while cur not in old: H.update(triple_add(h,cur,Bs) for h in old) cur=triple_add(cur,gen,Bs) return H def secondary_subgroup(gens,tables): coords=[tuple(v for T,g in zip(tables,gen) for v in T['encode'][g]) for gen in gens] orders=[] for g in coords: orders.append(lcm(*(64//gcd(g[i],64) if i%2==0 else (2 if g[i] else 1) for i in range(6)))) H=set() for ns in product(*(range(o) for o in orders)): q=tuple(sum(n*g[i] for n,g in zip(ns,coords))%(64 if i%2==0 else 2) for i in range(6)) H.add(tuple(T['decode'][q[2*i],q[2*i+1]] for i,T in enumerate(tables))) return H,coords,orders def projective_points(): return chain(((1,b,c) for b,c in product(range(P),repeat=2)),((0,1,c) for c in range(P)),[(0,0,1)]) def form_direct(beta,j): a,b,c=beta if j==0: return (2*a**3*b+6*a*a*c*c+12*a*b*b*c+b**4+8*b*c**3)%P return (2*a**4+10*a**3*b+12*a**3*c+18*a*a*b*b+48*a*a*b*c+30*a*a*c*c +16*a*b**3+60*a*b*b*c+72*a*b*c*c+32*a*c**3+5*b**4+24*b**3*c +48*b*b*c*c+40*b*c**3+12*c**4)%P def phi_primary(beta,j): alpha=mul(power(EPS,j),power(beta,4)) assert int(alpha[1])%P==0 Z,Y=int(alpha[0])%P,int(alpha[2])%P n=int(norm(beta))%P;bb=[ev(beta,r,P) for r in ROOTS] if 0 in bb: assert bb.count(0)==1 return tuple(None if not b else(0,0) for b in bb) out=[] for r,b in zip(ROOTS,bb): e=(1+r+r*r)%P v=n*pow(b,-3,P)%P s=(2*r*r*Y*pow((Z+r*r*Y)%P,-1,P)-1)%P x=12*v*v*(pow(e,-2,P) if j else 1)%P y=36*s*v%P B=-36*(e*e if j else 1)%P assert oncurve((x,y),B) out.append((x,y)) return tuple(out) def phi_secondary(beta,j): # Interpolate Z,Y from conjugate values, without multiplying in K. a,b,c=beta bs=[(a+b*r+c*r*r)%P for r in ROOTS] es=[(1+r+r*r)%P for r in ROOTS] alphas=[pow(e,j,P)*pow(bb,4,P)%P for e,bb in zip(es,bs)] Y=(alphas[1]-alphas[0])*pow(ROOTS[1]**2-ROOTS[0]**2,-1,P)%P Z=(alphas[0]-ROOTS[0]**2*Y)%P assert all((Z+r*r*Y-aa)%P==0 for r,aa in zip(ROOTS,alphas)) if 0 in bs: assert bs.count(0)==1 return tuple(None if not b else(0,0) for b in bs) n=bs[0]*bs[1]*bs[2]%P out=[] for r,e,bb,aa in zip(ROOTS,es,bs,alphas): vv=n*pow(bb,-3,P)%P ss=(r*r*Y-Z)*pow(aa,-1,P)%P out.append((12*vv*vv*(pow(e,-2,P) if j else 1)%P,36*ss*vv%P)) return tuple(out) def phi_homogeneous(beta,j): # Degree-six homogeneous coordinates give an integral morphism at 127. a,b,c=beta h=(a*a-2*b*c,2*c*c-a*b,b*b-a*c) alpha=mul(power(EPS,j),power(beta,4)) Z,Y=int(alpha[0])%P,int(alpha[2])%P out=[] for r in ROOTS: bb=ev(beta,r,P); hh=ev(h,r,P); e=(1+r+r*r)%P inv_e=pow(e,-j,P) U=12*inv_e*hh*hh*bb*bb%P V=36*inv_e*(r*r*Y-Z)*hh%P W=pow(bb,6,P) assert (U,V,W)!=(0,0,0) assert (V*V*W-U**3+36*pow(e,j,P)*U*W*W)%P==0 out.append((U*pow(W,-1,P)%P,V*pow(W,-1,P)%P) if W else None) return tuple(out) EXPECTED={0:[(1,0,0),(0,1,63),(0,0,1)],2:[(1,0,126)]} def run(): out={'prime':P,'roots':ROOTS,'curves':{}} for j in (0,2): es=[(1+r+r*r)%P for r in ROOTS] rs=[6*(e if j else 1)%P for e in es] Bs=[-r*r%P for r in rs] tables=[group_table(B) for B in Bs] gens=[((0,0),)*3,tuple((r,0) for r in rs)] gens += [tuple((ev(x,r,P),ev(y,r,P)) for r in ROOTS) for _,(x,y) in rational_generators(j)] assert all(oncurve(pt,B) for g in gens for pt,B in zip(g,Bs)) H=primary_subgroup(gens,Bs) H2,coords,orders=secondary_subgroup(gens,tables) assert H==H2 and len(H)==(4096 if j==0 else 128) points=[];survivors=[];image_list=[] for beta in projective_points(): alpha=mul(power(EPS,j),power(beta,4)) ispt=(int(alpha[1])%P==0) assert ispt==(form_direct(beta,j)==0) if not ispt:continue points.append(beta) im=phi_primary(beta,j) assert im==phi_secondary(beta,j)==phi_homogeneous(beta,j) image_list.append([list(beta),im]) if im in H:survivors.append(beta) assert len(points)==128 and survivors==EXPECTED[j] print(f'PASS C{j}: all 16257 projective residue points checked; 128 lie on the curve.') print(f'PASS E{j}: each finite elliptic group has 128 points; both subgroup methods give {len(H)}.') print(f'PASS C{j}: all three image methods leave exactly {survivors}.') out['curves'][str(j)]={'elliptic_coefficients':Bs,'group_size':len(H),'generators':gens, 'group_coordinate_generators':coords,'generator_orders':orders, 'survivors':survivors,'point_images':image_list, 'cyclic_bases':[[T['S'],T['T']] for T in tables]} print(f'PASS: complete addition tables of {len(TABLE_CACHE)} distinct elliptic curves checked in both representations.') return out if __name__=='__main__': out=run() Path('finite_sieve_certificate.json').write_text(json.dumps(out,indent=2)+'\n') print('ALL FINITE SIEVE CHECKS PASSED.') \end{lstlisting} % END VERIFIER FILE: verify_finite_sieve.py \Needspace{8\baselineskip} \subsection{\texorpdfstring{\texttt{verify\_chabauty.py}}{\detokenize{verify_chabauty.py}}}\label{src:chabauty} % BEGIN VERIFIER FILE: verify_chabauty.py \begin{lstlisting}[style=source] """Exact 127-adic and differential certificates for the four surviving disks. Logarithms are recomputed by BOTH projective doubling and division polynomials. """ import json from functools import lru_cache from pathlib import Path import sympy as sp from arith import * P=127 MOD=P**3 ROOTS=[32,100,122] EXPECTED_LOGS={0:[[15210,15210,15210],[1479,8949,7539]],2:[[12688,14137,3766]]} EXPECTED_ANN={0:[9,63,55],2:[0,83,87]} def root_lifts(): newton=[];by_digits=[] for a in ROOTS: r=a;m=P while m