encodeClause
The definition encodeClause turns a clause gadget (variable list plus negation flags) and a Boolean assignment into a finite tape window of cell states. Researchers modeling SAT via one-dimensional cellular automata for the P versus NP question cite it when constructing explicit local configurations. The body is a direct index-by-index case split that maps each variable position to One or Zero according to the assignment, inserts an OR gate marker, and fills the rest with wires.
claimLet $g$ be a clause gadget over $n$ variables with list of indices and negation flags, and let $a$ be an assignment from the $n$ variables to Boolean values. Then encodeClause$(g,a)$ is the function from positions $0$ to $w-1$ (where $w=3k+2$ for $k$ variables in the clause) to cell states that returns the appropriate One or Zero state for each variable position (flipped when the flag is true), places an OR-gate cell at the clause boundary, and returns a wire cell elsewhere.
background
The module builds one-dimensional cellular automata whose local rules evaluate Boolean circuits, drawing on the Rule 110 model for universal computation. A clause gadget packages the indices of variables that appear in one clause, their negation status, a tape starting position, and a computed width of three cells per variable plus two extra cells. The Window type is the finite function Fin $w$ to CellState that represents any local segment of the tape.
proof idea
The definition is written as an explicit lambda that branches on the numeric value of the window index $i$. When $i$ is inside the variable list it looks up the index and negation flag, evaluates the assignment, and chooses the matching cell state. At the exact clause position it returns the Gate constructor; all remaining positions return the Wire constructor.
why it matters in Recognition Science
This definition supplies the concrete map from an abstract SAT clause to a local CA configuration, forming the first step in the module's construction of gadgets that evaluate SAT instances under local rules. It supports the module claim that SAT can be decided by a cellular automaton in time $O(n^{1/3} log n)$ while preserving the balanced-parity encoding that forces linear query cost for the result. No downstream uses are recorded, so the definition acts as a foundational building block rather than an intermediate lemma.
scope and limits
- Does not define the local update rule that evolves the encoded window.
- Does not prove that the encoding preserves satisfiability after any number of CA steps.
- Does not extend to a full multi-clause SAT instance.
- Does not address the global time or space complexity of the resulting automaton.
formal statement (Lean)
143def encodeClause (g : ClauseGadget n) (assignment : Fin n → Bool) : Window g.width :=
proof body
Definition body.
144 fun i =>
145 if i.val < g.variables.length then
146 let var_idx := g.variables.get! i.val
147 let neg := g.negated.get! i.val
148 let val := assignment var_idx
149 if neg then (if val then .Zero else .One)
150 else (if val then .One else .Zero)
151 else if i.val = g.variables.length then
152 .Gate -- OR gate
153 else
154 .Wire
155
156/-- A full SAT instance encoded as CA tape -/