corollaryroutine

Integer coverage by prime patterns

Chooses prime patterns so every integer aa passes both local tests
verifies local-comparison hypotheses for all integers
Corollary·pri:integer-coverage·§2.2 Contact primes and ordinary integer witnesses

Statement (paper)

Let K⊂Z>0\mathcal K\subset\Z_{>0} be the finite multiplier set supplied by Lemma  in Section . It has the following property. For every integer K≥1K\ge1, every A∈ZA\in\Z, and every real lower bound Y0>0Y_0>0, there exist integers u1,u2,vu_1,u_2,v, with v≠0v\ne0, such that, on setting u3=Av−u1−u2u_3=Av-u_1-u_2, the following hold. \begin{enumerate}[label=(\arabic*),leftmargin=*] \item \textup{Representation and primes.} Each of the thirteen numbers v,Lb(ui,v)(1≤i≤3, b∈C∖{∞}) v,\qquad L_b(u_i,v) \quad(1\le i\le3,\ b\in\mathcal C\setminus\{\infty\}) equals εkr\varepsilon k r, where ε∈{1,−1}\varepsilon\in\{1,-1\}, k∈Kk\in\mathcal K, and r>Y0r>Y_0 is a positive rational prime. Every such rr splits in FF, is a prime of good reduction for both EE and EσE^\sigma, lies outside SES_E, and satisfies r>K+1r>K+1. \item \textup{Witnesses at each place.} For each occurrence of a prime rr in this list and each of the two places vrv_r of FF above it, there are nonzero integers h,j0h,j_0, chosen independently of a∈Za\in\Z, such that every a∈Za\in\Z satisfies conditions (i) and (ii) of Lemma  in the ordinary setting: take R=ZR=\Z, its identity embedding in the ordinary structure, Ta=aPT_a=aP, q=rq=r, and v∗=vrv_*=v_r, normalized by vr(r)=1v_r(r)=1. In this specialization the tildes disappear. The choices of h,j0h,j_0 may differ at different occurrences and at the two places. \end{enumerate} The set K\mathcal K is independent of K,A,Y0K,A,Y_0.

In plain English

There is a finite multiplier set K\mathcal K, independent of K,A,Y0K,A,Y_0, such that for any K≥1K\ge1, A∈ZA\in\Z and Y0>0Y_0>0 one can choose u1,u2,vu_1,u_2,v (with v≠0v\ne0, u3=Av−u1−u2u_3=Av-u_1-u_2) making all thirteen numbers vv and Lb(ui,v)L_b(u_i,v) equal to ±kr\pm k r with k∈Kk\in\mathcal K and r>Y0r>Y_0 a good split prime with r>K+1r>K+1. At each such prime and each place above it, there are nonzero integers h,j0h,j_0, independent of aa, so that every integer aa satisfies the two local-comparison conditions with Ta=aPT_a=aP.

Why it's here

This combines the prime-pattern lemma, which supplies the thirteen test numbers as bounded multiples of large good primes, with the simultaneous integer tests, which give the aa-independent h,j0h,j_0 at each place. It checks the hypotheses of the local comparison lemma for every integer aa at all these places, which is what the standard-model lemma uses to show that Z\Z with Ta=aPT_a=aP is a model.
Classified routine:
A direct combination of the prime-pattern lemma (which supplies the thirteen numbers as bounded multiples of large good primes) with the simultaneous integer-tests corollary (which gives a-independent h, j_0 at each place). It amounts to checking the hypotheses of the local comparison lemma.

Uses

lemPrime patterns with controlled reduction orderscorSimultaneous integer tests at both placeslemLocal comparison of elliptic index with integer

Used by

lemIntegers form a model of the theory

Sources

PaperOpen
Section
§2.2 Contact primes and ordinary integer witnesses
Page
—
Label
pri:integer-coverage
Line
sections/02-reduction.tex:294
Leannot aligned

Phase 2 aligns this node to a Lean declaration.