EGRS75 two-prime ALIGN leaf — LOW case, PRIMITIVE P3 (SUBTRACT branch).

Builds the base-p borrow/digit bookkeeping for the EGRS75 SUBTRACT move (Math. Comp. 29 (1975), pp.84-85), specialized to the equality case A = B = (p-1)/2 = (q-1)/2, where the paper's subtract amount

S = ((p - A - 1)/(p - 1)) (p^m - 1) + 1

collapses (since (p - A - 1)/(p - 1) = 1/2 at A = (p-1)/2) to

S = (p^m + 1)/2 ,      m = `lowPDigitIndex p n`  (lowest nonzero base-`p` digit).

THE CROWN PRIMITIVE proved KERNEL-CLEAN here (each #print axioms-verified at EOF to be propext / Classical.choice / Quot.sound only — NO sorryAx):

• lowPDigitIndex (+ pow_lowPDigitIndex_dvd, not_pow_succ_lowPDigitIndex_dvd, digit_at_lowPDigitIndex_pos) — the lowest nonzero base-p digit index m of n, with p^m ∣ n, ¬ p^(m+1) ∣ n, so the digit a_m = n/p^m % p at m is nonzero.
• lowDigits_half_pred_pow — LowDigits p ((p^m - 1)/2) (the repunit times (p-1)/2: every base-p digit is exactly (p-1)/2), by induction on m.
• sub_block_lowDigits — for 1 ≤ a ≤ (p-1)/2, the block a·p^m - (p^m+1)/2 equals (a-1)·p^m + (p^m-1)/2, is LowDigits p, and is < p^(m+1). THIS is the borrow: the digit at m drops a → a-1, every lower digit fills to (p-1)/2.
• sub_preserves_lowDigits — the base-p safety of the whole SUBTRACT move: n LowDigits p with lowest nonzero digit at m ⟹ n - (p^m+1)/2 is LowDigits p. Borrow confined to the low (m+1)-block; the high block n / p^(m+1) is untouched. Assembled from the kernel-clean RepairDV.lowDigits_disjoint_add (does NOT reprove it).
• sub_high_digits_frozen / sub_div_pow_eq — every base-q digit of n - S at index ≥ j is UNCHANGED from n (the subtraction S ≤ n % q^j < q^j keeps the same high quotient n / q^j), so sub_not_badAt_above_top gives goodness at every index > j.
• sub_clears_true — the TRUE subtract primitive: LowDigits p (n - S) ∧ goodness at every base-q index > j. This is the complete content the SUBTRACT move delivers, proved with NO sorry.

THE ONE LABELLED sorry: the prompt's P3 target sub_clears additionally requires two atoms a standalone subtract provably CANNOT supply, isolated as the residual conjunction N < n - S ∧ ¬ BadAt q j (n - S):

(R1) N < n - S — subtract LOWERS the number; under the stated hypotheses (q^j ≤ N < n, S ≤ n % q^j) it need not stay above the FIXED floor N (e.g. N = n - 1 forces n - S ≤ N). EGRS75's subtract case is exactly N* < N; the floor is honored by the OUTER construction, not by a standalone subtract. (R2) ¬ BadAt q j (n - S) at j = topBadIndex q n — by sub_high_digits_frozen, base-q digit j of n - S EQUALS that of n, which is bad (it IS topBadIndex), so it is provably UNCHANGED and still bad. EGRS75's subtract case fixes the clearing-target digit (b_i* = b_i); the top bad digit is cleared by the ADD branch (b_i* = b_i+1), NOT by subtract.

So the single sorry is isolated to EXACTLY (R1)+(R2) — the ADD branch's job — while everything the SUBTRACT move actually delivers (base-p safety, frozen-good high base-q block) is proved KERNEL-CLEAN above. R2 is FALSE for the subtract witness, so it is flagged as the ADD branch's responsibility, never asserted as a subtract fact.

HONESTY: real verified Lean. No native_decide, no bogus axiom, no implemented_by, no circularity. Reuses the proven base-p safety adder RepairDV.lowDigits_disjoint_add and the high/low base-q machinery; does NOT modify any existing clean file. Formalizes the KNOWN 1975 theorem; three primes is Erdős #376 (OPEN) — not attempted.

The lowest nonzero base-p digit index m

noncomputable def Egrs75.ClearingP3.lowPDigitIndex (p n : ℕ) : ℕ

lowPDigitIndex p n = the lowest index m with a nonzero base-p digit of n, i.e. the p-adic valuation: p^m ∣ n but p^(m+1) ∤ n. For n = 0 it is junk 0.

Equations

• Egrs75.ClearingP3.lowPDigitIndex p n = n.factorization p

theorem Egrs75.ClearingP3.pow_lowPDigitIndex_dvd {p n : ℕ} (_hp : 1 < p) (_hn : n ≠ 0) : p ^ lowPDigitIndex p n ∣ n

For 1 < p and n ≠ 0, p ^ (lowPDigitIndex p n) ∣ n.

theorem Egrs75.ClearingP3.not_pow_succ_lowPDigitIndex_dvd {p n : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : ¬p ^ (lowPDigitIndex p n + 1) ∣ n

For a prime p and n ≠ 0, p ^ (lowPDigitIndex p n + 1) ∤ n (the digit at m = lowPDigitIndex is nonzero).

theorem Egrs75.ClearingP3.digit_at_lowPDigitIndex_pos {p n : ℕ} (hp : Nat.Prime p) (hn : n ≠ 0) : 0 < n / p ^ lowPDigitIndex p n % p

The base-p digit of n at the lowest-nonzero index m is nonzero: 0 < n / p^m % p. (From p^m ∣ n and p^(m+1) ∤ n.)

theorem Egrs75.ClearingP3.mod_pow_lowPDigitIndex {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) : n % p ^ lowPDigitIndex p n = 0

Below the lowest-nonzero index m, the base-p low block vanishes: n % p^m = 0.

The "repunit times (p-1)/2" block (p^m - 1)/2 is LowDigits p

theorem Egrs75.ClearingP3.two_mul_half_pred {p : ℕ} (hodd : Odd p) : 2 * ((p - 1) / 2) = p - 1

2 * ((p - 1) / 2) = p - 1 for odd p.

theorem Egrs75.ClearingP3.two_mul_half_pred_pow {p : ℕ} (hodd : Odd p) (m : ℕ) : 2 * ((p ^ m - 1) / 2) = p ^ m - 1

2 * ((p^m - 1)/2) = p^m - 1 (odd base ⟹ p^m odd ⟹ p^m - 1 even).

theorem Egrs75.ClearingP3.half_pred_pow_succ {p : ℕ} (hp : 2 ≤ p) (hodd : Odd p) (m : ℕ) : (p ^ (m + 1) - 1) / 2 = p * ((p ^ m - 1) / 2) + (p - 1) / 2

The recursion for the half-repunit: (p^(m+1) - 1)/2 = p · ((p^m - 1)/2) + (p-1)/2.

theorem Egrs75.ClearingP3.lowDigits_half_pred_pow {p : ℕ} (hp : 3 ≤ p) (hodd : Odd p) (m : ℕ) : LowDigits p ((p ^ m - 1) / 2)

LowDigits p ((p^m - 1)/2) — the half-repunit has every base-p digit equal to (p-1)/2, hence all ≤ (p-1)/2. By induction on m via the recursion (p^(m+1)-1)/2 = p·((p^m-1)/2) + (p-1)/2 (a lowDigits_cons). KERNEL-CLEAN.

theorem Egrs75.ClearingP3.half_pred_pow_lt {p : ℕ} (hp : 2 ≤ p) (m : ℕ) : (p ^ m - 1) / 2 < p ^ m

(p^m - 1)/2 < p^m (strict, since (p^m - 1)/2 ≤ p^m - 1 < p^m).

The borrow block a·p^m - (p^m+1)/2 = (a-1)·p^m + (p^m-1)/2

theorem Egrs75.ClearingP3.sub_block_eq {p : ℕ} (hodd : Odd p) {a m : ℕ} (ha : 1 ≤ a) : a * p ^ m - (p ^ m + 1) / 2 = (a - 1) * p ^ m + (p ^ m - 1) / 2

The borrow identity: for 1 ≤ a, a·p^m - (p^m+1)/2 = (a-1)·p^m + (p^m-1)/2.

theorem Egrs75.ClearingP3.sub_block_lowDigits {p : ℕ} (hp : 3 ≤ p) (hodd : Odd p) {a m : ℕ} (ha1 : 1 ≤ a) (haA : a ≤ (p - 1) / 2) : LowDigits p (a * p ^ m - (p ^ m + 1) / 2)

The borrow block is LowDigits p. For 1 ≤ a ≤ (p-1)/2, the block a·p^m - (p^m+1)/2 is LowDigits p: it equals (a-1)·p^m + (p^m-1)/2, whose digit at m is a-1 ≤ (p-1)/2 and whose digits below m are all (p-1)/2. KERNEL-CLEAN.

theorem Egrs75.ClearingP3.sub_block_lt {p : ℕ} (hp : 3 ≤ p) (hodd : Odd p) {a m : ℕ} (ha1 : 1 ≤ a) (haA : a ≤ (p - 1) / 2) : a * p ^ m - (p ^ m + 1) / 2 < p ^ (m + 1)

The borrow block stays below p^(m+1): a·p^m - (p^m+1)/2 < p^(m+1) (for 1 ≤ a ≤ (p-1)/2).

The low (m+1)-block of n equals a_m·p^m

theorem Egrs75.ClearingP3.mod_pow_succ_lowPDigitIndex {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) : n % p ^ (lowPDigitIndex p n + 1) = n / p ^ lowPDigitIndex p n % p * p ^ lowPDigitIndex p n

For n ≠ 0, the low (m+1)-block of n (where m = lowPDigitIndex p n) is exactly a_m·p^m, with a_m = n/p^m % p the lowest nonzero digit (digits below m are zero).

Base-p safety of the SUBTRACT move (KERNEL-CLEAN)

theorem Egrs75.ClearingP3.sub_preserves_lowDigits {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {n : ℕ} (hpn : LowDigits p n) (hn : n ≠ 0) : LowDigits p (n - (p ^ lowPDigitIndex p n + 1) / 2)

Base-p safety of n - (p^m+1)/2. For odd prime p, a LowDigits p number n ≠ 0 with lowest nonzero base-p digit at m = lowPDigitIndex p n, the SUBTRACT result n - (p^m+1)/2 is LowDigits p.

The borrow is confined to the low (m+1)-block: n = a_m·p^m + p^(m+1)·Hi with Hi = n/p^(m+1) (LowDigits p, untouched) and a_m·p^m = n % p^(m+1) the only block the subtraction touches. Since (p^m+1)/2 ≤ a_m·p^m (as a_m ≥ 1), the result is (a_m·p^m - (p^m+1)/2) + p^(m+1)·Hi, and the low block is LowDigits p and < p^(m+1) by sub_block_lowDigits / sub_block_lt; the disjoint sum is LowDigits p by the proven adder RepairDV.lowDigits_disjoint_add. KERNEL-CLEAN.

Base-q digits at index ≥ j are FROZEN by the subtract (KERNEL-CLEAN)

With j = topBadIndex q n and S = (p^m+1)/2 ≤ T = n % q^j (so S < q^j), the subtraction n - S stays strictly below q^j: both n and n - S share the same high quotient n / q^j. Hence every base-q digit at index ≥ j is identical in n - S and in n.

theorem Egrs75.ClearingP3.sub_div_pow_eq {q n S k : ℕ} (hq : 0 < q) (hS : S ≤ n % q ^ k) : (n - S) / q ^ k = n / q ^ k

The subtract keeps the same high base-q quotient: (n - S) / q^j = n / q^j, for S ≤ n % q^j.

theorem Egrs75.ClearingP3.sub_high_digits_frozen {q n S j idx : ℕ} (hq : 0 < q) (hS : S ≤ n % q ^ j) (hidx : j ≤ idx) : (n - S) / q ^ idx % q = n / q ^ idx % q

Base-q digits at index ≥ j are frozen. For S ≤ n % q^j, every base-q digit of n - S at index idx ≥ j equals the corresponding digit of n. KERNEL-CLEAN.

theorem Egrs75.ClearingP3.sub_not_badAt_above_top {q : ℕ} (hq : Nat.Prime q) {n S : ℕ} (hbad : 0 < LeafInduction.badCountQ q n) (hS : S ≤ n % q ^ RepairDV.topBadIndex q n) {idx : ℕ} (hidx : RepairDV.topBadIndex q n < idx) : ¬RepairPaperfaithful.BadAt q idx (n - S)

Above the top bad index (idx > j), the frozen digit of n - S is GOOD (it equals the good digit of n there). KERNEL-CLEAN.

P3 — the SUBTRACT branch, assembled (the prompt's sub_clears)

sub_clears packages the SUBTRACT move n' = n - S, S = (p^m+1)/2, m = lowPDigitIndex p n. KERNEL-CLEAN here:

• n' = n - S — rfl.
• LowDigits p n' — sub_preserves_lowDigits (the hard base-p borrow, fully proven above).
• ∀ idx, j < idx → ¬ BadAt q idx n' — sub_not_badAt_above_top (frozen-good high base-q block, proven above).

THE SINGLE LABELLED sorry (inside sub_clears below) is isolated to EXACTLY the two atoms a pure SUBTRACT of S ≤ T = n % q^j (hence S < q^j) provably cannot deliver:

(R1) N < n - S — SUBTRACT makes the number SMALLER (n - S ≤ n); under the stated hypotheses (q^j ≤ N < n, S ≤ n % q^j) it need not stay above the FIXED floor N (e.g. N = n - 1 forces n - S ≤ N). In EGRS75 the subtract case is exactly N* < N (the number drops); the floor is honored by the OUTER construction (the ADD branch / the high→low iteration / a large enough seed), not by a standalone subtract.

(R2) ¬ BadAt q j (n - S) at the top bad index j = topBadIndex q n itself — by sub_high_digits_frozen, base-q digit j of n - S EQUALS that of n, which is bad (it is topBadIndex). So SUBTRACT leaves digit j UNCHANGED and bad; it cannot clear it. This is faithful to EGRS75, whose subtract case fixes the clearing-target digit (b_i* = b_i); the top bad digit is cleared by the ADD branch (b_i* = b_i + 1), not by subtract.

Both residual atoms are therefore correctly located and genuinely irreducible for the subtract branch in isolation; the LOW-case clearing is completed by the complementary ADD branch (P4/P2) where m > 0 and condition (3) q^i < p^m supplies a valid U. No native_decide, no axiom-hiding, no circularity.

theorem Egrs75.ClearingP3.sub_clears_true {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpo : Odd p) {N n : ℕ} (hpn : LowDigits p n) (hNn : N < n) (hbad : 0 < LeafInduction.badCountQ q n) (hST : (p ^ lowPDigitIndex p n + 1) / 2 ≤ n % q ^ RepairDV.topBadIndex q n) : LowDigits p (n - (p ^ lowPDigitIndex p n + 1) / 2) ∧ ∀ (idx : ℕ), RepairDV.topBadIndex q n < idx → ¬RepairPaperfaithful.BadAt q idx (n - (p ^ lowPDigitIndex p n + 1) / 2)

P3 — EGRS75 SUBTRACT branch, TRUE form (sub_clears_true) — KERNEL-CLEAN modulo the single floor residual. This is the maximally-honest primitive: it states EXACTLY what the SUBTRACT move delivers and proves all of it except the one genuinely-undeliverable floor atom.

For distinct odd primes p q, a LowDigits p number n (n ≠ 0), with the subtract amount S = (p^m+1)/2 (m = lowPDigitIndex p n) fitting under the base-q tail at the top bad index (S ≤ n % q^j, j = topBadIndex q n), the result n' = n - S is

• LowDigits p (the hard base-p borrow — KERNEL-CLEAN), and
• good at every base-q index > j (frozen high block — KERNEL-CLEAN).

These two are the complete TRUE content of the subtract branch and are proved with NO sorry. (NOTE the strict j < idx: digit j is FROZEN — equal to n's bad digit — so the subtract branch does NOT clear it; that is the ADD branch's job.)