Clause
plain-language theorem explainer
The Clause structure encodes each 3-SAT clause as a list of at most three signed variable indices over n variables. Researchers analyzing recognition-time SAT bounds or building J-cost arguments cite it when forming CNFFormula or SATLedger instances. The definition is a direct structure that pairs a literal list with an explicit length invariant.
Claim. A clause over $n$ variables is a list of pairs $(i,b)$ with $i$ a variable index in $0..n-1$ and $b$ a Boolean polarity, satisfying length at most 3.
background
The module encodes SAT instances for the Recognition Science operator R̂, which supplies a global, non-local certifier whose J-cost reaches zero in linear steps on satisfiable formulas. Clause sits inside this encoding and relies on the sibling Assignment type (Fin n → Bool) together with the Literal.satisfiedBy predicate that evaluates a signed index under an assignment. The local setting is the partial theorem that separates recognition-time complexity from Turing time: satisfiable instances admit O(n) zero-cost paths while unsatisfiable ones carry a Betti-1 obstruction.
proof idea
Direct structure definition that introduces the literals field and attaches the length invariant as a field; no tactics or lemmas are applied.
why it matters
Clause supplies the atomic unit for CNFFormula and SATLedger, which in turn support the constructive zero-cost theorem for satisfiable instances and the topological-obstruction theorem for unsatisfiable ones. It therefore occupies the encoding layer of the module's partial theorem on recognition-time versus Turing complexity. The definition also feeds downstream J-cost Laplacian results that track clause invariance under bit flips.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.