Generation by lazy and invertible cellular automata over the Klein four-group

Edgar Alcalá-Arroyo, Alonso Castillo-Ramirez, Haobo Ma, Wenlin Zhang

math.GR Oct 14, 2026 · v1

formalization mathlib algebra combinatorics

Read PDF arXiv abstract Code

TL;DR

The membership criterion and the cardinalities 59,712 and 4,007 are formalized in Lean 4 with Mathlib, kernel-checked without native_decide, in supplementary material.

Abstract

Let $G=C_2\times C_2$ and $A=\{0,1\}$. We characterize the submonoid of $\text{CA}(G;A)$ generated by lazy and invertible cellular automata. A cellular automaton belongs to this submonoid if and only if, whenever it maps the two free $G$-orbits onto the same free orbit, it maps both constant configurations and some two-point orbit to the same constant. The proof gives a factorization using elementary orbit collapses and three two-cell lazy maps. The criterion yields the cardinality $59\,712$ and identifies the maps missed by a weaker constant-separation invariant. Adjoining one idempotent generates the full monoid, and the generated submonoid is contained in exactly one maximal proper submonoid, of cardinality $65\,024$. The submonoid generated by lazy maps alone has $4\,007$ elements, and for both generating sets the maximum shortest-word length is six. The criterion and the cardinalities $59\,712$ and $4\,007$ are formally verified in Lean.

Problem

Alcalá-Arroyo and Castillo-Ramirez asked whether lazy and invertible cellular automata generate the full cellular-automaton monoid. The binary full shift over the Klein four-group is known to be an obstruction. The open task is to describe the proper submonoid these maps generate in that case.

Approach

The monoid CA(G;{0,1}) is identified with the endomorphism monoid of the G-set {0,1}^G, which has seven orbits. Membership is characterized through a factorization into elementary orbit collapses and three two-cell lazy maps. Relative rank and maximal submonoids are analyzed using rank ideals. The criterion and the cardinalities are formalized in Lean 4 with Mathlib, using only the standard axioms.

Results

A map lies in the generated submonoid exactly when, whenever it merges the two free orbits, it sends both constants and some two-point orbit to the same constant. The submonoid has 59,712 elements and adjoining one idempotent generates the full monoid. It lies in a unique maximal proper submonoid of size 65,024. The lazy-only submonoid has 4,007 elements, and the maximum shortest-word length is six for both generating sets.

Set	Size
CA(G;A)	65,536
Invertible CA	512
Generated submonoid M	59,712
Unique maximal proper submonoid containing M	65,024
Lazy-only submonoid	4,007

Key cardinalities

Papers With

Generation by lazy and invertible cellular automata over the Klein four-group