Pantone's bound
For every n ≥ 8, S(n) \ge n! + (n-1)! + (n-2)! + n - 3 + \left\lceil \frac{2(n-2)! - 2(n-2) - 4p_n/t_n}{n^2 - 4n + 1 - 2(n-1)/t_n} \right\rceil
For n = 8 to 12, (pₙ, tₙ) = (10, 46/3), (15, 287/12), (521/80, 359/40), (21, 263/12), (28, 195/4). For n ≥ 13, write n − 1 = 3m + r. If r = 0, (pₙ, tₙ) = (2m + 1/2 + 1/(4R₀), 4m − 3 − 1/(2R₀)); if r = 1, (m(2m + 1), 2m² + 2m − 2 − 1/R₁); if r = 2, ((m + 1)(2m + 1), 4m² + 5m − 5/2). R₀ = 2(n − 1)/7 if 7 divides n − 1, else u(n − 1 − u) with 7u ≡ 1 mod n − 1. R₁ is an LCM of cycle lengths set by m mod 6 (see the paper).
- Holds for
- n ≥ 8
- Announced
- Oct 29, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 0
By Jay Pantone 
Values
| n | At least |
|---|---|
| 8 | 46,130 |
| 9 | 408,469 |
| 10 | 4,033,374 |
| 11 | 43,917,903 |
| 12 | 522,622,380 |
| 13 | 6,746,626,531 |
| 14 | 93,891,141,149 |
Evidence
-
Lean proof, statement reviewed
github.com/jaypantone/2026-10-superpermutation-lower-palomar at commit
ad72ab5010e945b5c8768a918281778c834dcc40Paper: finite/finite-lower-bounds.pdf (+18 files) Checked on Oct 29, 2026.
Proof checks
statement reviewed
- Checked
- Oct 29, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean
v4.35.0- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 993 s, peak 7.5 GB
Statement reviewed, not matched to a fixed statement. Checked statement and definitions.
Result 1 of batch L-0015, theorem general_lower, checked in attempt 1: AlmanacSolution.lean, line 10.
Repository at the checked commit · Repository archive (17.6 MB)
The judge checks each proof with two kernels. A fixed statement is also compared with the Almanac’s definitions; a custom statement is reviewed by hand.