encodeClause
plain-language theorem explainer
This definition constructs a finite window of cell states that represents a single SAT clause gadget under a given Boolean assignment. Researchers modeling P vs NP via one-dimensional cellular automata would cite it when building SAT instances as CA tapes. The body is a direct case analysis on cell index: it maps variable positions to One or Zero (flipped by negation), places an OR gate after the variables, and fills the rest with wires.
Claim. Let $g$ be a clause gadget with variable indices, negation flags, and width $w = 3k+2$ where $k$ is the number of literals. For an assignment $a : [n] → {0,1}$, the map $i ↦$ cell state returns the literal evaluation (One if true under $a$, Zero if false, swapped when negated) for $i < k$, an OR gate at $i = k$, and a wire otherwise.
background
The module builds cellular-automata gadgets to encode SAT for the P-vs-NP argument. A ClauseGadget packages the literals of one clause together with their positions on the tape; its width is fixed at three cells per literal plus two extra cells. Window is the type of a finite tape segment, i.e., a function from Fin w to CellState. The surrounding development adapts Rule 110 to evaluate Boolean circuits locally and reversibly so that the global ledger remains compatible with Recognition Science.
proof idea
The definition is written directly as a lambda that branches on the index i. For i inside the variables list it indexes the variable and negation lists, reads the assignment, and chooses One or Zero accordingly. At the exact index equal to the number of variables it returns the Gate constructor; all remaining positions return Wire.
why it matters
It supplies the concrete encoding step that turns an abstract clause into the initial tape segment required by the CA evaluation model described in the module header. The construction is a prerequisite for showing that SAT instances can be processed by a local, deterministic, reversible cellular automaton whose computation time is claimed to be O(n^{1/3} log n). No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.