CNF
plain-language theorem explainer
CNF packages a list of clauses into a single object indexed by the number of variables n. Researchers formalizing SAT instances or backpropagation procedures cite it as the input type for satisfiability and consistency checks. The definition is a direct structure declaration whose single field receives the Repr derivation automatically.
Claim. A CNF formula on $n$ variables is a list of clauses, where each clause is a disjunction of literals over the $n$ variables.
background
Variable indices are elements of Fin n. The sibling Clause is the abbreviation List (Lit n), which stands for a disjunction of literals. The upstream RSatEncoding.Clause supplies a concrete 3-SAT variant whose literals field is a list of at most three signed indices with an explicit size_bound proof. The module setting therefore treats CNF as the unrestricted conjunction of such disjunctions.
proof idea
The structure is introduced directly by the single field clauses : List (Clause n) together with the deriving Repr clause; no tactics or lemmas are applied.
why it matters
CNF supplies the core data type consumed by BackpropSucceeds, BPStep, bp_step_sound and the surrounding backpropagation lemmas. It therefore sits at the interface between the SAT encoding layer and the consistency arguments that feed the larger Recognition Science development. The definition closes the syntactic side of the complexity encoding before any semantic evaluation or forcing-chain properties are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.