Raudvere's bound

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

Holds for: n ≥ 5
Announced: Jul 18, 2026
Proof: Lean proof
Coefficient of (n−3)!: 0

By Uku Raudvere.

Values

n	At least
5	153
6	868
7	5,886
8	46,093
9	408,289
10	4,032,273
11	43,910,408
12	522,562,987
13	6,746,084,362
14	93,885,792,011

Evidence

Lean proof, kernel-checked github.com/urdvr/superperm-coeff2 Commit 12acadf0069dd4098a6cacec2dff21b6c8096a18 Lean 4 formalization and PDF; Miles Gould confirmed it compiles with only the standard axioms (2026-07-23)

Historical proof checks

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

kernel-checked

LowerBoundFrom 5 (.add (.sub (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.var)) (.const 3)) (.div (.sub (.fact 3) (.const 1)) (.sub (.mul (.const 2) (.var)) (.const 1))))

Original job: historical-20261024-144910-8be0622c-raudvere-headline. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

Linking lemma written by the Almanac.