Halfar's general bound

For every n ≥ 7, S(n) \ge n! + (n-1)! + (n-2)! + n - 3 + \left\lceil \frac{2((n-2)! - (n-2))}{n^2 - 4n + 1} \right\rceil

Holds for: n ≥ 7
Announced: Oct 6, 2026
Proof: Lean proof
Coefficient of (n−3)!: 0

By Jakub Halfar.

Values

n	At least
7	5,895
8	46,129
9	408,465
10	4,033,329
11	43,917,793
12	522,622,030
13	6,746,615,766
14	93,891,107,960

Evidence

Lean proof github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditB.lean Theorem B, on Liu's library; no native_decide; Lean files first pushed 2026-10-06 20:48 UTC
Lean proof, statement reviewed github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower Commit cc5c763bd5854317b20dadb138990802656e6f03

Historical proof checks

These checks cover the bound’s mathematical statement. The paper and source notes are for citation.

statement reviewed

∀ n : ℕ, 7 ≤ n → ∀ w : Almanac.Word n, Almanac.IsSuperpermutation n w → n.factorial + (n-1).factorial + (n-2).factorial + n - 3 + (2*((n-2).factorial-(n-2)) + (n*n-4*n+1) - 1) / (n*n-4*n+1) ≤ w.length

Original job: historical-20261025-143453-f94580fe-halfar-b. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.

Linking lemma written by the Almanac.