SATGadget
plain-language theorem explainer
The SAT gadget structure assembles a complete SAT instance into a one-dimensional cellular automaton tape using n variables, m clauses each as a local gadget, variable positions, an output cell, and total width n plus three times m plus ten. Complexity researchers examining sub-linear SAT evaluation in the Recognition Science model would reference this encoding when studying parallel propagation bounds. The definition is a direct record construction that bundles the clause gadgets and positions without additional computation.
Claim. A SAT instance encoded as a cellular automaton tape consists of natural numbers $n$ and $m$, a list of clause gadgets each depending on $n$, a function from the first $n$ naturals to integers giving variable positions on the tape, an integer output cell position, and total tape width $n + 3m + 10$.
background
The module supplies cellular automata infrastructure for encoding SAT instances to address P versus NP questions inside the Recognition Science framework. A clause gadget encodes one SAT clause as CA cells, recording the list of variable indices, negation flags, starting tape position, and gadget width equal to three times the number of literals plus two. This rests on clause structures from SAT encodings, where a clause is a list of at most three literals each carrying a variable index and sign.
proof idea
The declaration is a structure definition that directly lists its six fields and supplies a default value for total width. No lemmas are invoked and no tactics are used; the construction simply assembles the supplied clause gadgets, positions, and output cell into a single tape configuration object.
why it matters
This structure supplies the input type for the downstream hypothesis asserting SAT evaluation via cellular automata in time O(n to the one-third times log n). It supplies the concrete data representation needed for the module's claim that local rules on a 1D tape achieve parallel speedup while result extraction still costs linear queries. The encoding supports the broader argument that CA gadgets remain local, deterministic, and reversible for ledger compatibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.