EGRS75 two-prime infinitude — strategy + defs scaffold.

Erdős–Graham–Ruzsa–Straus 1975, "On the prime factors of binomial coefficients" (Math. Comput. 29 (1975) 83–92).

TARGET (egrs_two_prime): for distinct odd primes p q, {n : ℕ | ¬ p ∣ Nat.centralBinom n ∧ ¬ q ∣ Nat.centralBinom n}.Infinite.

This file performs the BRIDGE REDUCTION only. It assembles the single-base Kummer→digit characterisation we already hold KERNEL-CLEAN in ConstructProofs/Erdos376Bridge.lean (coprime_centralBinom_prime_iff) ConstructProofs/ConcreteMath/KummerBridge.lean into the predicate LowDigits p n ("every base-p digit of n is ≤ (p-1)/2"), proves ¬ p ∣ Nat.centralBinom n ↔ LowDigits p n (kernel-clean), and reduces the target to the CRUX egrs_crux: {n : ℕ | LowDigits p n ∧ LowDigits q n}.Infinite.

The crux is the genuine theorem (counting-exponent density argument: θ_p + θ_q > 1 for all distinct odd p,q) and is left as the single labelled sorry. Three primes is Erdős #376 (OPEN) — do NOT attempt here.

Recon / context: MATH CONTEXT block in the run prompt; #376 recon at ~/Knowledge/Construct/recon/erdos_376.md DO NOT reprove Kummer — reuse the imports below.

The digit predicate

def Egrs75.LowDigits (p n : ℕ) : Prop

LowDigits p n: every base-p digit of n is ≤ (p-1)/2. This is the Kummer no-carry condition for doubling n in base p (p ∤ C(2n,n)). For an odd prime p, d ≤ (p-1)/2 ↔ 2*d < p, so it is the same predicate as #376's LowDoubleDigits p n := ∀ d ∈ digits p n, 2*d < p (see lowDigits_iff_lowDoubleDigits below).

Equations

• Egrs75.LowDigits p n = ∀ d ∈ p.digits n, d ≤ (p - 1) / 2

theorem Egrs75.digit_le_half_iff_two_mul_lt {p d : ℕ} (hp2 : 2 ≤ p) (hpodd : Odd p) : d ≤ (p - 1) / 2 ↔ 2 * d < p

For an odd prime p, the per-digit bound 2*d < p (the #376 form, i.e. "doubling produces no carry") is equivalent to d ≤ (p-1)/2 (the LowDigits form). The hypotheses are stated per-digit so the lemma threads through the ∀ d ∈ digits p n quantifier.

theorem Egrs75.lowDigits_iff_lowDoubleDigits {p n : ℕ} (hp2 : 2 ≤ p) (hpodd : Odd p) : LowDigits p n ↔ Erdos376.LowDoubleDigits p n

LowDigits and #376's LowDoubleDigits coincide for odd primes.

The single-base bridge (KERNEL-CLEAN — assembled from #376)

coprime_centralBinom_prime_iff (Erdos376Bridge) gives, for any prime p: Coprime (centralBinom n) p ↔ LowDoubleDigits p n. We turn Coprime _ p into ¬ p ∣ _ and LowDoubleDigits into LowDigits (odd prime), yielding the single-base fact we already hold.

theorem Egrs75.not_dvd_centralBinom_iff_lowDigits {p : ℕ} (hp : Nat.Prime p) (hpodd : Odd p) (n : ℕ) : ¬p ∣ n.centralBinom ↔ LowDigits p n

EGRS single-base bridge. For an odd prime p, p ∤ C(2n,n) exactly when every base-p digit of n is ≤ (p-1)/2. Kernel-clean: assembled from coprime_centralBinom_prime_iff + odd-prime digit arithmetic. This is the per-prime Kummer fact the two-prime target stands on.