EGRS75 two-prime — digit toolkit for the single μ-move (2026-06-12).

NEW file. Local, self-contained digit arithmetic consumed by EgrsMuFinish_20260612.lean. Deliberately does NOT import EgrsFinish_core (so that file can later import the μ-closure without a cycle); the two tiny overlaps (mem_badIndexSet_iff-style bridge) are re-proved here.

CONTENTS (all KERNEL-CLEAN, no sorry): • div_mul_pow_mono — truncation at a lower scale keeps a larger value. • add_carry_decomp — n+U = R + q^i·(H+1) under a single carry. • add_div_pow_eq — (n+U)/q^i = n/q^i + 1 (single carry). • add_digit_i — digit i becomes b_i + 1 (when b_i < q-1). • add_high_frozen — digits above i are frozen (when b_i < q-1). • add_low_digit — digits below i of n+U are the digits of R. • badAt_of_mem / topBad_lt_of_good_from — top-bad bound from a goodness ray. • staircase — THE KEY: a number < ((q^i)-1)/2 - 1 (i.e. 2R+3 ≤ q^i) has, below i, a strictly-good digit k with all digits in (k,i) exactly B = (q-1)/2. This is the EGRS75 p.85 case-(c) "staircase" fact, and it is what makes the clearing index DROP after every ADD move.

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

Truncation monotonicity

theorem Egrs75.MoveDigits.div_mul_pow_mono {q : ℕ} (_hq : 0 < q) (n : ℕ) {a b : ℕ} (hab : a ≤ b) : n / q ^ b * q ^ b ≤ n / q ^ a * q ^ a

Keeping MORE high digits keeps a larger (or equal) value: n/q^b · q^b ≤ n/q^a · q^a for a ≤ b.

Single-carry ADD arithmetic

theorem Egrs75.MoveDigits.add_carry_decomp {q : ℕ} (hq : 1 ≤ q) (n U i : ℕ) (hlo : q ^ i ≤ n % q ^ i + U) : n + U = n % q ^ i + U - q ^ i + q ^ i * (n / q ^ i + 1)

The carry decomposition n + U = R + q^i·(H+1), R = (T+U) − q^i, H = n / q^i, valid when q^i ≤ T + U with T = n % q^i.

theorem Egrs75.MoveDigits.add_div_pow_eq {q : ℕ} (hq : 1 < q) (n U i : ℕ) (hlo : q ^ i ≤ n % q ^ i + U) (hhi : n % q ^ i + U < 2 * q ^ i) : (n + U) / q ^ i = n / q ^ i + 1

Under a single carry (q^i ≤ T+U < 2q^i), the block above i increments: (n+U)/q^i = n/q^i + 1.

theorem Egrs75.MoveDigits.succ_div_pow_eq {q : ℕ} (hq : 1 < q) {H : ℕ} (hH : H % q < q - 1) {s : ℕ} (hs : 1 ≤ s) : (H + 1) / q ^ s = H / q ^ s

The increment does not cascade: (H+1)/q^s = H/q^s for s ≥ 1 when the units digit of H is below q − 1.

theorem Egrs75.MoveDigits.add_digit_i {q : ℕ} (hq : 1 < q) (n U i : ℕ) (hlo : q ^ i ≤ n % q ^ i + U) (hhi : n % q ^ i + U < 2 * q ^ i) (hbi : n / q ^ i % q < q - 1) : (n + U) / q ^ i % q = n / q ^ i % q + 1

Digit at i becomes b_i + 1 under a single carry, when b_i < q − 1.

theorem Egrs75.MoveDigits.add_high_frozen {q : ℕ} (hq : 1 < q) (n U i idx : ℕ) (hlo : q ^ i ≤ n % q ^ i + U) (hhi : n % q ^ i + U < 2 * q ^ i) (hbi : n / q ^ i % q < q - 1) (hidx : i < idx) : (n + U) / q ^ idx % q = n / q ^ idx % q

Digits above i are frozen under a single carry, when b_i < q − 1.

theorem Egrs75.MoveDigits.add_low_digit {q : ℕ} (hq : 1 < q) (n U i t : ℕ) (ht : t < i) (hlo : q ^ i ≤ n % q ^ i + U) : (n + U) / q ^ t % q = (n % q ^ i + U - q ^ i) / q ^ t % q

Digits below i of n+U are the digits of the new tail R.

Top-bad bound from a goodness ray

theorem Egrs75.MoveDigits.mem_badIndexSet_iff' {q n i : ℕ} (hq : 1 < q) : i ∈ RepairDV.badIndexSet q n ↔ RepairPaperfaithful.BadAt q i n

Membership in badIndexSet is exactly BadAt (local copy; the original lives in EgrsFinish_core, which this file must not import).

theorem Egrs75.MoveDigits.topBad_lt_of_good_from {q n x : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) (hgood : ∀ (idx : ℕ), x ≤ idx → n / q ^ idx % q ≤ (q - 1) / 2) : RepairDV.topBadIndex q n < x

If every digit at index ≥ x is good, the top bad index is < x.

THE STAIRCASE (EGRS75 p.85, case (c))

A tail R with 2R + 3 ≤ q^i (strictly below the all-B value (q^i−1)/2) has a strictly-good digit k < i such that every digit in (k, i) is exactly B. Consequence: after the tight-window ADD, the new clearing index drops strictly below the old one — the μ-measure first coordinate falls.

theorem Egrs75.MoveDigits.staircase {q : ℕ} (hq3 : 3 ≤ q) (hqo : Odd q) (i R : ℕ) : 2 * R + 3 ≤ q ^ i → ∃ k < i, R / q ^ k % q < (q - 1) / 2 ∧ ∀ (t : ℕ), k < t → t < i → R / q ^ t % q = (q - 1) / 2

The staircase lemma (KERNEL-CLEAN).