EGRS75 — the single-base density "Fact" (kernel-clean).

This isolates and proves the load-bearing density lemma from the original EGRS 1975 proof (Math. Comp. 29, the "Fact" inside the proof of their Theorem 1):

Fact. For an odd prime base p (more generally any odd p ≥ 3) and every x ≥ 1, the half-open interval [x, 2·x) contains a number all of whose base-p digits are ≤ (p-1)/2 (i.e. a LowDigits p number).

In EGRS the ratio is (p-1)/A; with A = (p-1)/2 (the central-binomial / Kummer case) it is exactly 2. This is the genuine density content #{n < X : LowDigits p n} ≍ X^{θ_p} made into a gap bound: consecutive LowDigits p numbers never differ by more than a factor 2.

We prove it constructively via the explicit "round up to the next low-digit number" map ru: ru x is the smallest LowDigits p number ≥ x, built by well-founded recursion on the base-p digit recursion x = p·(x/p) + x%p. Correctness (x ≤ ru x < 2x, LowDigits p (ru x)) is proven by strong induction.

KERNEL-CLEAN: #print axioms at the end must show only propext / Classical.choice / Quot.sound (NO sorryAx).

NOTE: this Fact does NOT by itself prove the two-prime crux — it is the single per-base density input. Combining the two per-base Facts into a simultaneous low-digit number in both bases is the EGRS Diophantine "iterative digit repair" step (their eq. (2) + the repair Lemma), which is the genuine remaining gap.

The round-up map ru and its correctness

@[irreducible]

def Egrs75.RoundUp.ru (p x : ℕ) : ℕ

ru p x = the smallest LowDigits p number ≥ x, built by rounding up the base-p digits with carry. Defined by well-founded recursion on x:

• x = 0 → 0;
• x < p or degenerate p < 3 → x if x ≤ (p-1)/2 (single low digit), else p (carry to 10₍ₚ₎);
• x ≥ p (and p ≥ 3), last digit d = x % p:
  • d ≤ (p-1)/2 → keep it: p · ru (x/p) + d;
  • d > (p-1)/2 → drop it and carry: p · ru (x/p + 1).

The p < 3 guard makes the definition total (the recursion only fires for p ≥ 3, where x/p + 1 < x for x ≥ p); correctness is only claimed for odd p ≥ 3 (ru_spec).

Equations

• One or more equations did not get rendered due to their size.

LowDigits of ru (kernel-clean)

ru p x is always LowDigits p. Proven by strong induction using the digit recursion: LowDigits p (p·m + d) holds when d ≤ (p-1)/2 and LowDigits p m.

theorem Egrs75.RoundUp.lowDigits_zero (p : ℕ) : LowDigits p 0

0 has no digits, hence LowDigits p 0 vacuously.

theorem Egrs75.RoundUp.lowDigits_cons {p m d : ℕ} (hp : 2 ≤ p) (hd : d ≤ (p - 1) / 2) (hm : LowDigits p m) : LowDigits p (p * m + d)

A low last digit on top of a low number stays low: LowDigits p (p*m + d) when d ≤ (p-1)/2 and LowDigits p m (and 2 ≤ p).

theorem Egrs75.RoundUp.one_le_half {p : ℕ} (hp : 3 ≤ p) : 1 ≤ (p - 1) / 2

For p ≥ 3, the digit 1 ≤ (p-1)/2.

theorem Egrs75.RoundUp.lowDigits_one {p : ℕ} (hp : 3 ≤ p) : LowDigits p 1

LowDigits p 1 for p ≥ 3 (digits of 1 are [1], and 1 ≤ (p-1)/2).

theorem Egrs75.RoundUp.lowDigits_ru {p : ℕ} (hp : 3 ≤ p) (x : ℕ) : LowDigits p (ru p x)

ru p x has all base-p digits ≤ (p-1)/2. KERNEL-CLEAN.

The bounds x ≤ ru x < 2x (kernel-clean): the density Fact

This is the quantitative core — consecutive LowDigits p numbers differ by a factor < 2. Proven by strong induction following EGRS's "Fact". The tight case is the carry branch (x % p > (p-1)/2), where ru x = p · ru(x/p + 1) and the upper bound p · ru(x/p+1) < 2x uses 2·(x%p) > p (which holds since x%p > (p-1)/2 and p is odd ⟹ x%p ≥ (p+1)/2).

theorem Egrs75.RoundUp.ru_bounds {p : ℕ} (hp : 3 ≤ p) (hodd : Odd p) (x : ℕ) : 1 ≤ x → x ≤ ru p x ∧ ru p x < 2 * x

The EGRS density Fact, as bounds on ru. For odd p ≥ 3 and x ≥ 1: x ≤ ru p x and ru p x < 2*x. Hence the smallest LowDigits p number ≥ x lies in [x, 2x). KERNEL-CLEAN.

theorem Egrs75.RoundUp.exists_lowDigits_between {p : ℕ} (hp : 3 ≤ p) (hodd : Odd p) (x : ℕ) (hx : 1 ≤ x) : ∃ (m : ℕ), x ≤ m ∧ m < 2 * x ∧ LowDigits p m

EGRS density Fact (existence form). For an odd prime base p ≥ 3 (in fact any odd p ≥ 3) and every x ≥ 1, the interval [x, 2x) contains a LowDigits p number. This is the single load-bearing density input from EGRS75's proof of their Theorem 1. KERNEL-CLEAN.