claimroutineinferred_dep

Few primes with large common order factor

Bounds primes sharing an order factor l>Ll>L by ≪X/(Llog⁡X)\ll X/(L\log X) + small
shows bad common-factor primes are rare
Claim·§6.5 Counting bad prime values·inside lemPrime patterns with controlled reduction orders

Statement (paper)

Fix one index ν\nu, and let BA,L(X)B_{A,L}(X) be the number of primes in the interval satisfying for which the two orders have a common odd factor l>Ll>L. Then BA,L(X)≪AXLlog⁡X+X7/8+Xlog⁡XB_{A,L}(X)\ll_A \frac{X}{L\log X}+X^{7/8}+\sqrt X\log X, with implied constants independent of LL.

In plain English

For a fixed index ν\nu, the number BA,L(X)B_{A,L}(X) of primes in the given interval satisfying the residue conditions whose two reduction orders share an odd factor l>Ll>L is ≪AX/(Llog⁡X)+X7/8+Xlog⁡X\ll_A X/(L\log X)+X^{7/8}+\sqrt X\log X, with constants independent of LL.

Why it's here

This bounds the primes that must be discarded because their two reduction orders have a large common odd factor, which the order-structure claim confines to primes l≡1(mod4)l\equiv1\pmod4 with l∣r+1l\mid r+1 and l∣al\mid a. The count uses the upper sieve with the lower bound on G(Z)G(Z) to save a factor of log⁡X\log X, and summing over l>Ll>L gives the 1/L1/L saving. Taking LL large then ensures some prime pattern survives, which is used by the next claim on surviving patterns satisfying the order conditions.
Classified routine:
A standard sieve count: it applies the paper's elementary upper sieve (pri-upper-sieve) and the lower bound on G(Z) to the extra congruence conditions l | r+1 and l | a, then sums over l > L. This is the usual bookkeeping for bounding exceptional primes and needs no new idea.

Uses

lemElementary upper sieve with uniform errorsclaimSieve product lower bound G(Z)claimReduction orders r+1±2a and common factors

Used by

claimSurviving prime pattern satisfies order conditions

Sources

PaperOpen
Section
§6.5 Counting bad prime values
Page
—
Label
—
Line
sections/06-primes.tex:550
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Bound on bad prime values with large common factor" rests on pri:upper-sieve
  • info
    inferred_dep
    outline: "Bound on bad prime values with large common factor" rests on claim-pri-pattern-4
  • info
    inferred_dep
    outline: "Bound on bad prime values with large common factor" rests on claim-pri-pattern-1