CNFFormula
plain-language theorem explainer
CNFFormula encodes a k-CNF instance as a list of clauses over n variables together with an explicit cardinality witness. Researchers formalizing recognition-based SAT complexity cite this structure when analyzing J-cost landscapes under the R̂ operator. The declaration is a direct structure with three fields that mirrors the standard mathematical object without additional proof obligations.
Claim. A $k$-CNF formula over $n$ variables consists of a list of clauses, where each clause is a list of at most three signed literals drawn from indices in $[n]$, together with a natural number var_count satisfying var_count = $n$.
background
The R̂ SAT Encoding module studies how the Recognition Science operator R̂ supplies a non-natural polytime certifier for SAT: satisfiable instances reach zero J-cost in O(n) steps while unsatisfiable instances carry a positive Betti-1 obstruction. Clause is defined as a structure whose literals field is a list of pairs (Fin n × Bool) with length at most 3. Assignment is the type Fin n → Bool that supplies the evaluation map used in downstream satisfiability checks. The module sits inside the forcing chain T0–T8 and imports LedgerForcing to connect clause lists to J-cost and defect measures.
proof idea
CNFFormula is introduced by a structure declaration whose three fields directly record the clause list, the variable count, and the equality proof var_count_eq. No tactics or lemmas are applied; the definition serves as the concrete carrier type for all subsequent J-cost and moat constructions.
why it matters
This structure supplies the input type for CircuitSeparation, which proves R̂ reaches zero cost in ≤ n steps precisely when the formula is satisfiable, and for DefectMoat, which returns 0 exactly on satisfiable instances. It fills the encoding step in the module's core claim that recognition-time complexity separates from Turing time for SAT, supporting the partial theorem status by providing the object on which J-cost and topological obstructions are defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.