corollaryroutineinferred_dep

Simultaneous integer tests at both places

Gives h,j0h,j_0 independent of aa so every integer passes both local tests
one choice of tests works for all integers
Corollary·pri:integer-tests·§6 Prime patterns for the two conjugate local tests

Statement (paper)

Fix an integer K≥1K\ge1 and a prime rr supplied by Lemma , large enough for Proposition  at precision KK. At each of the two places vv above rr there are nonzero integers h,j0h,j_0, chosen independently of a∈Za\in\Z, such that, for every a∈Za\in\Z: \begin{enumerate} \item hPhP and haPhaP reduce to OO at vv, ℓK(z(hP))≠0\ell_K(z(hP))\ne0, and v ⁣(ℓK(z(haP))ℓK(z(hP))−a)≥K; v\!\left(\frac{\ell_K(z(haP))}{\ell_K(z(hP))}-a\right) \ge K; \item j0Pσj_0P^\sigma and (h−4)aPσ(h-4)aP^\sigma reduce to OO at the same place vv, and v ⁣(z((h−4)aPσ)z(j0Pσ))≥K. v\!\left(\frac{z((h-4)aP^\sigma)}{z(j_0P^\sigma)}\right) \ge K. \end{enumerate} The choices of h,j0h,j_0 may differ at the two places.

In plain English

For a prime rr from the prime-pattern lemma that is large enough for the formal-group comparison at precision KK, each of the two places vv above rr has nonzero integers h,j0h,j_0, independent of a∈Za\in\Z. For every integer aa, ℓK(z(haP))/ℓK(z(hP))\ell_K(z(haP))/\ell_K(z(hP)) equals aa to vv-precision KK, and z((h−4)aPσ)/z(j0Pσ)z((h-4)aP^\sigma)/z(j_0P^\sigma) has vv-valuation at least KK.

Why it's here

This turns the prime pattern and the formal-group comparison into two conjugate local tests on an arbitrary integer aa. The first test reads aa off the multiples of PP to vv-precision KK. The second shows that the conjugate point (h−4)aPσ(h-4)aP^\sigma is vv-adically small relative to j0Pσj_0P^\sigma. The multipliers hh and j0j_0 do not depend on aa, so one pair of choices works for every integer aa at each place. The integer-coverage corollary builds on this.}
Classified routine:
A direct consequence of the prime-pattern lemma (pri:pattern) combined with the formal-group comparison (ell:formal). It takes hh and j0j_0 as multiples of the local reduction orders and then applies the standard formal-logarithm estimate for elliptic formal groups.

Uses

propFormal group comparison of elliptic multipleslemPrime patterns with controlled reduction orders

Used by

corInteger coverage by prime patterns

Sources

PaperOpen
Section
§6 Prime patterns for the two conjugate local tests
Page
—
Label
pri:integer-tests
Line
sections/06-primes.tex:53
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The statement fixes "a prime r supplied by Lemma " (06-primes.tex:54). The proof (lines 76-78) uses its order conditions gcd(d_1,d_2)|4 and r∤d_1, yet the DAG has no edge.