CellState
plain-language theorem explainer
CellState enumerates the six discrete states available to each cell in a one-dimensional cellular automaton that evaluates Boolean SAT instances via local rules. Researchers constructing the Recognition Science P-vs-NP argument cite it when building reversible gadgets that simulate circuit evaluation. The declaration is a plain inductive type with no computational content or hidden hypotheses.
Claim. Let $C$ be the finite set of cell states consisting of Boolean zero, Boolean one, a propagating signal, a gate marker (AND/OR/NOT), a passive wire, and an empty blank cell.
background
The module supplies the cellular-automaton layer for the Recognition Science treatment of SAT. It works with an infinite tape whose cells take values in $C$ and restricts attention to finite windows so that local update rules can be stated explicitly. The construction adapts the Rule 110 universal CA to Boolean circuit evaluation while preserving reversibility for ledger compatibility.
proof idea
The declaration is an inductive definition that simply lists the six constructors; no lemmas or tactics are applied.
why it matters
CellState is the base type for the downstream definitions of Neighborhood, Tape, Window and localRule. Those objects are used to establish that SAT evaluation can be performed by a local, deterministic, reversible CA whose running time is $O(n^{1/3} log n)$. The definition therefore supplies the concrete alphabet required by the module's claim that the CA exploits parallelism while the balanced-parity encoding still forces an $Omega(n)$ query lower bound for result extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.