CellState
CellState enumerates the six values a cell may hold in the one-dimensional Boolean cellular automaton built to evaluate SAT instances via local rules. Researchers constructing parallel SAT solvers inside the Recognition Science model cite it as the discrete alphabet for the tape. The declaration is a plain inductive definition that introduces constructors for Boolean literals, propagating signals, gate markers, wires, and vacancies.
claimLet $S = {0, 1, S, G, W, B}$ be the set of cell states, where $0$ and $1$ are Boolean values, $S$ denotes a propagating signal, $G$ a logic-gate marker, $W$ a passive wire, and $B$ an empty cell.
background
The module constructs cellular-automaton gadgets that realize SAT evaluation with local update rules derived from Rule 110. A Tape is an infinite map from integers to cell states; a Window extracts a finite segment of length $n$; a Neighborhood is the ordered triple of states at positions $i-1$, $i$, $i+1$. Upstream CircuitLedger.Gate supplies the gate-type and parent-index structure that the CA gadgets embed as markers.
proof idea
The declaration is an inductive definition that enumerates six constructors with no computational content or proof obligations.
why it matters in Recognition Science
CellState supplies the state alphabet required by localRule, Neighborhood, Tape and Window, which together establish that SAT instances can be processed by a local, deterministic, reversible CA. This step supports the module claim of $O(n^{1/3} log n)$ evaluation time while preserving ledger compatibility. It interfaces the circuit representation (from CircuitLedger) with the spatial evolution model used for the P-vs-NP argument in Recognition Science.
scope and limits
- Does not define any transition function or update rule.
- Does not specify locality radius or reversibility axioms.
- Does not connect states to phi-ladder or physical constants.
- Does not prove universality or simulation bounds.
formal statement (Lean)
37inductive CellState
38 | Zero -- Boolean 0
39 | One -- Boolean 1
40 | Signal -- Propagating signal
41 | Gate -- AND/OR/NOT gate marker
42 | Wire -- Passive wire
43 | Blank -- Empty cell
44 deriving DecidableEq, Repr
45
46/-- The CA tape is an infinite sequence of cells, but we work with finite windows -/