Jakub Halfar's 0*(n-3)! asymptotic upper bound

For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(0 + \varepsilon\right)(n-3)!

Evidence

Lean proof, kernel-checked github.com/jhalfar/superpermutation-almanac-lean at commit af99e8317297566e7bd33fb69bc10c44c484fdc3 Checked on Nov 8, 2026.

build 251 s, peak 3.8 GB

Result 1 of batch L-0016, theorem upper_coeff3_zero, checked in attempt 1: AlmanacSolution.lean, line 11.

theorem upper_coeff3_zero : Almanac.AsymptoticUpperAt 3 0

Pantone's 43/80 construction with nested block levels added, built on his Lean library. First in proofs/lean/constant43586371 of my main repository.