(Another) machine-verified improvement to the lower bound
106 views
Skip to first unread message
Uku Raudvere
Jul 28, 2026, 2:59:05 PMJul 28
to Superpermutators
Hi,
I took the partial draft Zach Hunter worked on and shared with this group in 2019, fixed some issues and filled in the gaps using AI. To be clear - I did not do any mathematics, just directed the search for the proof. The result is a Lean-formalized proof of a lower bound.
S(k) ≥ k! + (k−1)! + (k−2)! + ((k−2)! − (k−2))/(k² − 3k + 1) + k − 3 for every k ≥ 3,
an improvement over the 2018 HPV bound of order (k−4)!, roughly twice the coefficient-two improvement I posted earlier.
Kernel-checked consequences: S(6) ≥ 869, S(7) ≥ 5888, S(8) ≥ 46103.
There is a PDF write-up and the Lean proof at https://github.com/urdvr/superpermutations-hunter
[AI summary]
The proof works in the weighted overlap graph on the k! permutations, where S(k) = k + L(k) for L(k) the minimum Hamiltonian-path weight. A transformation F rewires any Hamiltonian path into a covering by "exitless" paths — paths that never leave a rotation class while its weight-1 edge is still fresh — with the rewiring cost tracked by an exact ledger: one bound counts components and cheapest re-entries, a second converts this to a cost-per-vertex ratio. Everything reduces to i_k(ℓ), the minimum weight of an exitless path on ℓ vertices.
The heart is the inequality i_k(ℓ) ≥ j_k(ℓ) for an explicit comparison function j_k. An exitless path is a chain of full rotation blocks; its weight-2 continuations follow a unique door map of period k−1, and of the six weight-3 continuations after a completed run exactly one sustains another full run (period k−2). A minimum-excess path through (k−1)(k−2) blocks is thereby forced into a single deterministic chart with excess exactly k−3, and from the chart's final exit every successor of weight ≤ 3 — all nine of them — lands in a visited class, so a fresh continuation costs at least 4. A strong induction on excess (opened blocks ≤ (E+1)(k−1) − ⌊E/(k−2)⌋) then gives i_k ≥ j_k at every supported length, partial terminal blocks included. Minimizing j_k(ℓ) − q_k·ℓ, whose ceiling remainders vanish exactly at ℓ = k(k−1)(k−2), yields the coefficient q_k.
(The formalization also proves the relaxation is tight — i_k = j_k on the whole base region, attained by the greedy chart — so further improvement must come from the reduction, not from exitless paths; and that the graph model is exact: L*(k) = S(k).)
[/AI summary]
Zach saw the work, agreed to be listed as a co-author and consented to sharing it.
I believe there is slack left - an integer-capacity argument on top of this bound appears to give roughly an additional (k−5)!-order term, which I'm still verifying.
As somewhat of a meta comment - I don't want to spam the group. I'm (obviously?) not used to communicating mathematics, I don't know what is generally interesting and to what detail. So if I'm overstepping somehow or violating some community rules, please just let me know.
I took the partial draft Zach Hunter worked on and shared with this group in 2019, fixed some issues and filled in the gaps using AI. To be clear - I did not do any mathematics, just directed the search for the proof. The result is a Lean-formalized proof of a lower bound.
S(k) ≥ k! + (k−1)! + (k−2)! + ((k−2)! − (k−2))/(k² − 3k + 1) + k − 3 for every k ≥ 3,
an improvement over the 2018 HPV bound of order (k−4)!, roughly twice the coefficient-two improvement I posted earlier.
Kernel-checked consequences: S(6) ≥ 869, S(7) ≥ 5888, S(8) ≥ 46103.
There is a PDF write-up and the Lean proof at https://github.com/urdvr/superpermutations-hunter
[AI summary]
The proof works in the weighted overlap graph on the k! permutations, where S(k) = k + L(k) for L(k) the minimum Hamiltonian-path weight. A transformation F rewires any Hamiltonian path into a covering by "exitless" paths — paths that never leave a rotation class while its weight-1 edge is still fresh — with the rewiring cost tracked by an exact ledger: one bound counts components and cheapest re-entries, a second converts this to a cost-per-vertex ratio. Everything reduces to i_k(ℓ), the minimum weight of an exitless path on ℓ vertices.
The heart is the inequality i_k(ℓ) ≥ j_k(ℓ) for an explicit comparison function j_k. An exitless path is a chain of full rotation blocks; its weight-2 continuations follow a unique door map of period k−1, and of the six weight-3 continuations after a completed run exactly one sustains another full run (period k−2). A minimum-excess path through (k−1)(k−2) blocks is thereby forced into a single deterministic chart with excess exactly k−3, and from the chart's final exit every successor of weight ≤ 3 — all nine of them — lands in a visited class, so a fresh continuation costs at least 4. A strong induction on excess (opened blocks ≤ (E+1)(k−1) − ⌊E/(k−2)⌋) then gives i_k ≥ j_k at every supported length, partial terminal blocks included. Minimizing j_k(ℓ) − q_k·ℓ, whose ceiling remainders vanish exactly at ℓ = k(k−1)(k−2), yields the coefficient q_k.
(The formalization also proves the relaxation is tight — i_k = j_k on the whole base region, attained by the greedy chart — so further improvement must come from the reduction, not from exitless paths; and that the graph model is exact: L*(k) = S(k).)
[/AI summary]
Zach saw the work, agreed to be listed as a co-author and consented to sharing it.
I believe there is slack left - an integer-capacity argument on top of this bound appears to give roughly an additional (k−5)!-order term, which I'm still verifying.
As somewhat of a meta comment - I don't want to spam the group. I'm (obviously?) not used to communicating mathematics, I don't know what is generally interesting and to what detail. So if I'm overstepping somehow or violating some community rules, please just let me know.
Robin Houston
Jul 28, 2026, 4:05:29 PMJul 28
to Uku Raudvere, Superpermutators
Please do keep it coming! This isn't spam, it's what we're here for.
Cheers,
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/28ed361d-ae99-437a-96cf-890226df6da9n%40googlegroups.com.
William Echols
Jul 28, 2026, 4:11:06 PMJul 28
to Superpermutators
Relating to the meta comment, I was thinking about
this earlier and I wonder if it would be helpful to have a wiki that
complements this Google Group; this could continue to be the place for
discussions, but a wiki could offer a more organized place to host or
link results, constructions, and papers. If there would be interest in
this, I would be happy to build and host it.
I remember there once being a couple websites that tracked results, but I believe they are now offline. My main idea would be to resurrect this but make it community edit-able.
I remember there once being a couple websites that tracked results, but I believe they are now offline. My main idea would be to resurrect this but make it community edit-able.
Jay Pantone
Jul 28, 2026, 4:15:00 PMJul 28
to Robin Houston, Uku Raudvere, Superpermutators
Very nice results on both the upper and lower bounds! In May I managed to also find a new lower bound, but hadn't had time to write it up yet. Your most recent one from today is stronger than mine, so you've saved me the job of writing the paper :) I did try very hard at that time to improve the upper bound, but couldn't, so it's nice to see improvement there as well.
And I agree with Robin, that's what this group is for, otherwise I wouldn't know about this exciting progress.
To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/CAD9Xfq22yGHFBGa-dfcxfk3wmEjQrFE-Fcmd8WotSA6TnVnd%2Bg%40mail.gmail.com.
Miles Gould
Jul 28, 2026, 5:17:15 PMJul 28
to Uku Raudvere, Superpermutators
Oh, great, I was hoping someone would try this!
On Tue, 28 Jul 2026 at 19:59, Uku Raudvere <u.rau...@gmail.com> wrote:
--
Zwish King
Jul 29, 2026, 7:17:28 AMJul 29
to Miles Gould, Uku Raudvere, Superpermutators
Apologies all for never properly polishing my old draft haha. I was just starting undergrad at the time, and by the time I learned how to properly write math papers, I got lost in other work...
I hope some time to look at Uku's other proof and see if there is a way to push the bound further by combining things. But I am currently dealing with applications for post-docs as I finish my last year of grad school. We will see.
ZH
I hope some time to look at Uku's other proof and see if there is a way to push the bound further by combining things. But I am currently dealing with applications for post-docs as I finish my last year of grad school. We will see.
ZH
To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/CAKFNCm1BRiCW2X59mfQd%3D6AOKBaMKXGGDmgjT%2BLHWFiRwoktkg%40mail.gmail.com.
Ranbir Das
Jul 29, 2026, 9:41:17 AMJul 29
to Jay Pantone, Zwish King, Miles Gould, Uku Raudvere, Superpermutators
What happened in May may be summarized
Best of luck with the applications
To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/CAOB4Wv77gn1w-X_oc%2Bu6E78z4W6%2BYEHmaiSn8HJBMLXJJDw4Jw%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages