Satisfiable
plain-language theorem explainer
Satisfiability for a CNF formula over n variables is defined as the existence of a Boolean assignment that makes the full conjunction evaluate to true. Researchers working on SAT-to-J-cost encodings or BWD-3 linear feasibility reductions cite this predicate to connect classical satisfiability with Recognition Science cost functions. The definition is a direct existential statement over the Assignment type using the evalCNF aggregator.
Claim. A CNF formula $φ$ with $n$ variables is satisfiable when there exists an assignment $a$ from the $n$ variables to Boolean values such that the conjunction of all clause evaluations under $a$ equals true.
background
CNF is a structure holding a list of clauses over variables indexed by Fin n, with the empty list evaluating to true. Assignment is the type of total functions from these variables to Bool, and evalCNF computes the logical AND across clause results. The module sets variable indices explicitly as Fin n for finite problem size.
proof idea
One-line definition that directly introduces the Prop via existential quantification over Assignment n and the predicate evalCNF a φ = true. It depends on the upstream evalCNF aggregator and the two Assignment aliases.
why it matters
This predicate is the central interface for the SAT module. It appears in the sound field of BWD3Model, in satJCost_zero_iff from RSatEncoding, and in the classical decider theorems sat_decider_classical and satisfiable_iff_linearFeasible. It supplies the logical bridge from CNF satisfiability to linear feasibility and J-cost zero conditions inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.