Lean-verified lower bound S(7) ≥ 5889

[にか]

Hi all,

I've obtained a Lean-verified lower bound

S(7) ≥ 5889

for the shortest superpermutation on 7 symbols.

The development builds on the Hunter–Raudvere formalization, whose certified n=7 lower bound is 5888. The additional step is specific to n=7: I analyze the equality case at 5888 and rule it out.

Very roughly, the proof:

• reduces equality to a small set of terminal component configurations;

• classifies the remaining cases into two finite exact-partition problems;

• rules those out using integer Farkas certificates;

• formally connects the finite certificates back to actual Hunter Xk 7 objects.

The final Lean theorem is:

Ssuper7_ge_5889 : 5889 ≤ Hunter.Ssuper 7

Repository:
https://github.com/nika0220/superperm5889

v1.0 release:
https://github.com/nika0220/superperm5889/releases/tag/v1.0

The repository builds successfully and contains an explicit axiom audit. There are no sorry, admit, or user-defined axioms; the finite certificate checks use the documented native_decide trust path.

As far as I have been able to determine, this improves the previous publicly available machine-verified n=7 lower bound of 5888. But I would especially appreciate confirmation from people here:

Is S(7) ≥ 5889 already known from any earlier unpublished or public work?

I'd also be very grateful for any comments on the proof or formalization.

Best,
nika0220

[Robin Houston]

I haven't looked at this, so no comment on its correctness. But on the novelty question, I'm almost sure this is new (unless I've missed some very recent development).

Robin

--
You received this message because you are subscribed to the Google Groups "Superpermutators" group.
To unsubscribe from this group and stop receiving emails from it, send an email to superpermutato...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/5c3e2293-56a6-4f59-98cd-9167b3384daen%40googlegroups.com.