Clause
plain-language theorem explainer
Clause n is the type alias for lists of literals over n variables in the SAT encoding. Complexity researchers building gadget reductions or ledger representations cite it when assembling CNF formulas for J-cost calculations. The declaration is a direct one-line type abbreviation with no further content.
Claim. A clause on $n$ variables is a finite list of literals, where each literal is either a positive or negative occurrence of a variable drawn from the finite set of size $n$.
background
Variable indices are taken from Fin n. The sibling Lit inductive type supplies the two constructors for positive and negative literals. The CNF structure then assembles lists of these clauses into a full formula. Upstream imports from ledger factorization and phi-forcing supply the surrounding J-cost and defect-distance machinery that later operate on these clauses.
proof idea
The declaration is a one-line type abbreviation that directly aliases List (Lit n).
why it matters
This supplies the basic clause type used by SATGadget, SATLedger, and the JCostLaplacian results on clause invariance under flips. It forms the entry point for encoding Boolean problems into the Recognition ledger and supports the bridge from SAT to cellular-automaton and complexity structures. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.