lemmaroutineinferred_dep

Integers form a model of the theory

Theory T\mathcal T is recursive and Z\mathbb Z with Ta=aPT_a=aP models it
supplies the integer model for the reduction
Lemma·red:standard-model·§2.3 A recursive theory with an ordinary integer model

Statement (paper)

The theory T\mathcal T is recursive and has a model whose ring is Z\Z. In this model Ta=aPT_a=aP for every integer aa.

In plain English

The theory T\mathcal T is recursive, and it has a model whose underlying ring is Z\Z, in which Ta=aPT_a=aP for every integer aa.

Why it's here

This shows that the standard integers, with each integer aa encoded as the point aPaP built from the fixed rank-one generator PP, satisfy T\mathcal T. The proof checks the local comparison hypotheses for every integer aa using integer coverage by prime patterns. Since T\mathcal T is recursive and has an ordinary integer model, it can be used in the reduction behind the main undecidability theorem.
Classified routine:
Checks that the standard integers satisfy the paper's own axioms by verifying the local comparison hypotheses via the earlier integer-coverage corollary and the fixed rank-one generator P; recursiveness is bookkeeping on the explicit axiom list.

Uses

corInteger coverage by prime patternspropElliptic curve over F has rank one

Used by

thmHilbert's tenth problem over Q is undecidable

Sources

PaperOpen
Section
§2.3 A recursive theory with an ordinary integer model
Page
—
Label
red:standard-model
Line
sections/02-reduction.tex:435
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof relies on "the nontorsion point P", which Proposition 2.1 provides, to show nonzero multiples avoid O and the two-torsion points.