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

Assignment

show as:
view Lean formalization →

The type of total assignments for n variables is the set of all functions from the finite index set to Boolean values. Complexity theorists working on SAT reductions and circuit simulations cite this definition to parameterize the evaluation of formulas and the computation of J-costs. It is introduced as a direct abbreviation over the variable index type.

claimFor a positive integer $n$, an assignment is any function $a : {0,1,…,n-1} → {true, false}$.

background

Variable indices are represented by the finite set Fin n. The module defines the index type as Fin n. An upstream result in the RSatEncoding module establishes the same convention for Boolean functions on variables, quoted as 'An assignment is a Boolean function on variables.' This supplies the domain for literal and clause evaluation in the CNF setting.

proof idea

The declaration is a one-line abbreviation that reuses the Var index abbreviation and the standard function type to Bool.

why it matters in Recognition Science

It serves as the input domain for all downstream SAT decision procedures and circuit evaluations. Parent results include BooleanCircuitWithEval which extends circuits with an eval field of this type, and theorems such as moat_width_unsat that quantify J-cost over all such assignments. It closes the interface between the Recognition forcing chain and concrete complexity bounds by providing the space on which defect distances are computed.

scope and limits

formal statement (Lean)

  25abbrev Assignment (n : Nat) := Var n → Bool

proof body

Definition body.

  26
  27/-- Evaluate a literal under an assignment. -/

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.