Pantone's explicit error bound

For large n, S(n) \le n! + (n-1)! + (n-2)! + 2(n-4)! + 400\,(n-4)!\,n^{-1/61}

For every n ≥ 8·10¹²·352⁴·6⁶¹, about 3.6·10⁷⁰. The same theorem proves the matching lower bound, S(n) ≥ n! + (n−1)! + (n−2)! + 2(n−4)! − 400(n−4)!·n^(−1/61).

Holds for: large n
Announced: Nov 9, 2026
Proof: Lean proof
Coefficient of (n−4)!: 2
Points: 0.0

By Jay Pantone.

Evidence

Lean proof, statement reviewed github.com/jaypantone/2026-10-superpermutation-asymptotics at commit 882721e53a9e4927dba06921a5efb8e817563464 Paper: manuscript.pdf · assembly.tex · geometry.tex · global.tex (+3 files) Checked on Nov 10, 2026.

Proof check

statement reviewed

Checked: Nov 9, 2026
Lean version: leanprover/lean4:v4.35.0
Mathlib commit: 56a005855ea17e0b0958f73ec801ae140b0a1679
lean4checker: lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
nanoda: lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc

build 623 s, peak 5.0 GB

Statement reviewed, not matched to a fixed statement.

Result 2 of batch L-0021, theorem explicit_error, checked in attempt 1: AlmanacSolution.lean, line 16.

theorem explicit_error : AlmanacAdapter.ExplicitError

Checked statement and definitions (JSON, 1.3 MB)

Repository at the checked commit · Repository archive (2.2 MB)