EGRS75 two-prime crux — route mathlib-api: the equidistribution INPUT.
TARGET (exists_pow_lowDigits_base_q_mathlibapi, statement-identical to
Cdensity.key): for distinct odd primes p q and every N,
∃ n, N < n ∧ LowDigits p n ∧ LowDigits q n.
This file is the mathlib-api route: it REUSES Mathlib's AddCircle dense-orbit
API (AddCircle.denseRange_zsmul_coe_iff) to supply the alignment INPUT that the
EGRS digit-repair construction consumes. Concretely it proves, KERNEL-CLEAN:
(A) irrational_log_div_log : Irrational (Real.log p / Real.log q) for distinct
primes p q — the irrationality sub-lemma the inventory flagged as the missing
Mathlib fact. Proof: a rational value a/b forces p^n = q^m (n,m ≥ 1) via
Real.log_pow + Real.log_injOn_pos, contradicting Prime.dvd_of_dvd_pow.
(B) denseRange_log_zsmul : the multiples of log p are dense in the circle
AddCircle (Real.log q) — i.e. the orbit {a · log p mod log q} is dense.
This is AddCircle.denseRange_zsmul_coe_iff instantiated at (A). It is the
exact equidistribution statement Mathlib packages, and the alignment input
EGRS use: it lets the base-q TOP block of p^a be steered into any target
window for arbitrarily large a.
What (A)+(B) DO give (and is real, kernel-clean): the seed p^a is automatically
LowDigits p (Cdensity.lowDigits_pow), and its base-q top block can be aligned
by density. What they DO NOT give, and what Mathlib does not package, is the
ITERATIVE DIGIT-REPAIR that turns "top block aligned" into "ALL base-q digits
small": EGRS75 (Math. Comp. 29, Thm 2 / cond. (3)) repair each oversized base-q
digit block by adding a controlled LowDigits p number (found via
exists_lowDigits_between) WITHOUT creating a large base-p digit, and prove the
repair TERMINATES using condition (3) (A/(p-1)+B/(q-1) ≥ 1, here = 1). This
termination + "remove a large base-q digit without making a large base-p digit"
lemma is elementary but multi-page number theory; the Bloom–Croot survey
(arXiv:2509.02835, §1) states explicitly it "is proved using elementary number
theory in [4] and makes essential use of the condition (3)". Mathlib has neither
the repair lemma nor the quantitative window-within-N bridge from density.
HONEST STATUS: (A) and (B) are FULLY PROVEN and kernel-clean (#print axioms =
propext / Classical.choice / Quot.sound). The target itself carries exactly ONE
labelled sorry, sitting on the genuine remaining step — the EGRS cross-base
digit-repair termination — which is the documented missing input, not laziness.
No fakes: no native_decide, no bogus axiom, no circular hypothesis.
DO NOT frame this as solving an open Erdős problem: this formalises EGRS75 (Math. Comp. 1975, Theorem 1/2), a KNOWN theorem. Three primes is Erdős #376 (open).
(A) The irrationality sub-lemma (KERNEL-CLEAN) #
Irrational (log p / log q) for distinct primes p q. Mathlib has no log
irrationality lemma, so we prove it: a rational value a/b cross-multiplies to
n · log p = m · log q with n,m ≥ 1 (after normalising signs — both sides are
positive), which via log_pow + injectivity of log on (0,∞) forces the
NATURAL-number identity p^n = q^m; then p ∣ q^m ⟹ p ∣ q ⟹ p = q, contradiction.
Core arithmetic obstruction. For distinct primes p q there are no
positive naturals n m with (p:ℝ)^n = (q:ℝ)^m. (Equivalently p^n = q^m in ℕ
is impossible.) This is the unique-factorisation fact behind log p / log q ∉ ℚ.
(A) — irrationality of log p / log q for distinct primes p q.
KERNEL-CLEAN. This is the Mathlib-missing fact; everything in the dense-orbit
route hangs off it.
(B) The dense orbit (KERNEL-CLEAN) #
AddCircle.denseRange_zsmul_coe_iff says the multiples of a are dense in
AddCircle p iff a/p is irrational. Instantiate a = log p, p = log q and feed
(A). This is the equidistribution INPUT EGRS use — the orbit {k · log p mod log q}
visits every window.
(B) — the dense orbit {k · log p mod log q} for distinct primes p q.
KERNEL-CLEAN. AddCircle.denseRange_zsmul_coe_iff ∘ (A). The base-q top block of
p^k can be steered into any window for arbitrarily large k.