encodeClause
plain-language theorem explainer
The definition constructs a finite tape segment that places the literals of one SAT clause into cell states under a supplied Boolean assignment, inserting an OR gate marker at the clause boundary. Workers building the cellular-automaton SAT solver inside the Recognition Science P-versus-NP argument would invoke this gadget when assembling the full instance tape. The map is defined by direct index cases that read the variable list and negation flags from the gadget record and emit One, Zero, Gate or Wire accordingly.
Claim. Let $g$ be a clause gadget holding a list of variable indices in $[n]$, a parallel list of negation flags, a tape offset, and width $w=3k+2$ where $k$ is the number of literals. For an assignment $a$ mapping each of the $n$ variables to a Boolean, the encoded window is the function on indices $0..w-1$ that returns the cell state One or Zero for each literal position according to the value of $a$ and the negation flag, returns the OR-gate marker exactly at position $k$, and returns the wire state elsewhere.
background
The CellularAutomata module supplies local gadgets that embed Boolean SAT instances into a one-dimensional cellular automaton whose update rule is derived from Rule 110. A ClauseGadget packages the indices of the variables that appear in a single clause, the corresponding negation flags, the starting tape coordinate, and a computed width of three times the literal count plus two. The Window type is the finite map Fin w → CellState that represents any contiguous segment of the tape on which the local rule will act.
proof idea
The definition is supplied directly by a lambda that branches on the window index i. When i is strictly less than the length of the variable list it extracts the variable index and negation flag, reads the assigned Boolean value, and selects One or Zero according to the polarity. At the index equal to the variable count it emits the Gate marker; every larger index receives the Wire state.
why it matters
This gadget is the atomic unit that lets an arbitrary SAT clause be written onto the CA tape while preserving locality and determinism. It directly implements the first claim listed in the module documentation that SAT can be evaluated by a cellular automaton with local rules. Because the construction is purely syntactic it supplies the concrete encoding step required before any later argument about computation time or query complexity can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.