ClauseGadget
plain-language theorem explainer
ClauseGadget packages the variable indices, negation flags, tape position, and default width for one SAT clause as a 1D cellular automaton segment. Researchers tracing the Recognition Science P-vs-NP sketch would cite it when assembling the full SAT instance tape from individual clauses. The declaration is a direct record structure whose width field is computed from the variable list length.
Claim. A structure for encoding one SAT clause in a cellular automaton, parameterized by the number of variables $n$, consisting of a list of indices from the set of $n$ variables, a matching list of negation flags, an integer starting position on the tape, and a width defaulting to $3k+2$ where $k$ is the length of the variable list.
background
The Cellular Automata module supplies local gadgets that simulate Boolean operations under deterministic, reversible update rules derived from Rule 110. ClauseGadget records the minimal data required to place a clause on the tape so that the subsequent encodeClause function can populate a Window of the computed width. The module imports ComputationBridge to connect these CA steps to Turing-machine simulations while preserving ledger compatibility.
proof idea
The declaration is a pure structure definition that directly records the four fields with the stated default for width. No lemmas or tactics are applied; it functions as a data carrier for the downstream encodeClause definition.
why it matters
ClauseGadget supplies the clause-level building block for SATGadget, which assembles a complete SAT instance for the CA-based solver. It advances the module's program of showing that SAT evaluation can be performed by a local 1D automaton whose computation time is claimed to be O(n^{1/3} log n), consistent with the Recognition Science ledger and forcing framework. The construction touches the open question of whether the balanced-parity readout cost remains linear despite the parallel CA evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.