Window
Window defines a finite segment of length n on a one-dimensional cellular automaton tape as a function from the finite set Fin n to CellState. Researchers constructing local gadgets for SAT evaluation in the Recognition Science P vs NP model would cite this when representing clause configurations. The declaration is a direct type abbreviation with no further computational content.
claimA window of size $n$ is a map from the finite index set $0,1,…,n-1$ to the cell states Zero, One, Signal, Gate, Wire, or Blank.
background
The module supplies cellular automata gadgets that evaluate SAT instances via local rules on a 1D tape. CellState is the inductive enumeration Zero (Boolean 0), One (Boolean 1), Signal (propagating marker), Gate (AND/OR/NOT), Wire (passive connector), and Blank (empty). Neighborhood and radius = 1 supply the local three-cell view used by every update. The module states that the CA computes SAT in O(n^{1/3} log n) time while result readout still costs Ω(n) queries because of balanced-parity encoding.
proof idea
One-line type abbreviation that directly identifies Window n with the function type Fin n → CellState, using the already-declared CellState inductive type.
why it matters in Recognition Science
Window supplies the basic data type for all clause encodings and ledger-compatible CA steps in the module. It is invoked by encodeClause to turn SAT clauses into cell configurations and appears in downstream results such as paired_preserves_balance and costCompose_right_cancel. The definition therefore anchors the local-rule infrastructure that the module uses to claim faster-than-naive SAT evaluation while preserving reversibility for ledger balance.
scope and limits
- Does not define any update rule or step function.
- Does not enforce locality constraints beyond the Fin n domain.
- Does not address reversibility or ledger compatibility.
- Does not relate the CA window to the RS-native measurement Window structure.
Lean usage
def sampleWindow (n : ℕ) : Window n := fun _ => CellState.Blankformal statement (Lean)
50def Window (n : ℕ) := Fin n → CellState
proof body
Definition body.
51
52/-! ## Local Update Rules -/
53
54/-- Neighborhood radius for the CA -/