s(7) >= 5,899, proved in Lean

[Jakub Halfar]

Hi all,

Every superpermutation on 7 symbols has at least 5,899 letters, and the proof is in Lean. Justin Lebar's bound was 5,898. The shortest known word has 5,905.

The proof has two parts. The first is an exact description of superpermutations for every n >= 5, proved in Lean from the Hunter-Raudvere transformation and Xiaolong Liu's chains. A word of length n! + (n-1)! + (n-2)! + n - 3 + D exists if and only if a configuration of defect D exists. A configuration is one sequence of rows with further pieces attached to it, where a row is a run of consecutive 1-cycles inside one 2-cycle and the rows use every 1-cycle exactly once. This part depends on the three standard axioms only.

The second part shows that for n = 7 there is no configuration of defect 14. Each piece is bounded by a table: how many rows a chain, a linked sequence of chains or a ring can have for a given number of missing 1-cycles. Adding the bounds up leaves no room. The tables come from searches of 1.1 * 10^11 nodes in all. The search and the proof that it misses nothing are in Lean and checked by the kernel. The 22 runs themselves are evaluated with native_decide, so for those the compiler is trusted. Justin's proof of 5,898 stands on the same footing.

The files and a README are at https://github.com/jhalfar/superpermutations in proofs/lean/n7.

My current words for n = 12 and n = 13 are in the same repository:

    n = 12:    522,745,531 ->    522,737,175  (-8,356, previous: Theo H.)
    n = 13:  6,747,918,066 ->  6,747,802,393  (-115,673, previous: Jay Pantone)

Best,
Jakub