The 43/80 bound
For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(\tfrac{43}{80} + o(1)\right)(n-3)!
- Holds for
- large n
- Announced
- Sep 29, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 43/80
By Jay Pantone 
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/superperm-upper-43-80
Commit
c8fb7ffdd69be1375580710ae11b47a295b1f0f6Lean proof of the main theorem and of an explicit finite bound for every K >= 11 (computed by tools/finite_bound.py)
Historical proof checks
These checks cover the bound’s mathematical statement. The paper and source notes are for citation.
kernel-checked
This proof establishes the 43/80 asymptotic upper-bound coefficient.
AsymptoticUpper (43/80)Original job: seed-pantone-43-80-20261024-042109. Original policy: 935d78d56a304711c7d70e241c7efeaf20b8abaea1a1fe6d9cbd4e6392a2f732.
Linking lemma written by the Almanac.