Tape
plain-language theorem explainer
The definition introduces the state space for the one-dimensional cellular automaton as all functions from the integers into the finite set of cell states. It is cited by proofs establishing locality of the update rule and the simulation by Turing machines in the SAT reduction argument. The introduction requires no derivation beyond the type alias.
Claim. The tape is the function space $T : {Z} {to} C$, where $C$ is the inductive type of cell states with constructors Zero, One, Signal, Gate, Wire and Blank.
background
The module develops cellular automata gadgets to embed SAT instances into local evolution rules for the P-vs-NP resolution. CellState is the inductive type whose constructors are Zero and One for Boolean values, Signal for propagation, Gate for logical markers, Wire for passive connections, and Blank for empty positions. The tape itself is modeled as an infinite line indexed by integers, with finite windows extracted for local updates as noted in the module comment. Upstream structures supply the J-cost minimization and dimensional constraints that motivate the discrete CA model.
proof idea
The declaration is a direct type definition equating the tape to the function type from integers to CellState. It serves as the domain for subsequent definitions such as neighborhood extraction and the global step function.
why it matters
This supplies the configuration space for the theorems establishing that each update depends only on a radius-one neighborhood and that information propagates at finite speed. It underpins the Turing machine simulator structure and the Church-Turing connection. Within the framework it realizes the local dynamics required for J-cost minimization while enabling the claimed evaluation time for SAT instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.