Erdős Problem #376 — first Lean target (the Kummer digit bridge, NOT the open infinitude claim).

Recon: ~/Knowledge/Construct/recon/erdos_376.md Builds on the proven Kummer infra in ConstructProofs/ConcreteMath/KummerBridge.lean (sub_one_mul_padicValNat_centralBinom: (p-1)·ν_p(C(2n,n)) = 2·S_p(n) − S_p(2n)).

GOAL (proved here, zero sorry):

Nat.Coprime (Nat.centralBinom n) 105 ↔ LowDoubleDigits 3 n ∧ LowDoubleDigits 5 n ∧ LowDoubleDigits 7 n

where LowDoubleDigits p n := ∀ d ∈ Nat.digits p n, 2*d < p (every base-3 digit ≤ 1, every base-5 digit ≤ 2, every base-7 digit ≤ 3). 105 = 3·5·7, so coprimality to 105 splits into the three prime conditions, and for each prime Kummer says: p ∤ C(2n,n) iff doubling n in base p has no carry iff every base-p digit d of n satisfies 2d < p.

This is the finite, exact bridge (recon §7 "Concrete first Lean target"). It does NOT touch the open statement {n | …}.Infinite.

The carry machinery below is the general-base-p analogue of the base-3 doubling transducer already proven in ConcreteMath/CarryTransducerCorrectness.lean.

The digit predicate (matches recon §7)

def Egrs75.Erdos376.LowDoubleDigits (p n : ℕ) : Prop

LowDoubleDigits p n: doubling n in base p produces no carry, i.e. every base-p digit d of n satisfies 2*d < p. For p = 3 this is "all digits ≤ 1", for p = 5 "≤ 2", for p = 7 "≤ 3".

Equations

• Egrs75.Erdos376.LowDoubleDigits p n = ∀ d ∈ p.digits n, 2 * d < p

General-base doubling carry transducer

We double a little-endian base-b digit list, carrying as needed. This mirrors the base-3 ternaryDouble* transducer in ConcreteMath/CarryTransducerCorrectness.lean, generalized to any base.

def Egrs75.Erdos376.doubleCarryStep (b carry d : ℕ) : ℕ

One step of the base-b doubling transducer: outgoing carry (0 or 1) given incoming carry and the current digit.

Equations

• Egrs75.Erdos376.doubleCarryStep b carry d = if b ≤ 2 * d + carry then 1 else 0

def Egrs75.Erdos376.doubleDigitsAux (b : ℕ) : List ℕ → ℕ → List ℕ

The little-endian digit list produced by doubling ds (base b) with an incoming carry.

Equations

• Egrs75.Erdos376.doubleDigitsAux b [] x✝ = [x✝]
• Egrs75.Erdos376.doubleDigitsAux b (d :: ds) x✝ = (2 * d + x✝) % b :: Egrs75.Erdos376.doubleDigitsAux b ds (Egrs75.Erdos376.doubleCarryStep b x✝ d)

def Egrs75.Erdos376.doubleCarryCountAux (b : ℕ) : List ℕ → ℕ → ℕ

Number of outgoing carries when doubling ds (base b) with an incoming carry.

Equations

• Egrs75.Erdos376.doubleCarryCountAux b [] x✝ = 0
• Egrs75.Erdos376.doubleCarryCountAux b (d :: ds) x✝ = Egrs75.Erdos376.doubleCarryStep b x✝ d + Egrs75.Erdos376.doubleCarryCountAux b ds (Egrs75.Erdos376.doubleCarryStep b x✝ d)

def Egrs75.Erdos376.doubleCarryCount (b : ℕ) (ds : List ℕ) : ℕ

Carries when doubling n in base b, given the little-endian digit list.

Equations

• Egrs75.Erdos376.doubleCarryCount b ds = Egrs75.Erdos376.doubleCarryCountAux b ds 0

Step facts

theorem Egrs75.Erdos376.doubleCarryStep_le_one (b carry d : ℕ) : doubleCarryStep b carry d ≤ 1

theorem Egrs75.Erdos376.doubleDigitsAux_length (b : ℕ) (ds : List ℕ) (carry : ℕ) : (doubleDigitsAux b ds carry).length = ds.length + 1

theorem Egrs75.Erdos376.doubleCarryStep_eq_div {b carry d : ℕ} (_hb : 2 ≤ b) (hcarry : carry ≤ 1) (hd : d < b) : doubleCarryStep b carry d = (2 * d + carry) / b

theorem Egrs75.Erdos376.doubleCarryStep_local {b carry d : ℕ} (hb : 2 ≤ b) (hcarry : carry ≤ 1) (hd : d < b) : (2 * d + carry) % b + b * doubleCarryStep b carry d = 2 * d + carry

Local conservation: outDigit + b · carryOut = 2d + carryIn.

Aux-list facts

theorem Egrs75.Erdos376.doubleDigitsAux_lt_base {b : ℕ} (hb : 2 ≤ b) {ds : List ℕ} {carry : ℕ} : carry < b → (∀ d ∈ ds, d < b) → ∀ x ∈ doubleDigitsAux b ds carry, x < b

theorem Egrs75.Erdos376.doubleDigitsAux_ofDigits {b : ℕ} (hb : 2 ≤ b) {ds : List ℕ} {carry : ℕ} : carry ≤ 1 → (∀ d ∈ ds, d < b) → Nat.ofDigits b (doubleDigitsAux b ds carry) = 2 * Nat.ofDigits b ds + carry

ofDigits of the doubled list equals 2 · ofDigits ds + carry.

theorem Egrs75.Erdos376.doubleDigitsAux_sum {b : ℕ} (hb : 2 ≤ b) {ds : List ℕ} {carry : ℕ} : carry ≤ 1 → (∀ d ∈ ds, d < b) → (doubleDigitsAux b ds carry).sum + (b - 1) * doubleCarryCountAux b ds carry = 2 * ds.sum + carry

Conservation with carry count: S(2n via aux) + (b−1)·carries = 2·S(ds) + carry.

From the aux list to the genuine base-b digits of 2n

theorem Egrs75.Erdos376.digitExcess_eq {b : ℕ} (hb : 2 ≤ b) (n : ℕ) : 2 * (b.digits n).sum - (b.digits (2 * n)).sum = (b - 1) * doubleCarryCount b (b.digits n)

The Kummer digit excess equals (b−1) times the number of doubling carries. (b ≥ 2.)

The no-carry ⇔ small-digits characterisation

theorem Egrs75.Erdos376.carryCount_eq_zero_iff {b : ℕ} (_hb : 2 ≤ b) (ds : List ℕ) : doubleCarryCountAux b ds 0 = 0 ↔ ∀ d ∈ ds, 2 * d < b

With carry-in 0, the doubling carry count is 0 iff every digit is small. (Both directions need only b ≥ 2.)

Per-prime Kummer coprimality characterisation

theorem Egrs75.Erdos376.coprime_centralBinom_prime_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : n.centralBinom.Coprime p ↔ LowDoubleDigits p n

For a prime p, C(2n,n) is coprime to p iff every base-p digit of n doubles without carry, i.e. LowDoubleDigits p n.

Main bridge for 105 = 3·5·7

theorem Egrs75.Erdos376.centralBinom_coprime_105_iff (n : ℕ) : n.centralBinom.Coprime 105 ↔ LowDoubleDigits 3 n ∧ LowDoubleDigits 5 n ∧ LowDoubleDigits 7 n

Erdős #376 Kummer bridge. C(2n,n) is coprime to 105 exactly when all its base-3 digits are ≤ 1, all its base-5 digits are ≤ 2, and all its base-7 digits are ≤ 3. (This is the finite digit characterisation — OEIS A030979 — not the open infinitude claim.)

Sanity: the bridge agrees with OEIS A030979 on small witnesses