pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CNF

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  20structure CNF (n : Nat) where
  21  clauses : List (Clause n)
  22deriving Repr
  23
  24/-- Total assignments for `n` variables. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.