The 1771/3456 bound
For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(\tfrac{1771}{3456} + o(1)\right)(n-3)!
- Holds for
- large n
- Announced
- Oct 6, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 1771/3456
By Jakub Halfar. Applies Pantone's 43/80 construction and Lean library with a new selection.
Evidence
- Lean proof github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean constant/: Pantone's argument with a new selection; no native_decide; finite version from n = 13
-
Lean proof, kernel-checked
github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/constant
Commit
cc5c763bd5854317b20dadb138990802656e6f03
Historical proof checks
These checks cover the bound’s mathematical statement. The paper and source notes are for citation.
kernel-checked
AsymptoticUpper (1771/3456)Original job: historical-20261025-143453-f94580fe-halfar-1771. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.
Linking lemma written by the Almanac.