PaperlayerView exact revision on arXiv

Source-linked AI summary

The Ultimate Fate of Life Is Not Shared

Ziyue Gan, Ziran Li, Jiadong Zhu

arXiv:2609.34122v1cs.FLmath.COmath.DS

TL;DR

The paper addresses whether spatial translations on the Game of Life limit set are topologically transitive. It uses a persistent marker to pump periodic lanes in backward histories. The result is a fixed pair of patterns that cannot coexist in any limit-set configuration, at any relative position.

  • Problem

    Salo and Törmä asked whether spatial translations on the Game of Life limit set are transitive, meaning that occurring finite patterns can be jointly realized after some relative shift.

    Source: §1 · p. 1

  • Method

    A persistent marker with pump states forces a periodic lane to grow in backward histories, and a rotated copy forces a perpendicular lane whose crossing yields incompatible cell values.

    Source: §1 · p. 2, §3.1 · p. 6

  • Results

    The spatial action on the Game of Life limit set is not topologically transitive: fixed patterns U and its quarter-turn each occur, but cannot coexist at any relative position.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The obstruction uses one fixed pair of patterns for every displacement, rather than a new witness at each scale.

    Source: §1 · p. 2

    The explicit marker is large, and the smallest possible separating pair is unknown.

    Source: §4 · p. 11

Abstract

from arXiv · show

The limit set of Conway's Game of Life collects the configurations that can still appear at arbitrarily late times: those admitting predecessors of every finite depth. Answering a question of Salo and T\"orm\"a (ICALP 2022), we prove that two fixed finite patterns can each occur in the limit set, yet can never be found together in a single configuration of it, at any relative position; equivalently, the spatial translation action on the limit set is not topologically transitive. Our method is to make a persistent marker force a periodic lane to grow in sufficiently deep predecessors, until two perpendicular lanes are forced to intersect and prescribe incompatible values at a common cell. The argument uses two computer-verified local implications.

1 Introduction

The paper answers whether spatial translations on the Game of Life limit set are topologically transitive: they are not. It constructs two fixed patterns that each occur in the limit set but cannot coexist there at any relative position, using a persistent marker to force growing lanes whose crossings prescribe incompatible values.

1 Introduction

  • The spatial action on the Game of Life limit set is not topologically transitive.A fixed finite pattern U and its quarter-turn V each occur, but no configuration in the limit set contains both at any relative position.Source: §1 · p. 2
  • The fixed separating pair changes the obstruction from one witness at each scale to the same pair for every relative displacement.Earlier results established non-soficity and distance-dependent obstructions, but did not provide two fixed cylinder sets with disjoint shift orbits [4, Theorem 3; 4, Theorem 7].Source: §1 · p. 2
  • A persistent marker with two width-preserving pump states lets the same fixed seeds extend a periodic lane to arbitrary length.The marker is restored throughout backward history, avoiding the increasingly wide initial patch required by the earlier construction [4, Lemma 22].Source: §1 · p. 2
  • The proof restores marker U in every h-predecessor, pumps vertical and rotated horizontal lanes, then derives a contradiction at their intersection.Here h = G2; the two lanes prescribe incompatible values at a common cell.Source: §1 · p. 2, Figure 1 · p. 3
  • Two local implications for marker forcing and lane pumping are checked by finite-state and SAT methods; the arbitrary-depth conclusion is proved mathematically.Persistence also uses the published Kynnös self-forcing lemma [4, Lemma 21].Source: §1 · p. 2

2 Preliminaries

The preliminaries set notation for configurations, patterns, shifts, cellular automata, and their limit sets. They state criteria for pattern occurrence and spatial transitivity, and record lattice symmetries used for the Life construction.

2 Preliminaries

  • A configuration over a finite alphabet A is an element of Y = A^Z^d, and a pattern is a map on a domain in Z^d; a finite pattern has finite domain.A cylinder consists of configurations agreeing with a finite pattern on its specified domain.Source: §2 · p. 3
  • A cellular automaton is a continuous, shift-commuting map on the full shift, and its limit set is a subshift.A finite pattern occurs in a subshift exactly when its cylinder intersects that subshift.Source: §2 · p. 3
  • A finite pattern occurs in a cellular-automaton limit set exactly when its cylinder intersects every finite-time image H^n(Y).Nested compactness gives the limit-set criterion from nonempty intersections at every depth.Source: §2 · p. 3
  • Spatial transitivity requires every pair of nonempty relatively open sets in the limit set to intersect after some translation.For finite-pattern questions, this asks whether occurring patterns can be jointly realized after a relative shift.Source: §2 · p. 3
  • The paper uses the clockwise quarter-turn and x-axis reflection, both of which commute with Life.The Life map G acts on binary configurations over Z^2, and the proof also writes h = G2.Source: §2 · pp. 3–4

3 The proof

The proof reduces non-transitivity to a persistent marker whose predecessors force an infinite lane incompatible with every translated quarter-turn. It constructs and verifies such a marker for Conway’s Game of Life.

3.1 The reduction

  • A uniform ancestral signature records finite pattern pieces forced at prescribed coordinates in every sufficiently deep predecessor of a configuration containing U.Persistence and repeated forcing of translated pump states build the signature; the pumping delay sets how deep a predecessor must be for each added translate.Source: §3.1 · p. 5
  • A fixed pattern U and its quarter-turn can each occur in the limit set, but no configuration contains both at any relative displacement.The reduction turns this incompatibility into disjoint orbit saturations, proving that the spatial action is not topologically transitive.Source: §3.1 · p. 6

3.2 The construction

  • The marker U is placed in a period-two configuration combining a marching-band channel, which supplies the periodic lane and pump states, with Kynnös half-planes that provide self-forcing patches.The patches form a rail used to restore U in predecessors, allowing the pump to restart as the lane grows.Source: §3.2 · pp. 6–7

3.3 The separating lemma

  • Repeated pumping fills the entire bi-infinite lane, so B ⊏ W; Lemma 3.9 establishes that for every v ∈ Z², B and σvρB disagree at a cell of square (3.10).Source: §3.3 · p. 10

4 Discussion

Four additional Life generations extend the forced lane by one four-row period at each end, and compactness turns these finite exclusions into exclusion at every displacement. The result is failure of transitivity, not a complete decomposition; the explicit marker is large and its minimum size is unknown.

4 Discussion

  • Every four additional Life generations add one four-row period to each end of the forced lane, yielding exclusion at every displacement in the limit set.The certificates establish fixed local implications; iteration supplies unbounded spatial scale, and compactness realizes the infinite signature in the limit set.Source: §4 · p. 11
  • The construction proves failure of transitivity, not a complete decomposition of the limit set; the all-zero configuration lies in neither open set.Its present application relies on a realizable periodic background, a marker restored throughout backward history, and pump states incompatible after rotation.Source: §4 · p. 11
  • The explicit marker is large, its smallest possible separating pair is unknown, and broader applicability of this pumping approach remains open.The paper also leaves open whether other mechanisms can produce fixed separating pairs without periodic lanes.Source: §4 · p. 11

A Verification of the finite statements

The verification package records finite inputs and certificates for the marker-restoration and lane-pumping implications. Its command reconstructs formulas, checks certificates, and recomputes finite-state proofs, but this is not a proof-assistant formalization of the whole argument.

A Verification of the finite statements

  • The appendix verifies marker-restoration and lane-pumping implications through finite-state and SAT calculations based on the same finite input patterns.These are separate verification routes by encoding and checker, not by input data.Source: A Verification of the finite statements · p. 12
  • The package includes reconstruction scripts, finite-state calculations, certificate checkers, and a manifest, with a command to run all checks.After setup, run python3 verify.py --all from the artifact root.Source: A Verification of the finite statements · p. 12
  • The reported computational verification is not a proof-assistant formalization of the whole argument.The verification depends on explicit finite implications, input data, and certificates reconstructed and checked by the package.Source: A Verification of the finite statements · p. 12

A.1 Finite patterns

This appendix specifies finite periodic patches, the marker, its rail, and pump states used in the construction, alongside finite checks of their properties. The marker consists of two caps whose union agrees with the periodic witness.

A.1 Finite patterns

  • The Kynnös tile Q, marching-band tile M, and transition strips AL and AR have fundamental vertical periods 6, 4, and 12, respectively.The Kynnös patch is formed from a rectangle with 32 specified cells removed near its corners.Source: §A.1 · pp. 12–13
  • The 584-cell spatially phased Kynnös patch is checked by SAT for self-forcing at the same position in predecessor and output.The periodic witness also has an orbit of exact period two, established by checking G2(c0)=c0 on 900 cells and showing G(c0) differs from c0.Source: §A.1 · p. 13
  • The marker U is assembled from bottom and top caps; their disjoint domains contain 2,456 and 1,503 cells, and their union has 3,959 cells.The cap values agree with c0, and translation by (0, −24) preserves the vertical phase.Source: §A.1 · p. 13
  • The raw marker has 6,726 cells, while bU has 6,719 after seven cells are omitted; four distinguish predecessor branches and three remain free.The remaining prescribed cells are common to the predecessor branches retained in the construction.Source: §A.1 · p. 13
  • The 56-cell pump states S+ and S− are subpatterns of U, each containing four complete rows of the width-three lane.They are related by S−= σ(4,19)κS+; reflection of the verified upper-pump implication gives the lower displacement (0, −4).Source: §A.1 · p. 14

A.2 Finite-state verification

The finite-state verification sweeps a cut across a spacetime patch, tracking boundary extensions and monitor outcomes while checking Life equations. Soundness and completeness of the transfer support the local implications used in marker restoration and pumping.

A.2 Finite-state verification

  • A layered DFA accepts boundary words that extend into the scanned region, while a monitor records properties such as target mismatches across possible extensions.A terminal colour records the set of monitor outcomes for extensions of a boundary word.Source: §A.2 · p. 14
  • The boundary transfer represents exactly those boundary words that extend into the scanned finite spacetime region, assuming each checked Life equation has its full input neighbourhood.The transfer is sound and complete: it neither discards a valid extension nor introduces a spurious one.Source: §A.2 · p. 14
  • Moving the cut left reads four new bits, chooses two hidden bits, and carries correlated tuples of boundary states and the preceding two six-bit rows.Once three rows are available, the scan checks the two Life equations at the middle row of column a.Source: §A.2 · p. 15
  • The finite-state calculations preserve extensions and monitor colours through each cut update, with induction over rows and columns establishing the invariant.Taking sets of correlated tuples handles multiple interior extensions and their differing monitor outcomes.Source: §A.2 · p. 15
  • For Lemma 3.7, reachable terminal masks exclude the all-failure mask, one-step scans rule out both nonreference candidates, and a mismatch monitor finds no extension disagreeing with the 56 target cells.Together, the three implications prove Lemma 3.7.Source: §A.2 · p. 15
  • The marker-restoration proof uses nine boundary-automaton stages to derive U in the older layer from U in the output and the common rail premises.Stages 4–9 reconstruct six disjoint regions, progressing from the marker centre toward its outer parts.Source: §A.2 · pp. 15–16
  • The restoration stages’ target regions partition dom(U), and the composition check verifies disjointness, union, and each stage’s premises.The check establishes Lemma 3.6.Source: §A.2 · p. 16

A.3 SAT proofs

The section proves three local implications by encoding finite counterexamples as SAT formulas and checking them unsatisfiable. Finite-domain reconstruction connects these checks to implications over arbitrary Life configurations.

A.3 SAT proofs

  • Complete local equations on finite layer domains correspond to restrictions of global Life histories, and any satisfying finite assignment extends to a global history.The oldest layer is completed arbitrarily, then Life is iterated forward; induction shows agreement on every layer.Source: §A.3 · p. 16
  • Each implication is encoded by local Life equations, fixed premises, and a clause requiring a target cell to differ from its prescribed value.The domains and premises for the three formulas are listed in Table 3.Source: §A.3 · p. 16, Table 3 · p. 17
  • The verification checks totalizer certificates with DRAT-trim and LRAT checkers, while separate binary-adder and cell-only encodings cross-check local semantics and reconstruct the implications.The binary-adder checks pass for all 4096 inputs and 8192 satisfiability queries; the cell-only LRAT certificates are checked by cake_lpr.Source: §A.3 · p. 17
  • Checked unsatisfiability of the three reconstructed formulas completes the SAT proofs of Fact 3.4 and Lemmas 3.6 and 3.7.Each formula encodes a counterexample to its corresponding implication.Source: §A.3 · pp. 16–17
Loading 2609.34122v1…