lemmaroutineinferred_dep

Compactness yields a model with rational embedding

Passing finite tests gives a model RR of T\mathcal T with a zero of ff
nonstandard solution analyzed by the height argument
Lemma·red:compactness·§2.4 Finite rational tests and compactness

Statement (paper)

If every finite rational test succeeds, there exist an ambient elementary extension of the many-sorted structure specified in \S, a model RR of T\mathcal T, a tuple a∈Rn\mathbf a\in R^n with f(a)=0f(\mathbf a)=0, and an embedding R↪∗QR\hookrightarrow{}^*\Q into its rational sort such that every element of the image satisfies Φ\Phi.

In plain English

If every finite rational test succeeds, then there is an ambient elementary extension ∗Q{}^*\Q-containing structure, a model RR of T\mathcal T, and a tuple a∈Rn\mathbf a\in R^n with f(a)=0f(\mathbf a)=0, together with an embedding of RR into the rational sort whose image consists entirely of elements satisfying Φ\Phi.

Why it's here

This is the compactness step that turns the family of finite solvable rational tests into a single nonstandard object: a model of T\mathcal T with a zero of ff sitting inside ∗Q{}^*\Q. The condition Φ\Phi is the pole-parity formula, so every element of the image has only even-order poles outside the finite set S1S_1. Later arguments use this to control valuations and to show that ff has an integer zero.
Classified routine:
A standard application of the compactness theorem of first-order logic (Gödel–Malcev) to the finite rational tests, packaging finite satisfiability into a nonstandard model inside an elementary extension ∗Q{}^*\Q.

Uses

propPositive existential formula forcing even poles

Used by

propFinite test success gives integer zeroclaimPolynomial error delta is zero or bounded

Sources

PaperOpen
Section
§2.4 Finite rational tests and compactness
Page
—
Label
red:compactness
Line
sections/02-reduction.tex:545
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The lemma asserts every image element "satisfies Φ" (02-reduction.tex:551-552), and the proof adds "Φ for each term value" (line 564). Φ is the formula of Proposition par:pole-parity, which constraint (d) cites at line 523.