claimroutineinferred_dep

Oracle reduces integer to rational solvability

Gives Turing reduction of H10(Z) to H10(Q) by relativizing the search

lower-bound step toward degree

0'

Claim·§7 Turing degree and a quartic normal form·inside corDegree 0' for rational solvability and quartic forms

Statement (paper)

The parallel search in the proof of Theorem , run with an

\mathrm{H10}(\Q)

oracle in place of the hypothetical rational decision procedure, halts on every input and gives a single oracle machine. Hence

\mathrm{H10}(\Z)\le_{\mathrm T}\mathrm{H10}(\Q)

, where

\mathrm{H10}(\Z)

is the set of integral polynomials having an integer zero.

In plain English

Running the parallel search from the proof of the main theorem with an

\mathrm{H10}(\Q)

oracle in place of the rational decision procedure always halts and defines one oracle machine. Hence

\mathrm{H10}(\Z)\le_{\mathrm T}\mathrm{H10}(\Q)

Why it's here

The main theorem's argument is a reduction of integer to rational solvability, and nothing in it needs the rational procedure to be an actual algorithm. Substituting the oracle makes the reduction relativized, which yields the Turing reduction. This is the step toward the lower bound

0'

for

\mathrm{H10}(\Q)

in the degree statement, and it relies on the finite-test criterion, which guarantees that the search halts.

Classified routine:

Direct relativization of the main theorem's parallel-search reduction: the oracle replaces the hypothetical decision procedure, and halting follows from the earlier finite-test criterion (red-finite-test-success).

Uses

thmHilbert's tenth problem over Q is undecidablepropFinite test success gives integer zero

Used by

claimH10(Q) has Turing degree 0'

Sources

PaperOpen

Section: §7 Turing degree and a quartic normal form
Page: —
Label: —
Line: sections/07-consequences.tex:26

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Oracle reduction of integer to rational solvability" rests on red:finite-test-success