New upper bound with 1771/3456 and new lower bounds for n = 8 to 14, both in Lean

[Jakub Halfar]

Hi all,

I have two results proved in Lean: an upper bound with 1771/3456 in place of 43/80, and lower bounds for n = 8 to 14. Neither uses native_decide, and the theorems depend on the three standard axioms only.

Upper bound

In Jay's thread I gave 1771/3456 = 0.5124 as a claim to be checked. It is now proved: Jay's bound holds with 1771/3456 in place of 43/80 = 0.5375, and the finite version holds from n = 13 on. The proof is Jay's, applied to the selection with only full and short slices from that post, and the statements use the definitions of his Challenge.lean. For n >= 14 there are no explicit words, so the bound is new there:

    n = 14:      93,907,379,760 ->      93,905,309,790  (-2,069,970)
    n = 15:   1,401,355,309,200 ->   1,401,331,300,446  (-24,008,754)

The numbers on the left are the best values of Jay's finite bound.

Lower bounds

These are built on Xiaolong Liu's library. The first is

    L(n) >= n! + (n-1)! + (n-2)! + n - 3 + ceil( 2((n-2)! - (n-2)) / (n^2 - 4n + 1) )    for n >= 7.

Cole Fritsch proposed this formula here in January 2020. In September Jay announced a Lean proof of a bound that gives the same integers up to n = 14, together with a sharper table. My proof goes through the deficit-one lemma from Marin Kisic's note of August.

The formula rests on an inequality between the number of pieces of a chain and its deficit. For each n from 8 to 14 a finite search shows that a stronger inequality holds, and the Lean kernel runs that search: 827,022 states for n = 8 and fewer than 30,000 for each of the others. The results:

     n    before (Lean)              now      change   Jay (announced)
     8           46,130           46,133          +3            46,130
     9          408,418          408,469         +51           408,468
    10        4,033,080        4,033,378        +298         4,033,374
    11       43,916,235       43,917,903      +1,668        43,917,903
    12      522,610,764      522,622,378     +11,614       522,622,378
    13    6,746,523,219    6,746,626,957    +103,738     6,746,626,519
    14   93,890,256,441   93,891,141,008    +884,567                 -

The column "before" is William Echols's 46,130 for n = 8 and Xiaolong Liu's bounds for the others. The table starts at n = 8 because for n = 7 the formula gives 5,895 and Justin Lebar's 5,898 is higher.

The last column is Jay's table. He announced it before I had any of these bounds. I haven't seen his proofs, so I don't know how much mine have in common with them. I'd be glad to compare once they are out.

Everything is at https://github.com/jhalfar/superpermutations in proofs/lean, and the READMEs there say how each proof goes. The same directory has a command that checks a word in the Lean kernel. My words of 4,034,855, 43,930,578 and 522,737,175 letters are checked that way.

Best,
Jakub