EGRS75 two-prime ALIGN leaf — route digitvector: the carry-controlled repair step.

This file attacks the SINGLE remaining gap of the EGRS two-prime theorem, repair_step (EgrsLeaf_induction.lean:154), via an explicit base-q digit-vector manipulation. The target, with the SAME signature as the scaffolding's repair_step, is:

for distinct odd primes p q, if LowDigits p n and 0 < badCountQ q n, then ∃ n', n < n' ∧ LowDigits p n' ∧ badCountQ q n' < badCountQ q n.

ROUTE digitvector. Model n by its base-q digit list, locate the highest oversized base-q digit at index j, split n = q^(j+1)·Hi + Lo, construct an additive LowDigits p correction U (drawn from the per-base density Fact RoundUp.exists_lowDigits_between, i.e. EGRS's interval at (p-1)/A = 2) placed at position j, and prove by direct base-q/base-p digit bookkeeping that the bad base-q count strictly drops while no oversized base-p digit is created (the "makes essential use of condition (3)" step).

This file IMPORTS the existing kernel-clean definitions (LowDigits, badDigitsQ, badCountQ) and the density Fact; it does NOT modify any pre-existing clean file.

HONESTY. Real Lean. Everything here is kernel-clean (propext / Classical.choice / Quot.sound only) EXCEPT possibly one clearly-labelled sorry at the genuinely-hardest residual carry-invariant, reported precisely in the run summary. No native_decide, no bogus axiom, no implemented_by, no circular hypothesis. Formalizes the KNOWN theorem EGRS75 (Math. Comp. 29 (1975), the repair Lemma p.84, case κ₁ = κ₂ = 1/2). Three primes is Erdős #376 (OPEN); not attempted.

Local notation and the "oversized digit" predicate

@[reducible]

def Egrs75.RepairDV.bigQ (q d : ℕ) : Bool

The base-q "oversized" test: a digit d is oversized iff (q-1)/2 < d.

Equations

• Egrs75.RepairDV.bigQ q d = decide ((q - 1) / 2 < d)

theorem Egrs75.RepairDV.badCountQ_eq (q n : ℕ) : LeafInduction.badCountQ q n = (List.filter (fun (d : ℕ) => bigQ q d) (q.digits n)).length

badCountQ unfolded as a filter-length over the base-q digit list.

theorem Egrs75.RepairDV.badCount_filter_append (q : ℕ) (L₁ L₂ : List ℕ) : (List.filter (fun (d : ℕ) => bigQ q d) (L₁ ++ L₂)).length = (List.filter (fun (d : ℕ) => bigQ q d) L₁).length + (List.filter (fun (d : ℕ) => bigQ q d) L₂).length

badCountQ additivity over filter/append: the bad count of a digit list that splits as L₁ ++ L₂ is the sum of the two bad counts. Used to read the bad count off a high/low decomposition of n.

theorem Egrs75.RepairDV.badCount_filter_replicate_zero (q k : ℕ) : (List.filter (fun (d : ℕ) => bigQ q d) (List.replicate k 0)).length = 0

Appending zeros to a digit list does not change its bad count (since 0 is never oversized for q ≥ 1).

High/low split of the base-q digit list and bad count

For n = q^k · Hi + Lo with Lo < q^k and Hi > 0, the base-q digit list of n is (digits q Lo) ++ (zero padding to length k) ++ (digits q Hi), so the bad count splits additively: badCountQ q n = badCountQ q Lo + badCountQ q Hi. This is the digit-vector view that lets the repair reason about the high block and low block independently.

theorem Egrs75.RepairDV.digits_split {q k Lo Hi : ℕ} (hq : 1 < q) (hLo : Lo < q ^ k) (hHi : 0 < Hi) : q.digits (Lo + q ^ k * Hi) = q.digits Lo ++ List.replicate (k - (q.digits Lo).length) 0 ++ q.digits Hi

Base-q digit list of Lo + q^k · Hi is digits Lo ++ zeros ++ digits Hi, for Lo < q^k, Hi > 0, q ≥ 2.

theorem Egrs75.RepairDV.badCountQ_split {q k Lo Hi : ℕ} (hq : 1 < q) (hLo : Lo < q ^ k) (hHi : 0 < Hi) : LeafInduction.badCountQ q (Lo + q ^ k * Hi) = LeafInduction.badCountQ q Lo + LeafInduction.badCountQ q Hi

Bad-count split (KERNEL-CLEAN). For n = Lo + q^k · Hi with Lo < q^k, Hi > 0, q ≥ 2: the oversized-base-q-digit count is the sum of the low block's and the high block's bad counts.

Disjoint-support LowDigits p addition (KERNEL-CLEAN)

The base-p safety half of the repair: a LowDigits p correction U < p^k added to p^k · Hi (with Hi itself LowDigits p) keeps the result LowDigits p. Its base-p digit list is digits U ++ zeros ++ digits Hi, every entry of which is ≤ (p-1)/2. This is EGRS's "adding two (p,A)-good numbers with disjoint base-p supports keeps the result (p,A)-good" — the place where U < p^m (condition (3)) is used to guarantee no oversized base-p digit is created.

theorem Egrs75.RepairDV.lowDigits_disjoint_add {p k U Hi : ℕ} (hp : 1 < p) (hU : U < p ^ k) (hHi : 0 < Hi) (hUlow : LowDigits p U) (hHilow : LowDigits p Hi) : LowDigits p (U + p ^ k * Hi)

Disjoint-support LowDigits p addition (KERNEL-CLEAN). If U < p^k and both U and Hi are LowDigits p (and Hi > 0, p ≥ 2), then U + p^k · Hi is LowDigits p: its base-p digits are exactly those of U, of Hi, and padding zeros, all ≤ (p-1)/2.

The highest oversized base-q index (KERNEL-CLEAN)

When badCountQ q n > 0, there is at least one oversized base-q digit; we extract the highest such index j. Above j, every base-q digit is good. This j defines the decomposition scale k = j+1 for the repair (low block = digits 0..j, containing the bad digit at j; high block = digits > j, all good).

def Egrs75.RepairDV.badIndexSet (q n : ℕ) : Finset ℕ

The (decidable, finite, nonempty) set of oversized base-q digit positions of n, as indices into the digit list. i is oversized iff (q-1)/2 < n / q^i % q (= the i-th base-q digit) and i < length.

Equations

• Egrs75.RepairDV.badIndexSet q n = {i ∈ Finset.range (q.digits n).length | Egrs75.RepairDV.bigQ q ((q.digits n).getD i 0) = true}

theorem Egrs75.RepairDV.badIndexSet_nonempty {q n : ℕ} (_hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) : (badIndexSet q n).Nonempty

If the bad count is positive, the bad-index set is nonempty.

noncomputable def Egrs75.RepairDV.topBadIndex (q n : ℕ) : ℕ

The highest oversized base-q index of n (defined when the bad count is positive; otherwise junk 0).

Equations

• Egrs75.RepairDV.topBadIndex q n = if h : (Egrs75.RepairDV.badIndexSet q n).Nonempty then (Egrs75.RepairDV.badIndexSet q n).max' h else 0

theorem Egrs75.RepairDV.topBadIndex_mem {q n : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) : topBadIndex q n ∈ badIndexSet q n

The top bad index is itself a bad index: its base-q digit is oversized and it is within the digit list.

theorem Egrs75.RepairDV.le_topBadIndex {q n i : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) (hi : i ∈ badIndexSet q n) : i ≤ topBadIndex q n

Maximality: every bad index is ≤ topBadIndex.

Digit-at-index helper and the "high block is all good" fact (KERNEL-CLEAN)

getD_digits reads the i-th base-q digit as n / q^i % q. Combined with topBadIndex maximality, every base-q digit at index > topBadIndex is good, so the high block n / q^(topBadIndex+1) is LowDigits q (bad count 0).

theorem Egrs75.RepairDV.digit_good_above_top {q n i : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) (hi : topBadIndex q n < i) : n / q ^ i % q ≤ (q - 1) / 2

The base-q digit of n at any index strictly above topBadIndex q n is good (≤ (q-1)/2). Indices beyond the list read as 0 (also good); indices in range above the top bad index are good by maximality.

theorem Egrs75.RepairDV.highBlock_lowDigits {q n : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) : LowDigits q (n / q ^ (topBadIndex q n + 1))

High block is LowDigits q (KERNEL-CLEAN). With k = topBadIndex q n + 1, the high block Hi = n / q^k has no oversized base-q digit.

The low block carries the entire bad count, and it is positive (KERNEL-CLEAN)

With k = topBadIndex q n + 1, write n = Lo + q^k·Hi, Lo = n % q^k, Hi = n / q^k. The high block is LowDigits q (bad count 0), so by the split the entire bad count sits in the low block: badCountQ q n = badCountQ q Lo. And Lo ≥ 1 carries the oversized top digit, so badCountQ q Lo ≥ 1.

theorem Egrs75.RepairDV.digit_top_big {q n : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) : (q - 1) / 2 < n / q ^ topBadIndex q n % q

The base-q digit at index topBadIndex q n is itself oversized ((q-1)/2 < n / q^(topBadIndex) % q).

theorem Egrs75.RepairDV.badCount_eq_lowBlock {q n : ℕ} (hq : 1 < q) (hbad : 0 < LeafInduction.badCountQ q n) : LeafInduction.badCountQ q n = LeafInduction.badCountQ q (n % q ^ (topBadIndex q n + 1))

Decomposition (KERNEL-CLEAN). With k = topBadIndex q n + 1, the bad count of n equals the bad count of its low block n % q^k, and that is ≥ 1. Moreover the high block n / q^k is positive (the top bad digit forces n ≥ q^(k-1) > 0, and since the digit at topBadIndex is nonzero the number extends at least that far).

The EGRS carry-controlled correction (THE RESIDUAL — one labelled sorry)

Everything above is kernel-clean digit-vector infrastructure. What remains is the single irreducible EGRS75 carry-control content: the existence of the additive LowDigits p correction that clears the top oversized base-q digit without creating an oversized base-p digit and without a net increase in the base-q bad count.

We isolate it as repair_correction, stated in the decomposed coordinates produced above (top bad index j, scale k = j+1, low block Lo = n % q^k, high block Hi = n / q^k, with Hi already LowDigits q and Lo carrying the bad count ≥ 1). The statement asks exactly for the corrected number n':

n < n', LowDigits p n', badCountQ q n' < badCountQ q Lo.

This is the EGRS Lemma (Math. Comp. 29 (1975) p.84) in the equality case A = B = (p-1)/2 = (q-1)/2. Its proof "makes essential use of the condition (3)" (q^i − 1 < ((q-1)/B)((p−A−1)/(p-1))(p^m − 1), EGRS75 p.85 eq. (3)), which couples the base-q clearing window to the base-p safety margin U < p^m — the single place the two bases interact, and the part Bloom–Croot (arXiv:2509.02835 §1) explicitly defer to [4] and that current Mathlib does not package (no effective equidistribution, no carry bookkeeping). The intended correction source is RoundUp.exists_lowDigits_between (the density Fact = EGRS's interval at (p-1)/A = 2); the residual is the carry-controlled PLACEMENT of that correction.

ONE labelled sorry, reported precisely. No native_decide, no bogus axiom, no circularity.