EGRS75 LOW-case clearing — PRIMITIVE P4: condition-(3) window producer (2026-06-08).

This file builds the EGRS75 "condition (3)" producer for the ADD branch of the LOW-case repair (Finish.egrs_clearing_low, EgrsFinish_core.lean:301). NEW file; does NOT modify any existing clean file and reuses the proven base-q digit machinery.

THE MATH (EGRS75, Math. Comp. 29 (1975), pp.84-85, the Lemma; equality case A = (p-1)/2, B = (q-1)/2). Write n in base q; let j = topBadIndex q n be the largest index whose base-q digit exceeds B (the top oversized digit), and let i be the LEAST index > j whose base-q digit is < B (strictly good). By maximality of j and minimality of i, every digit at an index k with j < k < i equals exactly B. Let T = n % q^i (the paper's "tail" of N = digits below i) and S = ((p-A-1)/(p-1))(p^m - 1) + 1, which in the equality case is S = (p^m + 1)/2, m = lowest nonzero base-p` digit index.

The paper's ADD branch fires when T < S. The tail then satisfies the lower bound T ≥ B·(q^i - 1)/(q - 1) + 1. Combining B·(q^i-1)/(q-1) + 1 ≤ T < S = (p^m+1)/2 and B = (q-1)/2 (so B·(q^i-1)/(q-1) = (q^i-1)/2) yields condition (3) in equality form:

  q^i < p^m.

This is the carry-interlock the ADD branch (P2) consumes: it guarantees the EGRS density Fact (RoundUp.exists_lowDigits_between) draws U ∈ [q^i - T, p^m) LowDigits p, < p^m, so adding it clears the top oversized base-q digit WITHOUT creating a large base-p digit (base-p SAFETY half RepairDV.lowDigits_disjoint_add, kernel-clean).

The paper clause is literally "from T < S AND T ≥ B(q^i-1)/(q-1)+1 derive (3)". This file delivers, KERNEL-CLEAN: • the place-value GOLDEN identity q^i = (q-1)·G i + 1, G i = ∑_{k<i} q^k, • the EXISTENCE+minimality of the least strictly-good index i > j (Nat.find), • the middle-digits-are-B structural fact (digit_good_above_top + minimality), • the ALGEBRAIC INTERLOCK cond3_of_tail_small turning B·G i + 1 ≤ T < S into q^i < p^m, and • cond3_window, the assembled producer: from T < S it extracts i, proves it is a valid clearing index (strictly good, > j) and q^i < p^m, consuming the tail lower bound tail_ge as the one structural input (see its docstring).

HONESTY: real verified Lean. No native_decide, no bogus axiom, no circularity. Reuses (does not reprove) the imported base-q digit machinery. Formalizes the KNOWN theorem EGRS75 (1975). Three primes is Erdős #376 (OPEN) — not attempted.

The base-q geometric sum and the GOLDEN place-value identity

def Egrs75.P4.geomQ (q i : ℕ) : ℕ

The base-q geometric sum G q i = 1 + q + … + q^(i-1).

Equations

• Egrs75.P4.geomQ q i = ∑ k ∈ Finset.range i, q ^ k

theorem Egrs75.P4.geomQ_golden {q : ℕ} (hq : 1 ≤ q) (i : ℕ) : (q - 1) * geomQ q i + 1 = q ^ i

GOLDEN identity (KERNEL-CLEAN). (q-1)·G q i + 1 = q^i for q ≥ 1. Division- and subtraction-free form of G q i = (q^i - 1)/(q - 1), from geom_sum_mul_add at x = q-1 ((q-1)+1 = q).

theorem Egrs75.P4.geomQ_mul {q : ℕ} (hq : 1 ≤ q) (i : ℕ) : (q - 1) * geomQ q i = q ^ i - 1

(q-1)·G q i = q^i - 1 (KERNEL-CLEAN corollary).

theorem Egrs75.P4.geomQ_succ (q i : ℕ) : geomQ q (i + 1) = geomQ q i + q ^ i

G q (i+1) = G q i + q^i (KERNEL-CLEAN).

theorem Egrs75.P4.one_le_geomQ {q i : ℕ} (hi : 1 ≤ i) : 1 ≤ geomQ q i

1 ≤ G q i for i ≥ 1 (the k=0 term is 1; KERNEL-CLEAN).

The ALGEBRAIC INTERLOCK (KERNEL-CLEAN): B·G i + 1 ≤ T < S ⟹ q^i < p^m

This is the load-bearing condition-(3) derivation. With B = (q-1)/2, q odd, the tail lower bound B·G i + 1 ≤ T and the ADD condition T < S = (p^m+1)/2 combine via the golden identity (q-1)·G i = q^i - 1 to force q^i < p^m. Pure ℕ arithmetic.

theorem Egrs75.P4.cond3_of_tail_small {p q : ℕ} (hq : 3 ≤ q) (hpo : Odd p) (hqo : Odd q) (m i T : ℕ) (hlo : (q - 1) / 2 * geomQ q i + 1 ≤ T) (hTS : T < (p ^ m + 1) / 2) : q ^ i < p ^ m

CONDITION (3), algebraic form (KERNEL-CLEAN). For odd p, q ≥ 3, given the EGRS tail squeeze in the equality case A = (p-1)/2, B = (q-1)/2:

• hlo : (q-1)/2 * geomQ q i + 1 ≤ T (paper: T ≥ B(q^i-1)/(q-1) + 1), and
• hTS : T < (p^m + 1)/2 (paper: T < S, equality case S = (p^m+1)/2),

condition (3) reduces to q^i < p^m.

Proof. p, q odd ⟹ 2·((q-1)/2) = q-1 and 2·((p^m+1)/2) = p^m+1. From hTS, 2T < p^m + 1, so 2T ≤ p^m. From hlo, 2·((q-1)/2·G i + 1) ≤ 2T, i.e. (q-1)·G i + 2 ≤ 2T ≤ p^m. The golden identity (q-1)·G i = q^i - 1 then gives (q^i - 1) + 2 ≤ p^m, i.e. q^i + 1 ≤ p^m, hence q^i < p^m.

The least strictly-good base-q index above the top bad index (KERNEL-CLEAN)

leastGoodAbove q n is the least index i > j = topBadIndex q n whose base-q digit is < B = (q-1)/2 (STRICTLY good). It exists because base-q digits eventually vanish (out of range they read 0 < B for q ≥ 3). We expose it via Nat.find, supplying the existence proof.

def Egrs75.P4.StrictGoodAt (q i n : ℕ) : Prop

The strictly-good base-q digit predicate at index i: n / q^i % q < (q-1)/2.

Equations

• Egrs75.P4.StrictGoodAt q i n = (n / q ^ i % q < (q - 1) / 2)

@[implicit_reducible]

instance Egrs75.P4.instDecidableStrictGoodAt (q i n : ℕ) : Decidable (StrictGoodAt q i n)

Equations

• Egrs75.P4.instDecidableStrictGoodAt q i n = id inferInstance

theorem Egrs75.P4.exists_strictGood_above {q n : ℕ} (hq : 3 ≤ q) (_hbad : 0 < LeafInduction.badCountQ q n) : ∃ (i : ℕ), RepairDV.topBadIndex q n < i ∧ StrictGoodAt q i n

There is a strictly-good index above j = topBadIndex q n (KERNEL-CLEAN): for any i ≥ length the digit reads 0, and 0 < (q-1)/2 since q ≥ 3.

noncomputable def Egrs75.P4.leastGoodAbove {q n : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) : ℕ

leastGoodAbove q n: the least strictly-good base-q index > topBadIndex q n, defined for q ≥ 3 and a positive bad count. Carries the existence witness.

Equations

• Egrs75.P4.leastGoodAbove hq hbad = Nat.find ⋯

theorem Egrs75.P4.topBad_lt_leastGoodAbove {q n : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) : RepairDV.topBadIndex q n < leastGoodAbove hq hbad

leastGoodAbove lies strictly above the top bad index (KERNEL-CLEAN).

theorem Egrs75.P4.strictGoodAt_leastGoodAbove {q n : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) : StrictGoodAt q (leastGoodAbove hq hbad) n

leastGoodAbove is strictly good (KERNEL-CLEAN).

theorem Egrs75.P4.not_strictGood_of_lt_leastGoodAbove {q n k : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) (hjk : RepairDV.topBadIndex q n < k) (hk : k < leastGoodAbove hq hbad) : ¬StrictGoodAt q k n

Minimality (KERNEL-CLEAN). No index strictly between j and leastGoodAbove is strictly good: any k with j < k < leastGoodAbove has (q-1)/2 < n / q^k % q — wait, this is ¬ StrictGoodAt, i.e. the digit is ≥ B. Combined with digit_good_above_top (≤ B) this pins the middle digits to exactly B.

theorem Egrs75.P4.middle_digit_eq {q n k : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) (hjk : RepairDV.topBadIndex q n < k) (hk : k < leastGoodAbove hq hbad) : n / q ^ k % q = (q - 1) / 2

Middle digits are exactly B (KERNEL-CLEAN). For j < k < i = leastGoodAbove, the base-q digit of n at index k equals (q-1)/2. (digit_good_above_top gives ≤ B; non-strict-goodness gives ≥ B.)

The TAIL LOWER BOUND (the genuine base-q digit bookkeeping, KERNEL-CLEAN)

T = n % q^i ≥ B·G i + 1. The digits of n at indices j .. i-1 are b_j ≥ B+1 (the top oversized digit) and B, …, B (the middle digits, middle_digit_eq). Dropping the digits below j, the tail is ≥ b_j·q^j + B(q^{j+1} + … + q^{i-1}), which (using b_j ≥ B+1 and the golden identity) is ≥ B·G i + 1.

We prove it by a clean upward induction on the cutoff t from j+1 to i, telescoping the partial lower bound LB t := b_j·q^j + B·(q^{j+1} + … + q^{t-1}) via the base-q mod-recursion n % q^{t+1} = n % q^t + q^t·(n/q^t % q).

theorem Egrs75.P4.mod_pow_succ (n q t : ℕ) : n % q ^ (t + 1) = n % q ^ t + q ^ t * (n / q ^ t % q)

Base-q mod-recursion (KERNEL-CLEAN): n % q^{t+1} = n % q^t + q^t·(n / q^t % q).

theorem Egrs75.P4.tailLB_le_mod {q n : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) {t : ℕ} (htlo : RepairDV.topBadIndex q n < t) (hthi : t ≤ leastGoodAbove hq hbad) : Egrs75.P4.tailLB✝ q n (RepairDV.topBadIndex q n) t ≤ n % q ^ t

Inductive tail bound (KERNEL-CLEAN). For j = topBadIndex q n, i = leastGoodAbove, and any t with j < t ≤ i: tailLB q n j t ≤ n % q^t. The middle digits being exactly B (middle_digit_eq) feed the inductive step.

theorem Egrs75.P4.tail_ge {q n : ℕ} (hq : 3 ≤ q) (hbad : 0 < LeafInduction.badCountQ q n) : (q - 1) / 2 * geomQ q (leastGoodAbove hq hbad) + 1 ≤ n % q ^ leastGoodAbove hq hbad

THE TAIL LOWER BOUND (KERNEL-CLEAN). (q-1)/2 · G q i + 1 ≤ n % q^i, where i = leastGoodAbove. Assembles tailLB_le_mod (at t = i) with b_j ≥ B+1 and the golden identity: tailLB q n j i = b_j q^j + B(q^{j+1}+…+q^{i-1}) ≥ B·G i + 1.

THE ASSEMBLED CONDITION-(3) WINDOW PRODUCER (KERNEL-CLEAN)

cond3_window is the EGRS75 "window-nonempty / condition-(3)" producer for the ADD branch of the LOW case. Given a LowDigits q-failing number n (0 < badCountQ q n) whose paper tail T = n % q^i (at the least strictly-good index i = leastGoodAbove > j = topBadIndex) is below S = (p^m + 1)/2 (the ADD trigger T < S in the equality case A = (p-1)/2, B = (q-1)/2), it produces the clearing index i together with:

• topBadIndex q n < i (above the top oversized digit),
• n / q^i % q < (q-1)/2 (the digit at i is STRICTLY good, so b_i* = b_i + 1 ≤ B stays good after the ADD), and
• q^i < p^m (condition (3) — the carry interlock the ADD draw needs).

It chains tail_ge (the tail LOWER bound B·G i + 1 ≤ T, KERNEL-CLEAN) with cond3_of_tail_small (the algebraic interlock, KERNEL-CLEAN). This is the exact triple P2 consumes to draw U ∈ [q^i - T, p^m) from RoundUp.exists_lowDigits_between.

theorem Egrs75.P4.cond3_window {p q : ℕ} (_hp : 3 ≤ p) (hq : 3 ≤ q) (hpo : Odd p) (hqo : Odd q) (n m : ℕ) (hbad : 0 < LeafInduction.badCountQ q n) (hTS : n % q ^ leastGoodAbove hq hbad < (p ^ m + 1) / 2) : ∃ (i : ℕ), RepairDV.topBadIndex q n < i ∧ n / q ^ i % q < (q - 1) / 2 ∧ q ^ i < p ^ m

CONDITION-(3) WINDOW PRODUCER (KERNEL-CLEAN). For odd primes p, q ≥ 3, a number n with a bad base-q digit, and the ADD trigger n % q^i < (p^m + 1)/2 at the least strictly-good index i = leastGoodAbove, the clearing index i is above the top bad index, strictly good, and satisfies condition (3) q^i < p^m.

This is the producer the ADD branch consumes: i is a valid place to add (digit strictly good, above the top bad digit), and q^i < p^m guarantees the EGRS density Fact (RoundUp.exists_lowDigits_between at x = q^i - T) yields a correction < p^m that is base-p safe (via RepairDV.lowDigits_disjoint_add).