localRule
localRule specifies the deterministic successor state for each cell in a one-dimensional cellular automaton whose neighborhoods encode Boolean gates and signal propagation. Researchers modeling SAT instances via local computation in Recognition Science would reference this rule when establishing the locality of the global step function. The definition is given by exhaustive case analysis on the three-cell neighborhood.
claimThe local update rule maps a neighborhood triple $(left, center, right)$ of cell states to the next center state by cases: signal propagates rightward on Wire or Blank; Wire carries Signal; AND gate outputs One only if both inputs are One; OR gate outputs One if either input is One; NOT inverts the center on Signal input; otherwise the center state is preserved.
background
CellState is an inductive type with constructors Zero and One for Boolean values, Signal for propagating information, Gate for operation markers, Wire for passive connections, and Blank for empty positions. Neighborhood is a structure holding the left, center, and right CellState values at a given tape position. This definition sits inside the Cellular Automata module, which supplies local deterministic gadgets for SAT evaluation in a 1D automaton inspired by Rule 110, with the explicit goals of O(n^{1/3} log n) computation time and reversibility for ledger compatibility.
proof idea
The definition is implemented by exhaustive pattern matching on the left, center, and right fields of the input Neighborhood. Cases are ordered to handle signal propagation first, followed by AND/OR gate logic, NOT inversion, and a final default clause that returns the unchanged center state.
why it matters in Recognition Science
localRule supplies the concrete update mechanism required by the downstream step definition and the ca_is_local theorem that certifies radius-1 locality. It realizes the Boolean circuit gadgets needed for the SAT-to-CA reduction in the P vs NP argument. The rule set preserves the deterministic and reversible character demanded by the simplicial ledger and the Recognition Science forcing chain.
scope and limits
- Does not define the global tape evolution or initial configuration for SAT instances.
- Does not prove correctness of the SAT evaluation or the stated time bound.
- Does not establish universality or reversibility of the full automaton.
- Does not address embedding into higher-dimensional or continuous Recognition Science models.
formal statement (Lean)
70def localRule (n : Neighborhood) : CellState :=
proof body
Definition body.
71 match n.left, n.center, n.right with
72 -- Signal propagation: Signal moves right
73 | _, .Signal, .Wire => .Signal
74 | _, .Signal, .Blank => .Signal
75 -- Wire carries signal
76 | .Signal, .Wire, _ => .Signal
77 | .Signal, .Blank, _ => .Blank -- Signal consumed
78 -- AND gate: both inputs must be One
79 | .One, .Gate, .One => .One
80 | .One, .Gate, .Zero => .Zero
81 | .Zero, .Gate, .One => .Zero
82 | .Zero, .Gate, .Zero => .Zero
83 -- OR gate: either input is One
84 | .One, .Wire, .One => .One
85 | .One, .Wire, .Zero => .One
86 | .Zero, .Wire, .One => .One
87 | .Zero, .Wire, .Zero => .Zero
88 -- NOT gate: invert center when activated
89 | .Signal, .Zero, _ => .One
90 | .Signal, .One, _ => .Zero
91 -- Default: preserve state
92 | _, c, _ => c
93
94/-- Apply local rule globally to create successor tape -/