Window
plain-language theorem explainer
Finite windows of length n on the cellular automaton tape are realized as maps from the finite set of n positions to the six cell states. Workers on the SAT-CA embedding cite this when building clause gadgets and when aggregating recognition costs over discrete segments. The definition is a one-line type abbreviation with no computational content.
Claim. Let $C$ be the set of cell states. A finite window of length $n$ is a function from the set of $n$ consecutive positions to $C$.
background
The module supplies cellular automata gadgets that embed SAT instances into a 1D automaton with local rules derived from Rule 110. CellState is the inductive type whose constructors are Zero, One, Signal, Gate, Wire and Blank. Radius is fixed at 1 and Neighborhood is the ordered triple of left, center and right cells. The imported RSNative.Core.Window records a start tick and length in ticks; the present definition specializes that idea to finite functions over cell states. The module states that SAT evaluation proceeds by a CA whose computation time is O(n^{1/3} log n) while reading the result still requires Ω(n) queries due to balanced-parity encoding.
proof idea
One-line definition that directly equates the window type to the function space from the finite index set to cell states. No lemmas are invoked.
why it matters
The definition supplies the finite tape segments required by encodeClause and by downstream results in CostAlgebra and LedgerAlgebra that aggregate over windows. It supports the claim that CA computation preserves ledger balance while remaining faster than naive SAT algorithms. It supplies the discrete measurement objects needed for the eight-tick octave and recognition cost accounting in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.