EGRS75 two-prime — the μ-MEASURE CLOSURE (2026-06-12).
NEW file. Imports the kernel-clean P-machinery + EgrsMoveDigits_20260612
(local digit toolkit) + EgrsSeedWindow_20260612 (the Diophantine seed) +
EgrsAll (the clean egrs_two_prime_of_crux). Modifies nothing upstream.
════════════════════════════════════════════════════════════════════════════
THE CLOSURE ARGUMENT (EGRS75, Math. Comp. 29 (1975), pp.84-85, equality case
A = (p-1)/2, B = (q-1)/2), with two fixes over the 2026-06-08 wave:
(1) THE MEASURE. μ(n) = i·q + (B − b_i), where j = topBadIndex q n, i = leastGoodAbove(j) (least strictly-good index above j; digits strictly between are exactly B), b_i = digit of n at i. μ strictly drops on every single ADD move and never rises on a SUBTRACT (which strictly drops n), so lex (μ, n) ∈ ℕ² is a faithful termination measure — the outer strong induction does ALL the iterating and no inner iteration is hidden anywhere.
(2) THE FLOOR. The magnitude invariant is NOT N < n alone (the paper's
SUBTRACT branch lowers n) but N < (n / q^i)·q^i — the digits at/above the
working index alone already exceed N. Both branches preserve it: SUBTRACT
freezes the block at/above i (it only strips the tail S ≤ T = n % q^i);
ADD increments it. The Diophantine seed p^α (condition (2), file
EgrsSeedWindow_20260612) establishes it at start: its base-q digits are
B at e+3, 0 at e+2 (a strictly-good barrier), staircase below, so its
working index is ≤ e+2 and the preserved block is ≥ B·q^(e+3) > N.
THE MOVE (single, no iteration), branch on T = n % q^i vs S = (p^m+1)/2 with m = lowest nonzero base-p digit index: • T < S (ADD): condition (3) gives q^i < p^m; draw a LowDigits-p correction U ∈ [q^i−T, 2(q^i−T)) (density Fact); the single carry sends digit i to b_i+1, freezes everything above, and replaces the tail by R = T+U−q^i with 2R+3 ≤ q^i — STRICTLY below the all-B ceiling. The STAIRCASE lemma then locates a strictly-good barrier k < i with exactly-B digits in (k,i), so the new working index is ≤ k < i: μ STRICTLY DROPS. n grows; the block at i increments — floor preserved. • S ≤ T (SUBTRACT): n' = n − S is LowDigits p (borrow eats the trailing base-p zeros), digits at/above i are FROZEN (S ≤ T), so μ is unchanged (or drops) while n strictly drops — the lex pair falls. Floor frozen.
STATUS: ZERO sorry. Every theorem in this file is kernel-clean
(#print axioms = propext / Classical.choice / Quot.sound; no native_decide,
no extra axiom). This completes the Lean 4 formalization of the KNOWN
Erdős–Graham–Ruzsa–Straus 1975 two-prime theorem (Theorem 1, equality case):
infinitely many n with p ∤ C(2n,n) and q ∤ C(2n,n) for distinct odd primes p,q.
NOT an open-problem solve: the r ≥ 3 generalization is Erdős #376 (OPEN) and is
not attempted. Recon: ~/Knowledge/Construct/recon/erdos_376.md.
The μ-measure (total ℕ-valued) #
The μ-measure. μ(n) = i·q + (B − b_i) with i = leastGoodAbove(topBad n),
B = (q-1)/2, b_i = n / q^i % q. Total: junk 0 when n has no bad base-q
digit. B − b_i < q, so this is the faithful mixed-radix linearisation of the
lex pair (i, B − b_i).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The μ-drop arithmetic core (KERNEL-CLEAN) #
μ strictly drops. μ(n') < μ(n) whenever n' is fully good, or its
working index dropped, or the index held and the digit there strictly climbed.
THE SINGLE MOVE — fully proven (no sorry) #
One EGRS75 condition-(3) carry-controlled move: ADD when T < S, SUBTRACT when
S ≤ T. Output: still LowDigits p, the floor block at the working index is
preserved-or-grown, and the lex pair (μ, n) strictly falls.
THE EGRS75 SINGLE MOVE (KERNEL-CLEAN, no sorry).
The clean lex-(μ, n) strong induction #
ALIGN via the lex pair (μ, n) (KERNEL-CLEAN). Repeatedly applying the
single move from a seed whose floor block exceeds N yields a number that is
> N, LowDigits p, and LowDigits q. Outer strong induction on μ, inner
on n; the floor invariant N < (n/q^i)·q^i is threaded (it implies N < n).
The seeded finish: Diophantine seed + μ-induction + single move #
ALIGN, fully proven (KERNEL-CLEAN, no sorry). For distinct odd primes
p q, every N admits n > N that is LowDigits p and LowDigits q. Seeded
by the Diophantine window seed_window (EGRS condition (2)); driven by
align_mu consuming the fully-proven egrs_move.
Final assembly: the EGRS75 two-prime theorem, ZERO sorry #
EGRS75 two-prime theorem — CLOSED (KERNEL-CLEAN, no sorry). For
distinct odd primes p q, there are infinitely many n with p ∤ C(2n,n) and
q ∤ C(2n,n). (Erdős–Graham–Ruzsa–Straus, Math. Comp. 29 (1975), Theorem 1,
equality case — a KNOWN theorem; this is its machine-checked proof.)
The 2026-06-08 residual, discharged. Statement byte-identical to
Finish.egrs_clearing_low (EgrsFinish_core.lean:301): from the μ-closure, a
fully (q,B)-good number above any floor exists, which clears every index.