The 101/120 bound
For every n ≥ 8, S(n) \le n! + (n-1)! + (n-2)! + \tfrac{101}{120}(n-3)!
- Holds for
- n ≥ 8
- Announced
- Sep 29, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 101/120
By Jay Pantone 
Values
| n | At most |
|---|---|
| 8 | 46,181 |
| 9 | 408,846 |
| 10 | 4,036,242 |
| 11 | 43,942,416 |
| 12 | 522,852,624 |
| 13 | 6,748,993,440 |
| 14 | 93,917,910,240 |
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/superperm-upper-43-80
Commit
c8fb7ffdd69be1375580710ae11b47a295b1f0f6'earlier uniform bound' proved in the repository's Lean library
Historical proof checks
These checks cover the bound’s mathematical statement. The paper and source notes are for citation.
kernel-checked
UpperBoundFrom 8 (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.div (.mul (.const 101) (.fact 3)) (.const 120)))Original job: historical-20261025-125404-7575882e-pantone-101-120. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.
Linking lemma written by the Almanac.