trureturingGitHub MATHEMATICAL ATLAS

RESEARCH / Focused target

Lazy and invertible cellular automata do not generate all cellular automata

Literature status: not recheckedRepository record: refuted

RELEASED FOUNDATIONS / PROPOSED CONNECTION

Research connections

0 released anchors
All source anchors (1)

Problem

The question

E. Alcalá-Arroyo and A. Castillo-Ramirez (arXiv:2510.14841, cs.FL with nlin.CG; Theoret. Comput. Sci. 1076 (2026) 115965) study the lazy cellular automata over A^G: a local map on a finite neighborhood S ∋ e returns the central value z(e) on every pattern z except one, the unique active transition p, where it writes a symbol different from p(e). Motivated by the generation of the full transformation monoid of a finite set by its permutations and its idempotents of defect one, they ask:

If $\mathcal{L}(G,A)$ is the set of all lazy cellular automata over $A^G$, prove or disprove the following: $\text{CA}(G,A) = \langle \text{ICA}(G,A) \cup \mathcal{L}(G,A) \rangle$.

Issue #11773 fixes the reading: every group G and every finite alphabet A with at least two symbols, cellular automata and lazy automata as in the paper, ICA(G, A) the units of the monoid CA(G, A) under composition, and ⟨C⟩ the submonoid generated by C. The result disproves the equality.

Motivation

Our foothold

A positive answer would reduce every cellular automaton to invertible ones and automata that act at a single local pattern, the analogue for A^G of the generation of Tran(A) by Sym(A) and the idempotents of defect one; the paper notes that the lazy automata with neighborhood {e} are exactly those idempotents. The frozen declaration D5/S3/StatisticalMechanics/CellularAutomata/LazyInvertibleGeneration.result shows that the equality fails for the Klein four-group and the binary alphabet.

Gap

Missing bridges

Issue #11773 preregisters the reading, the witness, the route and the literature check. Problem 2 is stated in arXiv v3, the latest version. Semantic Scholar lists no citing record. arXiv searches for "lazy cellular" and "unique active transition" return only the paper and its predecessor (arXiv:2411.03601); the work on generating sets of CA(G, A) relative to ICA(G, A) for finite G (Castillo-Ramirez and Gadouleau, arXiv:1601.05694) does not consider lazy automata.

These readings are not-found-in-searched-scope; they do not establish an exhaustive worldwide literature search, priority, or the absence of an independent answer.

Route

Proposed approach

Let G be the Klein four-group, A = {0, 1}, w(x) the number of cells of x equal to 1, and F(x) the complement of x when w(x) = 1, and x otherwise.

  1. F is a cellular automaton with neighborhood G, since w is invariant under the shifts.
  2. Every cellular automaton commutes with the shifts. In the Klein group a configuration has even weight exactly when a shift by some k ≠ e fixes it, so cellular automata send even weight to even weight, and they send the constant configurations c₀, c₁ to constant configurations.
  3. A lazy automaton with constant pattern b sends c₀ and c₁ to c_{1−b}. With a non-constant pattern, on a configuration of weight one (three) the pattern occurs at most once, located by a cell where it is 1 (0), so the automaton fixes the configuration or changes one cell and makes the weight even.
  4. The property "if T c₀ ≠ T c₁, then T is injective on the configurations of odd weight whose image has odd weight" holds for invertible and for lazy automata and is preserved by composition, so it holds on the generated submonoid.
  5. F separates c₀ and c₁ but sends the configuration with a single 1 at e and its complement, of weight three, to that complement.

Falsifier

What would falsify this route

The answer would change if ICA(G, A) were read as a set strictly larger than the injective automata, or if ⟨·⟩ allowed infinite compositions; the paper defines neither. It would also change for the smaller groups: by the computation below, the equality holds for the cyclic groups of order at most four with the binary alphabet.

Evidence

Evidence to collect

An exhaustive Python computation (issue #11773) over the 16 configurations of the Klein four-group finds 65 536 shift-equivariant maps, 54 lazy and 512 invertible automata, and a generated submonoid of 59 712 elements that does not contain F. As controls, every lazy automaton lies in the computed submonoid, and for the cyclic groups of orders 1, 2, 3 and 4 the same code finds the submonoid equal to CA(G, A).

The canonical source is D5/S3/StatisticalMechanics/CellularAutomata/LazyInvertibleGeneration.lean. Its public declarations are IsCA, IsLazy, IsInvertibleCA, claim and result. The frozen module state has statement identity sha256:5cbad1e3ef5fa57f4614f49e203eadf64adeedf0568b7cada8a7ff370037f18c. The result declaration has statement identity sha256:60558c7904887c04979774c14e890e81962f3ce7755d5902752c52827bec4479. The Freeze event is sha256:7d1612b4444052356f299a1db103e27dc728e92db7f4fc2cb68a695c4e04e0c8. It has no project-level frozen prerequisites (pinned Mathlib only). The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Triage

Scope assessment

Tier 1 open problem from a 2025 paper, preregistered in issue #11773 before any Lean. theorem; resolution refuted. The public theorem has proof_shape: content, with escape witness form (2), the conclusion itself: inside its proof, the induction over the generated submonoid with the invariant of Route step 4, and the single-occurrence argument for lazy automata that preserves it, are local steps on its live path. Its admission basis is open-problem-resolution. Utility kind=certified-instance; basis=refutes with typed claim and result.

What the settlement shows

Proved (Lean): over the Klein four-group with the binary alphabet, the automaton F is not a finite composition of invertible and lazy cellular automata, so CA(G, A) ≠ ⟨ICA(G, A) ∪ L(G, A)⟩ there.

Mechanism (proved inside result): a lazy automaton either merges the two constant configurations or moves a configuration of odd weight by at most one cell; in the Klein group a single cell change of an odd-weight configuration creates a nontrivial stabilizer, which no later cellular automaton can remove. Hence every element of the generated submonoid that keeps the two constants apart is injective on the configurations of odd weight (trivial stabilizer) whose image also has odd weight; F merges two such configurations.

Computed (Python, not formalized): among the groups of order at most four with the binary alphabet, the Klein four-group is the only one where the equality fails; ⟨ICA ∪ L⟩ misses 5 824 of the 65 536 cellular automata.

Argument (not formalized): the equality also fails for G = ℤ and every finite alphabet A with at least two symbols. Under the uniform Bernoulli measure the cylinder {x : τ(x)(0) = p(e)} of a lazy automaton τ has measure 1/|A| − |A|^{−|S|} < 1/|A|, while surjective cellular automata on A^ℤ preserve the uniform measure (Hedlund, Math. Systems Theory 3 (1969) 320–375), so no lazy automaton is surjective. If a surjective T = T_m ⋯ T_1 with invertible or lazy factors, then T_m is surjective, hence invertible, and induction makes T injective. Identifying A with ℤ/|A|ℤ, the automaton x ↦ (g ↦ x(g) + x(g + 1)) is surjective, since a preimage of y is obtained from any value of x(0) by solving x(g + 1) = y(g) − x(g) forward and x(g) = y(g) − x(g + 1) backward, and not injective, since the |A| choices of x(0) give distinct preimages; so it is not generated.

Open: the follow-up of Problem 2, a description of ⟨ICA ∪ L⟩ and of ⟨L⟩; and which finite groups satisfy the equality.

Source consequences: the paper's results on the order of lazy automata do not depend on Problem 2 and stand; Problem 1 (idempotency) is untouched.

ASSUMED-UNVERIFIED

Unverified assumptions

The Theoret. Comput. Sci. text was not read, so it is unverified whether the problem was edited there. The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent answer. The Lean kernel does not authenticate the external source or its version history.

Dossier & anchor history

Loading release observations...