Formal proof (in Coq) of the lower bound

[Robin Houston]

Somebody on Twitter has drawn my attention to a GitHub repository – 

https://github.com/ccd0/superpermutations – which claims to contain a formalised proof of the lower bound that was proved on 4chan’s /sci/ board in 2011.

Are any of you au fait with Coq?

Intriguingly the author of this formal proof appears to be the same person who posted the original proof anonymously. See 

https://warosu.org/sci/thread/S7251421#p7253760

Robin

[Nathaniel Johnston]

Very cool! I think that you've cracked the problem of finding the author. They're still active on github and have a publicly-facing e-mail address attached. Have you contacted them yet?

- Nathaniel

[Robin Houston]

I have. No answer yet. It’s possible they don’t want to be identified and have their real-life identity irrevocably linked to 4chan, and I think we should be a bit sensitive about that possibility – while giving them the opportunity to come forward if they choose.

What about the formal proof, though? I remember finding this repository once before in a Google search, without knowing it had any link to the mystery proof, and failing to persuade Coq to do anything with it other than issue baffling error messages. But I know almost nothing about Coq, so perhaps that is to be expected.

R

--
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 post to this group, send email to superper...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Roberto Colombari]

Hi Robin,

I'm taking advantage of this post to link here my approach, you probably hadn't the chance to have a look at it in the other thread.

http://www.njohnston.ca/2013/04/the-minimal-superpermutation-problem/   <-- you can see my comment just scrolling down a little bit

What I basically do is to maximize the overlaps.

What I found is that, given an arbitrary n, I can find (n-1) permutations with an overlap equal to (n-1). Lets call Block1 these (n-1) permutations.

Block 2 has its first permutation that has an overlap of (n-2) digits with the last permutation of block 1 and the overlaps between its permutations equal to (n-1).

I can put in a row (n-1) blocks that have overlaps equal to (n-2) between them. Then I have to lower down to an overlap equal to (n-3) and start again.

This leads to the formula I wrote in the other thread -> lower bound = n^2(n-2)! + n - 3 that actually is the same as n! + (n-1)! + (n-2)! + n-3 => (n-2)!(n*(n-1) + n - 1 + 1) + n - 3

Bests.

Roberto

Em segunda-feira, 29 de outubro de 2018 07:45:16 UTC-3, Robin Houston escreveu:

I have. No answer yet. It’s possible they don’t want to be identified and have their real-life identity irrevocably linked to 4chan, and I think we should be a bit sensitive about that possibility – while giving them the opportunity to come forward if they choose.

What about the formal proof, though? I remember finding this repository once before in a Google search, without knowing it had any link to the mystery proof, and failing to persuade Coq to do anything with it other than issue baffling error messages. But I know almost nothing about Coq, so perhaps that is to be expected.

R

On Mon, 29 Oct 2018 at 10:25, Nathaniel Johnston <nathaniel...@gmail.com> wrote:

Very cool! I think that you've cracked the problem of finding the author. They're still active on github and have a publicly-facing e-mail address attached. Have you contacted them yet?

- Nathaniel

On Monday, October 29, 2018 at 7:11:54 AM UTC-3, Robin Houston wrote:

Somebody on Twitter has drawn my attention to a GitHub repository – 

https://github.com/ccd0/superpermutations – which claims to contain a formalised proof of the lower bound that was proved on 4chan’s /sci/ board in 2011.

Are any of you au fait with Coq?

Intriguingly the author of this formal proof appears to be the same person who posted the original proof anonymously. See 

https://warosu.org/sci/thread/S7251421#p7253760

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 superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

[Robin Houston]

Hi Roberto,

Yes, I saw that. Thanks. I agree with Greg Egan that it sounds as though you’ve rediscovered the recursive construction method. I don’t understand how it leads to the lower bound you claim.

Cheers,

Robin

To unsubscribe from this group and stop receiving emails from it, send an email to superpermutato...@googlegroups.com.
To post to this group, send email to superper...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

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 post to this group, send email to superper...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/dcbcb300-06eb-4792-b0a0-0eb1b287b447%40googlegroups.com.

[Tahg]

I also found I needed to go down to overlaps of n-3 (but seemingly that was enough for all n), but when I worked through the math on that, it gave me an extra term (n-3)!, as well as a final term of -4, not -3.

To unsubscribe from this group and stop receiving emails from it, send an email to superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

[Roberto Colombari]

Building the superpermutation in the way I described, you'll have:

(n - 2)! - 1 super blocks with overall length:

((n - 2)! - 1)[(n + 2) + (n - 2)(n + 1)]

plus the first block with length:

2n - 1 + (n - 2)(n + 1) = n^2 + n - 2n - 2 + 2n - 1 = n^2 + n - 3

Lower bound = ((n-2)! - 1)(n + 2 + n^2 + n - 2n - 2) + n^2 + n - 3 = n^2(n - 2)! - n^2 +  n^2 + n - 3  = n^2(n - 2)! + n - 3

_______________________

n = 5

Bests

[Tahg]

I can't find any issues with that work for n = 5. Could you perhaps take a look at my (de)construction of n = 6 and see what might be wrong? It looks like our methods diverge at my Iteration 3. See here: https://github.com/superpermutators/superperm/blob/master/notes/construction.txt

[Jay Pantone]

Tahg, and Roberto,

It seems to me that you're not really finding lower bounds. For example, Tahg, you start out by cyclicly rotating the first permutation until you get stuck, giving you a word of length 2n-1. How do you know that *every* superpermutation *must* start like this? Simply saying that that approach is locally the best ("greedy") doesn't imply that it could be better to start by being wasteful because it saves you letters down the road.

Now, if your approach led to you being able to actually construct a word of length n! + (n-1)! + (n-2)!+ (n-3)! + (n-4), then you'd have a new upper bound!

- Jay

To unsubscribe from this group and stop receiving emails from it, send an email to superpermutato...@googlegroups.com.
To post to this group, send email to superper...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to superper...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/dcbcb300-06eb-4792-b0a0-0eb1b287b447%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

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 post to this group, send email to superper...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/c6b4ba28-7e64-4cba-8c92-785d16a7df30%40googlegroups.com.

[Tahg]

I don't say that.  I don't generate the sequence from the first character to the last.  The first steps generate an outer shell in which the rest of the sequences are inserted.  In any case, I think my work shows that for n = 6 you cannot continue at (n - 3) through all the permutations.  I've taken the only possible choice at every step, and still ended up with a cycle containing only n(n-1)(n-2) permutations.  This disagrees with Roberto's implication that you can proceed at (n-3) through the entire list of permutations.

To unsubscribe from this group and stop receiving emails from it, send an email to superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/dcbcb300-06eb-4792-b0a0-0eb1b287b447%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 superpermutators+unsubscribe@googlegroups.com.
To post to this group, send email to superpermutators@googlegroups.com.

[Roberto Colombari]

Hi Tahg,

I made some further checks and my approach can't be valid on n > 5.

Testing with n = 5, I thought that it was enough to go down to an overlap equal to n - 3.

But with n = 6, you have go down up to n - 4 (look at the red squadre below, I can't anymore use 123. I've already place all the 123* permutations):

Cheers

To unsubscribe from this group and stop receiving emails from it, send an email to superpermutato...@googlegroups.com.
To post to this group, send email to superper...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/7ea2671d-e822-4bb9-8c63-a1af74187d3b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to superper...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/dcbcb300-06eb-4792-b0a0-0eb1b287b447%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

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 post to this group, send email to superper...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/superpermutators/c6b4ba28-7e64-4cba-8c92-785d16a7df30%40googlegroups.com.