Egan's bound minus one

For every n ≥ 8, S(n) \le n! + (n-1)! + (n-2)! + (n-3)! + n - 4

Holds for: n ≥ 8
Announced: Jul 28, 2026
Proof: Lean proof
Coefficient of (n−3)!: 1

By Uku Raudvere.

Values

n	At most
8	46,204
9	408,965
10	4,037,046
11	43,948,807
12	522,910,088
13	6,749,568,009
14	93,924,230,410

Evidence

Lean proof, kernel-checked github.com/urdvr/superpermutation-examples/tree/62958c6268f728828ed578a171486866b6fe4b20/formal Commit 62958c6268f728828ed578a171486866b6fe4b20 Lean: for all n >= 8 a superpermutation of length E(n) - 1 exists, by a certificate lift from the 46204 word; no sorry or native_decide

Historical proof checks

These checks cover the bound’s mathematical statement. The paper and source notes are for citation.

kernel-checked

UpperBoundFrom 8 (.sub (.add (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.fact 3)) (.var)) (.const 4))

Original job: historical-20261025-164127-23effe32-raudvere-upper. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.

Linking lemma written by the Almanac.