There Are No 4 Row High Orphans in Conway's Game of Life

[mscibing]

The proof consists of showing that there exists a set consisting of two columns from the parent generation and six "context" columns from the orphan candidate where any partial solution to an orphan candidate that matches an element of the set in it's last two columns and candidate context can be extended to some longer partial solution that also matches an element of the set in it's last two columns and candidate context.
The empty set trivially matches these conditions, but if a non-empty set can be found it is then possible to do induction on the length of the partial solutions and show that no orphan can exist.

An example of what I mean by extending to a longer partial solution:

Code: Select all

enter target:
 *******************************
 **.*.***.* ***.*.***.*.***.*.**
 *.***.*.***.*.***.*.***.*.***.*
 *******************************
enter partial solution:
..**
.*..
*...
.*.*
*.**
....

Precondition:
 **
(.., ******) is a member of the proof set: VERIFIED.
 ..  .*.***
 .*  ***.*.
 **  ******
 ..

Longer partial solution found:
..***.*
.*.....
*....*.
.*.**..
*.**..*
......*

Postcondition:
 .*
(.., ******) is a member of the proof set: VERIFIED.
 *.  ***.*.
 ..  .*.***
 .*  ******
 .*

The proof set I found has 21,767,045,299 elements. Finding this set is in principle as easy as starting with the set of all combinations and iteratively removing elements that don't fit the criteria until you're only left with the elements that do. But there are a couple of complications: In trying to prove an element belongs in the set you have the possibility of infinite loops, or even just taking an excessive amount of time. Therefore there needs to be some limit on how hard the program tries to prove an element belongs before giving up. I tried a number of possibilities here, and a simple distance-based cut off (at most 17 columns before finding a further element of the set) seemed to work as well as anything else. The other complication is that the self-referential nature of the proof set means that whenever an element is removed from the set the remaining elements will need to be re-checked for membership at some point. I think the number of passes through the set before convergence ended up being somewhere in the teens. The program does claw back a factor of two on the work required by taking advantage of symmetry, but it did end up taking about two months to run.

I've uploaded the program here:
https://codeberg.org/ajwade/orphan_disprover

The proof was completed with an earlier version of the program. I'm currently re-checking the proof with the latest version which should complete in the next day.

The artefact produced by the program is an 8GB file specifying the proof set so verification is difficult. I have added an --extend-solution option and have done some very limited spot-checks.

[squareroot12621]

Wow, there goes one of dvgrn's conjectures from 5½ years ago!

Conjecture: There exists a Garden of Eden inside a 4xN bounding box.
(It is known that no Garden of Eden patterns exist that are 1, 2, or 3 cells high, and Steven Eker found some 5-cell-high Gardens of Eden in 2016, but it is currently an open question whether a 4-cell-high GoE can be constructed.)

[mscibing]

I should probably call out a distinction between live cells and specified cells. I haven't quite disproved Gardens of Eden where the live cells are restricted to four (consecutive) rows. But when the specified cells in the target generation, both alive and dead, are restricted to four consecutive rows, there will always be a parent pattern.

[mscibing]

I am working on extending the proof to Gardens of Eden, i.e. cells outside the four rows in the target are specified as dead.

If I take a typical parent pattern that produces a given four row high sub-pattern it will often have a few stray live cells produced outside the four target rows. But if I then take that parent pattern and run it between "rails" the stray cells are mostly suppressed:

Code: Select all

x = 124, y = 53, rule = B3/S23
2$32b2o30bo2$30bo4bo30bo$34bo39bo3b2ob2o2b3o2bo3bo3bo$59bo2bo2bo2bo5b
2ob2obobobobob3ob4ob2o$33bo40b2ob2o3bo2b2obobo2b3ob2o$33bo32bo7b2ob2ob
obobob2o2bo3b2ob2o2$64bo$33bo11$64bo$95bo4b3o$5b2obo3b2o7b2ob3o2b5ob2o
bo27bo8b3obo11b5o2bo2b3o2b2o$5b2o2b2o5b2o3bo2bo3b3o3b3o3bo3bo3bo3bo21b
o3b2ob2o2b3o2bo3bo3bo$5bo2bo3bobobobobobo10bo3bo3bo3bo3bo3bo5bo2bo2bo
2bo5b2ob2obobobobob3ob4ob2o24bo$5bobo2bob2obo2bo2bobob2obob24o20b2ob2o
3bo2b2obobo2b3ob2o24bo$5bo2bobo3bo2bo2bobobo3b4o2b2o2b2o2b2o2b2o2b2o
14bo7b2ob2obobobob2o2bo3b2ob2o$5bo2bo2bo2bobo4b2o56bo5bo5b3o5b2o$64bo
11$71b52o$54o10bo5bo52bo$54o16bo52bo$5b2obo3b2o7b2ob3o2b5ob2obo27bo4b
3o15bo18bo3bo3bo3bo2bo$5b2o2b2o5b2o3bo2bo3b3o3b3o3bo3bo3bo3bo21bo3b2ob
2o2b3o2bo3bo3bo$5bo2bo3bobobobobobo10bo3bo3bo3bo3bo3bo5bo2bo2bo2bo5b2o
b2obobobobob3ob4ob2o24bo$5bobo2bob2obo2bo2bobob2obob24o20b2ob2o3bo2b2o
bobo2b3ob2o24bo$5bo2bobo3bo2bo2bobobo3b4o2b2o2b2o2b2o2b2o2b2o14bo7b2ob
2obobobob2o2bo3b2ob2o$5bo2bo2bo2bobo4b2o48b3o22bo$54o10bo5bo52bo$54o
16bo52bo$71b52o!

By itself this isn't enough, but what I can do is modify the definition for the proof set so that the stray cells in the target generation are always suppressed when run between rails. The cells produced where the rails stop can be dealt with by just running the rails out to infinity:

Code: Select all

x = 49, y = 43, rule = B3/S23
24bo2$24bo2$24bo3$8bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2$7b35o$7b35o$8b
2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o4$8bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2bo
2bo2$7b35o$7b35o$8b2o2bob2ob2o10b2obobobo3b2o$13b2obo2bobob2obo2b2o2b
2o2bo$obobo8bo5bo4bo2bo2bo2bobo8bobobo$13bobobo4bobobobobo2bo2bo$8bo2b
o2b2o2b3o4bo2bo3bo2bo3bo$13bo5b2ob2o4bo2b2o3bo$7b35o$7b35o$8b2o2b2o2b
2o2b2o2b2o2b2o2b2o2b2o2b2o4$8bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2bo2$7b
35o$7b35o$8b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o3$24bo2$24bo2$24bo!

A schematic of what's going on:

Code: Select all

                          .
                          .
                          .

    **********************************************
    **********************************************


        (solution producing empty target here)



    **********************************************
    **********************************************


...     (solution producing desired target here)   ...



    **********************************************
    **********************************************


        (solution producing empty target here)



    **********************************************
    **********************************************

                          .
                          .
                          .

For B3/S23 it's not too hard to find a finite stabilization for the rails for a finite target population, and I expect this will be possible to prove. But this extra step isn't necessary to disprove Gardens of Eden:

Code: Select all

x = 46, y = 14, rule = B3/S23
o44bo$bo2b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o2b2o2bo$46o$46o$bo2b2o2bob
2ob2o10b2obobobo3b2o2b2o2bo$o8b2obo2bobob2obo2b2o2b2o2bo11bo$9bo5bo4bo
2bo2bo2bobo$9bobobo4bobobobobo2bo2bo$o3bo2bo2b2o2b3o4bo2bo3bo2bo3bo2bo
2bo3bo$bo7bo5b2ob2o4bo2b2o3bo11bo$46o$46o$bo2b2o2b2o2b2o2b2o2b2o2b2o2b
2o2b2o2b2o2b2o2bo$o44bo!

My hope is that the extra requirement on the proof set is mild enough that a proof set can be found without an excessive amount of computation. It's not looking good at the moment, but I'm not throwing in the towel yet.

[mscibing]

It looks like I'm finally getting close to disproving 4 row high gardens of eden, but I had to move the "rails" further apart. With the rails separated by 8 rows it looks like I will converge to a proof set sometime in the next couple of weeks.