The merger invariant
Abstract
The binary Klein-four shift has two fixed configurations, three two-point orbits, and two free orbits. The free orbits consist of weight-one and weight-three configurations. An equivariant map satisfies Criterion when a common free image of these two orbits forces both constants and one two-point orbit to share one constant image. The structural argument is adapted from the MIT-licensed public supplementary formalization by E. Alcala-Arroyo, A. Castillo-Ramirez, H. Ma and W. Zhang, version v1.1.0, DOI 10.5281/zenodo.23280244.
Theorem 1.1 (Composition preserves the criterion).
Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/CellularAutomata/KleinFourInvariant.criterion_mul (✓ std3). ∎
Citation. Edgar Alcalá-Arroyo; Alonso Castillo-Ramirez; Haobo Ma; Wenlin Zhang (2026). Supplementary material for Generation by lazy and invertible cellular automata over the Klein four-group. DOI: 10.5281/zenodo.23280244. URL: https://github.com/the-omega-institute/klein-four-lazy-ca-supplement/tree/fae47ad9dbbd4cbc1462a058dffe6ad4c2e416f1.
Commentary.
Suppose the composite A B maps both free orbits onto one free orbit. A nonfree configuration cannot acquire a free image under an equivariant map. Thus both intermediate images are free. If they lie in the same free orbit, B has a merger witness, and postcomposition by A preserves it. If they lie in different free orbits, A has a merger witness; precomposition by B preserves it because constant and two-point strata cannot leave their stabilizer classes. Composition acts right-to-left.
Theorem 1.2 (Every generated map satisfies the criterion).
Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/CellularAutomata/KleinFourInvariant.membership_implies_criterion (✓ std3). ∎
Citation. Edgar Alcalá-Arroyo; Alonso Castillo-Ramirez; Haobo Ma; Wenlin Zhang (2026). Supplementary material for Generation by lazy and invertible cellular automata over the Klein four-group. DOI: 10.5281/zenodo.23280244. URL: https://github.com/the-omega-institute/klein-four-lazy-ca-supplement/tree/fae47ad9dbbd4cbc1462a058dffe6ad4c2e416f1.
Commentary.
Here M is the submonoid generated by every bijective equivariant map and every binary lazy map, on any neighborhood containing the identity. Units cannot merge the two free orbits. Every lawful lazy map satisfies the criterion, and the identity does too. Closure under composition therefore gives the assertion, including the empty word.