Assignment
plain-language theorem explainer
An assignment for n variables is a map from Fin n to Bool. Researchers modeling SAT formulas and circuit evaluation in the Recognition framework cite this to supply the domain for satisfiability checks and J-cost calculations. The declaration is a direct abbreviation with no proof obligations.
Claim. For $n : Nat$, an assignment is any function from the finite set of $n$ variable indices to the Boolean values.
background
Variable indices are modeled as Fin n in this module. The sibling abbrev Var n expands to Fin n and supplies the domain. The upstream RSatEncoding module defines an analogous Assignment n as Fin n → Bool, which this local version mirrors for CNF formulas and their evaluation functions.
proof idea
Direct abbreviation that expands Assignment n to the function type Var n → Bool.
why it matters
This supplies the domain type used in 40 downstream declarations, including BooleanCircuitWithEval (which bundles eval : Assignment n → Bool) and moat_width_unsat (which quantifies J-cost over all assignments). It supports the circuit separation claim by enabling statements about zero-cost assignments for SAT formulas and positive lower bounds for UNSAT formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.