Erdős #403 — the sharp bound m ≤ 7 (Phases B–D)

Using the factorial number system (FactBase), factSum S = 2^m is impossible once 2^m and 2^m − 1 both carry a factorial digit ≥ 2 (not_factSum_of_digits).

• Phase B (done): m even ≥ 4 is killed cleanly — 2^m ≡ 16 (mod 24) forces the 3!-digit of both 2^m and 2^m − 1 to be 2 (and 3! = 6 has no factorial degeneracy, so the 0! carry cannot fix it).
• Phase C (done): m ≥ 8 is killed by a fixed modulus 12! — every such 2^m (and 2^m − 1) carries a factorial digit ≥ 2 at some index ≤ 11, a finite check over the period-1620 cycle of 2^m mod 12!, discharged by a kernel-pure decide.
• Phase D (done): erdos_403_sharp and erdos_403_finite are assembled below (decide the small m). Both are sorry-free and depend only on [propext, Classical.choice, Quot.sound].

theorem Erdos403.two_pow_mod_24_even (t : ℕ) : 2 ^ (2 * t + 4) % 24 = 16

2^(2t+4) ≡ 16 (mod 24) — the period-2 cycle …,16,8,16,8,… of 2^m mod 24 (m ≥ 3), on the even branch.

theorem Erdos403.two_pow_mod_24_of_even {m : ℕ} (he : Even m) (hm : 4 ≤ m) : 2 ^ m % 24 = 16

2^m ≡ 16 (mod 24) for even m ≥ 4.

theorem Erdos403.factDigit_three_two_pow_even {m : ℕ} (he : Even m) (hm : 4 ≤ m) : factDigit 3 (2 ^ m) = 2

For even m ≥ 4, the 3!-digit of 2^m is 2.

theorem Erdos403.factDigit_three_two_pow_sub_one_even {m : ℕ} (he : Even m) (hm : 4 ≤ m) : factDigit 3 (2 ^ m - 1) = 2

For even m ≥ 4, the 3!-digit of 2^m − 1 is also 2 (so the 0! carry can't rescue it).

theorem Erdos403.factSum_ne_of_even {m : ℕ} (he : Even m) (hm : 4 ≤ m) (S : Finset ℕ) : factSum S ≠ 2 ^ m

Phase B result. No sum of distinct factorials equals 2^m for even m ≥ 4.

theorem Erdos403.factSum_ne_of_leading_two {m M : ℕ} (hM : 2 ^ m < (M + 1).factorial) (h2 : 2 * M.factorial < 2 ^ m) (S : Finset ℕ) : factSum S ≠ 2 ^ m

Phase C-7a (leading-digit kill). If 2·M! < 2^m < (M+1)! — i.e. 2^m reaches twice its leading factorial M! without spilling into the next — then the top factorial digit of both 2^m and 2^m − 1 is ≥ 2 (2^m − 1 shares the same leading index and still clears 2·M!, strictly, since 2^m is a power of two). So not_factSum_of_digits fires. This bankable sub-case kills every odd m ≥ 9 whose 2^m lands in the upper half [2·M!, (M+1)!); the residual nut is the lower half [M!, 2·M!).

Phase C — odd m ≥ 9 killed by a FIXED modulus (12!)

Direct computation (verified three ways) shows the factorial-base expansion of 2^m and of 2^m - 1 carries a digit ≥ 2 at some index ≤ 11 for every m ≥ 8. Equivalently, a single fixed modulus 12! closes Erdős #403. The earlier belief that "no fixed modulus works" was a heuristic extrapolation — the smallest offending index climbs 5 → 7 → 8 → 11 and was assumed to grow without bound; in fact it caps at 11.

Mechanism: factDigit i n depends only on n mod (i+1)!, hence for i ≤ 11 only on n mod 12!; and 2^m mod 12! is periodic in m with period 1620 (ord_{467775}(2) = 1620, where 12! = 1024 · 467775). So the claim reduces to a finite check over one period, discharged by a kernel-pure decide over a residue fold (no native_decide).

theorem Erdos403.factDigit_mod (i n : ℕ) : factDigit i n = factDigit i (n % (i + 1).factorial)

factDigit i n depends only on n modulo (i+1)!.

theorem Erdos403.factDigit_mod_twelve {i : ℕ} (hi : i ≤ 11) (n : ℕ) : factDigit i n = factDigit i (n % Nat.factorial 12)

For i ≤ 11, factDigit i n depends only on n modulo 12!.

theorem Erdos403.two_pow_offending {m : ℕ} (hm : 8 ≤ m) : ∃ (i : ℕ), 1 ≤ i ∧ 2 ≤ factDigit i (2 ^ m)

Fixed-modulus kill (heart of Phase C). For every m ≥ 8, 2^m carries a factorial-base digit ≥ 2 at some positive index — so 2^m is not a sum of distinct factorials.

theorem Erdos403.two_pow_sub_one_offending {m : ℕ} (hm : 8 ≤ m) : ∃ (i : ℕ), 1 ≤ i ∧ 2 ≤ factDigit i (2 ^ m - 1)

The 2^m - 1 companion of two_pow_offending.

theorem Erdos403.factSum_ne_of_ge_eight {m : ℕ} (hm : 8 ≤ m) (S : Finset ℕ) : factSum S ≠ 2 ^ m

Phase C complete. No sum of distinct factorials equals 2^m for m ≥ 8.

The headline theorems (FNS route, fully sorry-free)

The fixed-modulus kill makes the entire 2-adic carry machinery (cascade_*, tied_*) unnecessary: factSum_ne_of_ge_eight gives m ≤ 7 directly, and finiteness follows from the size sandwich M! ≤ 2^m ≤ 2^7.

theorem Erdos403.erdos_403_sharp {S : Finset ℕ} {m : ℕ} (h : factSum S = 2 ^ m) : m ≤ 7

Erdős #403 (sharp form) — the largest power of two that is a sum of distinct factorials is 2⁷ = 2! + 3! + 5! = 128. Every solution has m ≤ 7.

theorem Erdos403.erdos_403_finite : {S : Finset ℕ | ∃ (m : ℕ), factSum S = 2 ^ m}.Finite

Erdős #403 (finiteness) — exactly what the problem asks: only finitely many sums of distinct factorials are powers of two. By erdos_403_sharp, every solution has m ≤ 7, so M! ≤ 2^m ≤ 128 forces max' S ≤ 5; hence every solution lives in (range 6).powerset.