Hilbert’s tenth problem over the rational numbers

1. Separate a first-order theory into finite existential queries

For fixed $F=\mathbb Q(\sqrt2)$, $d=75-53\sqrt2$, and $E:y^2=x^3-d^2x$, Proposition 2.1 supplies $m>0$ and a nontorsion point $P$ with $mE(F)=\mathbb ZP$. The theory $T$ requires a characteristic-zero integral domain $R$ with $\sqrt2\notin\operatorname{Frac}(R)$, assigning to each $a\in R$ a point $T_a\in mE(\operatorname{Frac}(R)(\sqrt2))$. It imposes $T_0=O,T_1=P,T_{a+a'}=T_a+T_{a'}$, and finite, nonzero coordinate conditions for nonzero $a$. Six $R$-valued functions record coordinate numerators and denominators.

For each ordinary integer $K\ge1$ and each $A\in R$, the theory also requires a three-slope representation $A=(u_1+u_2+u_3)/v$ and paired local comparisons at factors of the contact forms. The theory itself contains universal quantifiers; it does not define $R$ inside the rationals by one existential formula. The fixed finite data are independent of the input $f$ and can be hardcoded. Lemma 2.7 supplies an integer model with $T_a=aP$.

Proposition 2.1; §2.3; Lemma 2.7 · pp. 7, 11–12

Adjoin $f(a)=0$, Skolemize, and enumerate ground terms. Assign rational variables to their values, and impose finite collections of constraints for ring operations, functionality on equal inputs, ground instances of universal axioms, and the positive existential condition $\Phi$ on every term value. Each finite collection is an existential Boolean combination of polynomial equations and inequations. Replacing $g\ne0$ by $gy=1$ and conjunctions by sums of squares reduces it to finitely many rational-solvability queries for integral polynomials. Auxiliary witnesses for $\Phi$ and inverse variables used in this translation are not added as new ground terms of the term-generated ring.

§2.4 · pp. 12–13

2. Obtain a model from all successful tests and complete the failure search

An integer zero gives an integer model whose term values all satisfy $\Phi$, so every test succeeds. Conversely, if all tests succeed, compactness gives $R\hookrightarrow{}^*\mathbb Q$ and $f(a)=0$ inside one elementary extension of the ordinary structure carrying arithmetic, valuations, heights, and finite products. The elementary diagram is used only in this existence argument; the algorithm neither enumerates nor queries all true arithmetic sentences.

Proposition 2.12 extracts an ordinary integer zero from this model. Hence, when no integer zero exists, a finite test fails. Alternating the integer-zero enumeration with the failure search turns a hypothetical rational decision procedure into an integer decision procedure, contradicting DPRM. Constant polynomials are handled directly.

Lemma 2.9 · pp. 13–14

Proof of Theorem 1.1 · p. 17

[Dav73, Theorem 8.1, print p. 264 / PDF p. 33]

1. Connect odd contact to a tested localization

Theorem 2.4 supplies five fixed points $C\subset\mathbb P^1(\mathbb Q)$ including infinity, a finite exceptional prime set $S$, and $H,c>0$. Choose primitive integral linear forms $L_b$ vanishing at these points. For $s=(u:v)\notin C$ set

Here $h$ is logarithmic Weil height and the product has no repetitions. Enlarging the exceptional set changes only the constant, not $c$. Fix one ordinary $K\ge cD$ and choose representations for every $A\in R$ at this precision. Contact-form values have the shape $\varepsilon kr$, with $k$ in a fixed finite set; a contact prime $q$ makes the valuation of some $\widetilde r$ odd.

Theorem 2.4; Corollary 2.5 · pp. 9–10

The condition $\Phi$ holds on all integers and makes negative valuations outside $S_1$ even; it does not define integrality. Since every ring value satisfies $\Phi$, every ring valuation lying in the convex subgroup $J\subset{}^*\mathbb Z$ generated by negative ring valuations is even. Thus the odd value $v_q(\widetilde r)$ lies outside $J$ and is positive in the quotient valuation. Its center is one of the two branches of $R_F/rR_F\simeq(R/rR)^2$. Lemma 2.10 converts divisibility by $r^l$ in that tested localization into the actual extended-valuation bound $v^*\ge l$. The ring is not assumed to be $q$-integral at the start.

Lemma 2.10; Proposition 2.11 · pp. 14–15

2. Use the conjugate comparison to establish integrality of the index ratio first

At the selected branch, the same nonzero $h,j_0\in R$ work for every $a\in R$. The formal-parameter comparison on the conjugate curve gives

As $q\ne2$, the denominator $\eta(h)$ is a unit: $\eta(ha)/\eta(h)$ is integral and congruent to $\eta(a)$. Only after obtaining this integrality can one apply Proposition 2.2 to the truncated formal logarithm $\ell_K$ on the primary curve. Combining its estimate with the tested condition yields

and integrality of $\widetilde a$. One never substitutes $\eta(ha)=\eta(h)\eta(a)$ by assuming multiplicativity. Transfer concerns evaluations of the fixed-degree polynomial $\ell_K$, not an infinite series in the elementary extension.

Proposition 2.2; Lemma 2.3 · pp. 8–9

3. Fix the root error and bound heights uniformly

Apply these congruences to the root coordinates at every contact prime of each slope $s_i=(\widetilde u_i:\widetilde v)$. They give $v_q(\delta)\ge K$, and transfer of finite-product divisibility gives $M_K(s_i)^K\mid\delta$. Since $|\delta|\le C_fB^D$,

The constant is independent of $A$ and uniform in the root tuple. Apply the bound to the three ring values in $x(T_{a_j})=(x_0(a_j)+\sqrt2x_1(a_j))/x_2(a_j)$. For nonzero $a_j$ this gives $h(x(\eta(a_j)P))\ll_fB$. On the other hand, the canonical-height comparison at the fixed nontorsion point gives $h(x(nP))=2\widehat h(P)n^2+O(1)$ with $\widehat h(P)>0$. If $B>1$, choose a maximizing index to obtain $B^2\ll_fB+1$; the case $B=1$ is immediate. All indices therefore lie in an ordinary finite interval, so $\eta(a_j)=n_j\in\mathbb Z$. Additivity, $\eta(1)=1$, and injectivity force $a_j=n_j$, producing the ordinary integer zero.

Proposition 2.12; (2.21)–(2.28) · pp. 16–17

1. Bound the degree of rational solvability in both directions

DPRM makes the halting set Diophantine over the positive integers. Replace positive-integer witnesses by $1+u_1^2+u_2^2+u_3^2+u_4^2$ to obtain $\mathbf0'\le_T H10(\mathbb Z)$. The previous argument gives $H10(\mathbb Z)\le_T H10(\mathbb Q)$. Rational-tuple enumeration makes $H10(\mathbb Q)$ computably enumerable, giving the opposite upper bound. The arithmetic constants are hardcoded in one oracle machine, not chosen separately for each $f$.

[Dav73, Theorem 8.1, print p. 264 / PDF p. 33]

Proof of Corollary 7.1 · pp. 56–57

2. Record each operation by a quadratic equation

For every node in an arithmetic circuit for $f$, introduce a variable $Y_v$. Input, constant, sum, and product nodes give equations $Y_v-X_j=0$, $Y_v-c=0$, $Y_v-Y_u-Y_w=0$, and $Y_v-Y_uY_w=0$, respectively. Impose $Y_{\mathrm{out}}=0$ at the output. The resulting nonempty quadratic list $(q_i)$ uniquely extends every rational input tuple through the circuit equations. Nonnegativity of rational squares gives

Consequently $H10(\mathbb Q)\le_m S_2\le_m H_{\le4}$. Both restricted problems are also computably enumerable and hence have degree $\mathbf0'$. The arrow from the integer problem to the rational problem remains a Turing reduction: neither many-one completeness of $H10(\mathbb Q)$ nor a single existential definition of $\mathbb Z\subset\mathbb Q$ follows. In $S_2$, the list presenting the sum of squares is part of the input, so recognizing such a presentation is unnecessary.

§7, arithmetic-circuit conversion · p. 57