Window
plain-language theorem explainer
Finite segments of length n on the cellular automaton tape are formalized as maps from a finite index set of size n into the possible cell states. Researchers analyzing the parallel evaluation of SAT instances via local automata rules reference this when building clause encodings and establishing sublinear time bounds. It is supplied as a direct type abbreviation that supports neighborhood extraction and local rule application.
Claim. A window of size $n$ is a function from the finite set of indices from 0 to $n-1$ to the set of cell states, where the cell states consist of the constructors Zero, One, Signal, Gate, Wire and Blank.
background
This module develops cellular automata gadgets for embedding SAT instances into a one-dimensional automaton. The construction exploits local update rules to achieve evaluation in order $n^{1/3} log n$ time, although extracting the result still demands linear queries because of the balanced-parity encoding. CellState is the inductive type labeling tape positions with Zero, One, Signal, Gate, Wire or Blank. Neighborhood collects states at positions i-1, i and i+1 with radius fixed at one. The local setting draws on Recognition Science to keep rules reversible for ledger compatibility.
proof idea
The declaration is a direct type definition that equates the window of size n with the function type from a finite index set of size n to the cell states. It inherits decidable equality and representation from the inductive cell state type.
why it matters
This definition is used by the encodeClause construction that maps SAT clauses to cell configurations and appears in theorems on cost composition right cancellation and ledger balance preservation. It realizes the module's insight that a local cellular automaton can evaluate SAT instances in sub-cubic time. The approach connects to the Recognition Science landmarks of local rules, the eight-tick octave for periodicity, and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.