The Life-like rule B37/S2378: an exhaustive census of 4×4 seeds, disk-shaped growth, and two oscillators with machine-checked periods

The outer-totalistic rule B37/S2378 (a dead cell is born with 3 or 7 live neighbours; a live cell survives with 2, 3, 7 or 8) is a close relative of DryLife (B37/S23). We report the first census of it that we could find. Every one of the 65,535 non-empty seeds of the 4×4 box was evolved until it recurred up to translation; the same protocol was run for Conway's B3/S23 as a control. The B37/S2378 census yields 96 objects, including an oscillator of period 10 (11 cells) and one of period 32 (13 cells), neither of which exists under B3/S23. Seeds that do not settle behave very differently in the two rules: under B37/S2378, 338 of 471 sampled unsettled seeds are still growing after 1,000 generations, as a disk whose interior holds the density of random soup (0.111–0.130) and whose edge advances at 0.056–0.065 c; under B3/S23 none of the 465 sampled unsettled seeds keeps growing (the 6 still growing at 1,500 generations all settle by 20,000). The periods of both oscillators, the minimality of the period 10, and the failure of the period-10 pattern under Conway's rule are proved in Lean 4 by kernel computation, with no axioms beyond the standard ones. Files: b37s2378-census-note.pdf (the note) and b37s2378-note-source.zip (LaTeX source, the JSON data, the Python scripts that produced it, the script that generates every number, table and figure of the note, the RLE files and the Lean 4 development). The note is released under CC BY 4.0; the code and the Lean development under the Apache License 2.0.