EGRS75 two-prime — THE DIOPHANTINE SEED (paper condition (2)), 2026-06-12.

NEW file. Imports Equidist_mathlibapi (for the kernel-clean irrationality irrational_log_div_log) + Mathlib's Dirichlet approximation. Modifies nothing.

GOAL (seed_window): for distinct primes p q (q ≥ 3) and every floor F, produce a PURE POWER p^α landing in the base-q window

(q-1)/2 · q^(e+3)  <  p^α  <  (q-1)/2 · q^(e+3) + q^(e+1)/4,

with q^(e+3) > F. Such a seed has base-q digits: digit(e+3) = (q-1)/2 = B (good), digit(e+2) = 0 (STRICTLY good), everything above zero, and the excess below q^(e+1) — exactly the "B-led staircase" start EGRS75 manufacture with their condition (2) (Math. Comp. 29 (1975), p.84). p^α is automatically LowDigits p. The iterated repair (file EgrsSeedClose_2026-06-12.lean) consumes this seed and never sinks below B·q^(e+3).

METHOD (fully elementary given Mathlib):

1. irrational_log_div_log (REUSED, kernel-clean): log p / log q ∉ ℚ.
2. Dirichlet (Real.exists_int_int_abs_mul_sub_le): a NONZERO step δ = a·log p − b·log q with |δ| < window-width, a ≥ 1.
3. walk_hits: an arithmetic walk with positive step smaller than the window width cannot jump over the window — the first crossing lands inside.
4. Transfer the log-inequalities back to ℕ via exp monotonicity + casts.

No native_decide, no axiom, no sorry. Formalizes part of the KNOWN theorem EGRS75 (1975); three primes is Erdős #376 (OPEN) — not attempted. Recon: ~/Knowledge/Construct/recon/erdos_376.md.

Real-log bridge

theorem Egrs75.SeedWindow.lt_of_log_lt {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h : Real.log a < Real.log b) : a < b

exp-bridge: log a < log b → a < b for positive reals.

The walk: a small-step arithmetic progression cannot jump a window

theorem Egrs75.SeedWindow.walk_hits {δ w₁ w₂ start : ℝ} (hδ0 : 0 < δ) (hδw : δ < w₂ - w₁) (hstart : start < w₁) : ∃ (t : ℕ), 1 ≤ t ∧ w₁ < start + ↑t * δ ∧ start + ↑t * δ < w₂

Walk lemma (KERNEL-CLEAN). If 0 < δ < w₂ − w₁ and the walk start + t·δ begins below w₁, then its FIRST crossing of w₁ lands strictly inside (w₁, w₂).

The small nonzero step: Dirichlet + irrationality

theorem Egrs75.SeedWindow.exists_small_step {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p ≠ q) {ε : ℝ} (hε : 0 < ε) : ∃ (a : ℕ) (b : ℕ), 1 ≤ a ∧ ↑a * Real.log ↑p - ↑b * Real.log ↑q ≠ 0 ∧ |↑a * Real.log ↑p - ↑b * Real.log ↑q| < ε ∧ (↑a * Real.log ↑p - ↑b * Real.log ↑q < 0 → 1 ≤ b)

Small-step lemma (KERNEL-CLEAN). For distinct primes p q and any ε > 0 there are naturals a ≥ 1, b with δ := a·log p − b·log q NONZERO, |δ| < ε, and b ≥ 1 whenever δ < 0. Dirichlet supplies the approximation; the kernel-clean irrational_log_div_log rules out δ = 0.

The seed window

theorem Egrs75.SeedWindow.seed_window {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hq3 : 3 ≤ q) (hpq : p ≠ q) (F : ℕ) : ∃ (α : ℕ) (e : ℕ), 1 ≤ α ∧ F < q ^ (e + 3) ∧ (q - 1) / 2 * q ^ (e + 3) < p ^ α ∧ 4 * p ^ α < 4 * ((q - 1) / 2 * q ^ (e + 3)) + q ^ (e + 1)

THE DIOPHANTINE SEED (KERNEL-CLEAN). For distinct primes p q with q ≥ 3 and any floor F, there are α ≥ 1 and e with q^(e+3) > F and

(q-1)/2 · q^(e+3)  <  p^α   and   4·p^α < 4·((q-1)/2 · q^(e+3)) + q^(e+1).

So p^α (automatically LowDigits p) has base-q digit (q-1)/2 at e+3, digit 0 at e+2, zeros above e+3, and excess < q^(e+1) — the EGRS75 condition-(2) staircase seed at arbitrary height.