Liu's bound

For every n ≥ 5, S(n) \ge H_n + \Gamma_n

Hₙ is the Hunter–Raudvere bound. Γₙ is the least layer passing Liu's test, found for each n; his paper shows Γₙ = (1 − 3/n + O(1/n²))(n − 4)!.

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

By Xiaolong Liu.

Values

n	At least
5	153
6	869
7	5,892
8	46,118
9	408,418
10	4,033,080
11	43,916,235
12	522,610,764
13	6,746,523,219
14	93,890,256,441

Evidence

Lean proof, statement reviewed github.com/Haruhiyuki/superpermutations-preimage-chain-lower-bounds Commit a3852f0de2d84b99cc65d4c281e86892b5f6e911 Lean 4.31.0 on the Hunter-Raudvere library; release commit a3852f0, published 2026-08-10 (repository created 10:10 UTC); theorem superperm_new_bound_closed

Historical proof checks

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

statement reviewed

∀ (n : ℕ) (hn : 5 ≤ n), ∀ w : Almanac.Word n, Almanac.IsSuperpermutation n w → PreimageChain.Numerics.hunterBound n + PreimageChain.Numerics.gamma n hn ≤ w.length

Original job: historical-20261024-145632-264cc426-liu-general. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 10 4033080

Original job: historical-20261024-160642-943b58ba-liu-n10. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 11 43916235

Original job: historical-20261024-160642-943b58ba-liu-n11. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 12 522610764

Original job: historical-20261024-160642-943b58ba-liu-n12. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 13 6746523219

Original job: historical-20261024-160642-943b58ba-liu-n13. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 14 93890256441

Original job: historical-20261024-160642-943b58ba-liu-n14. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 5 153

Original job: historical-20261024-145632-264cc426-liu-n5. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 6 869

Original job: historical-20261024-160642-943b58ba-liu-n6. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 7 5892

Original job: historical-20261024-160642-943b58ba-liu-n7. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 8 46118

Original job: historical-20261024-160642-943b58ba-liu-n8. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

LowerBoundAt 9 408418

Original job: historical-20261024-160642-943b58ba-liu-n9. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

Linking lemma written by the Almanac.