The factorial number system (for Erdős #403)

The unique mixed-radix representation n = ∑_{i≥1} dᵢ·i! with 0 ≤ dᵢ ≤ i, where dᵢ = (n / i!) mod (i+1). A number is a sum of distinct factorials (indices ≥ 1) iff every digit is ≤ 1. This is the engine for the sharp form m ≤ 7 of #403: the question becomes a digit condition on 2^m.

This file builds the infrastructure the sharp endgame needs:

• factDigit, the i-th factorial-base digit,
• factDigit_sum_factorial: the digits of a sum of distinct factorials are its indicator,
• not_factSum_of_digits: the non-representability criterion Erdos403.Sharp calls on 2^m.

(The general reconstruction lemmas n = ∑ dᵢ·i!, unused by the final proof, live in Erdos403.Superseded.)

def Erdos403.factDigit (i n : ℕ) : ℕ

The i-th factorial-base digit of n: dᵢ(n) = ⌊n / i!⌋ mod (i+1).

Equations

• Erdos403.factDigit i n = n / i.factorial % (i + 1)

theorem Erdos403.sum_lt_factorial_of_lt (T : Finset ℕ) (hT : ∀ a ∈ T, 1 ≤ a) (i : ℕ) : ∑ a ∈ T with a < i, a.factorial < i.factorial

The factorials below i (positive indices) sum to less than i!.

theorem Erdos403.factDigit_sum_factorial (T : Finset ℕ) (hT : ∀ a ∈ T, 1 ≤ a) {i : ℕ} (hi : 1 ≤ i) : factDigit i (∑ a ∈ T, a.factorial) = if i ∈ T then 1 else 0

The digits of a sum of distinct factorials are its indicators. For T a finite set of positive integers, d_i(∑_{a∈T} a!) = [i ∈ T] ∈ {0,1}. (The "representable ⟹ all digits ≤ 1" direction, with the exact value.)

theorem Erdos403.factDigit_top {n M : ℕ} (h : n < (M + 1).factorial) : factDigit M n = n / M.factorial

Leading digit. If n < (M+1)! then the top digit is just the quotient: d_M(n) = ⌊n / M!⌋ (no mod truncation, since n/M! < M+1).

theorem Erdos403.two_le_factDigit_top {n M : ℕ} (h : n < (M + 1).factorial) (h2 : 2 * M.factorial ≤ n) : 2 ≤ factDigit M n

If n reaches 2·M! (but stays below (M+1)!), its top digit is ≥ 2. The size-sandwich side of the residual: n ∉ [M!, 2M!) ⟹ leading digit ≥ 2 ⟹ not all digits ≤ 1.

theorem Erdos403.factDigit_factSum_le_one (T : Finset ℕ) (hT : ∀ a ∈ T, 1 ≤ a) {i : ℕ} (hi : 1 ≤ i) : factDigit i (∑ a ∈ T, a.factorial) ≤ 1

A sum of distinct factorials (positive indices) has all digits ≤ 1.

theorem Erdos403.factSum_digit_dichotomy (S : Finset ℕ) {n : ℕ} (hn : factSum S = n) : (∀ (i : ℕ), 1 ≤ i → factDigit i n ≤ 1) ∨ ∀ (i : ℕ), 1 ≤ i → factDigit i (n - 1) ≤ 1

The 0! bridge. Since 0! = 1!, allowing index 0 adds at most one unit. So if n is a sum of distinct factorials (n = factSum S, indices ≥ 0), then either n or n - 1 has all factorial digits ≤ 1 (the latter when 0 ∈ S, peeling 0! = 1).

theorem Erdos403.not_factSum_of_digits (n : ℕ) (h1 : ∃ (i : ℕ), 1 ≤ i ∧ 2 ≤ factDigit i n) (h2 : ∃ (i : ℕ), 1 ≤ i ∧ 2 ≤ factDigit i (n - 1)) (S : Finset ℕ) : factSum S ≠ n

Non-representability criterion. If both n and n - 1 carry a factorial digit ≥ 2 (at a positive index), then n is not a sum of distinct factorials: no S has factSum S = n. This is the interface the sharp endgame calls on n = 2^m.