localRule
plain-language theorem explainer
The local update rule maps each three-cell neighborhood to its successor center state via explicit cases for signal movement, AND/OR/NOT gates, and state preservation. Researchers modeling SAT evaluation through one-dimensional automata would cite this definition to establish that circuit computation remains strictly local. The definition is realized by exhaustive pattern matching on the six cell states.
Claim. Let $N$ be a neighborhood of three consecutive cell states $(l,c,r)$ drawn from the set $S = $ {Zero, One, Signal, Gate, Wire, Blank}. The map $f:N→ S$ is defined by the cases: signal propagation yields Signal when the center is Signal and the right neighbor is Wire or Blank, or when the left neighbor is Signal and the center is Wire; AND behavior on a Gate center outputs One only when both neighbors are One; OR behavior on a Wire center outputs One when at least one neighbor is One; NOT behavior inverts the center when the left neighbor is Signal; otherwise the center state is preserved.
background
The module constructs cellular automata gadgets to evaluate SAT instances in a one-dimensional setting. CellState is the inductive type whose constructors are Zero and One for Boolean values, Signal for propagating information, Gate for logic markers, Wire for passive connections, and Blank for unoccupied positions. Neighborhood is the structure that packages the three adjacent cells left, center, and right at any tape position.
proof idea
The definition proceeds by a single match expression on the triple of left, center, and right states. It dispatches first on signal-propagation patterns, then on Gate-centered AND cases, Wire-centered OR cases, Signal-left NOT cases, and finally defaults to copying the center state.
why it matters
This definition supplies the update function invoked by the step operation and the locality theorem ca_is_local. It implements the module's claim that SAT can be evaluated by a CA whose local rules realize Boolean circuits while preserving reversibility for ledger compatibility. The construction sits inside the Complexity domain that supports the P-vs-NP argument via the O(n^{1/3} log n) parallel bound, though its direct connection to the T0-T8 forcing chain is left to the foundational modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.