step
plain-language theorem explainer
The step definition supplies the global successor map for a one-dimensional cellular automaton tape. Researchers working on SAT-to-CA reductions in the Recognition Science setting cite it to establish deterministic local evolution. The implementation is a direct pointwise application of the local rule to each extracted three-cell neighborhood.
Claim. The successor tape $T'$ satisfies $T'(i)$ equals the local update rule applied to the three-cell neighborhood of $T$ at each integer position $i$.
background
The Tape type is an infinite sequence of CellState values indexed by integers. Neighborhood extraction pulls the radius-1 window consisting of cells at positions i-1, i, and i+1. The local update rule is a deterministic function that maps each such triple to the next cell state, implementing signal propagation and wire behaviors adapted from Rule 110.
proof idea
The definition is a one-line wrapper that applies the local update rule to the neighborhood extracted at each integer position on the tape.
why it matters
This operator realizes the deterministic global evolution step required for the cellular-automaton encoding of SAT instances. It is used by forty downstream declarations, including srCost_pos_off_threshold for acoustic cost thresholds and actionJ_local_min_is_global for convexity arguments in the action functional. Within the module it supports the claim that SAT computation via local CA rules respects the Recognition Science locality and reversibility constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.