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

Assignment

show as:
view Lean formalization →

An assignment for n variables is a map from Fin n to Bool that evaluates literals and clauses in the R̂ SAT model. Researchers studying recognition-time complexity of SAT cite it when constructing J-cost landscapes or circuit separation claims. The definition is a direct type abbreviation that enables all downstream satisfiedBy predicates and cost functions without further proof.

claimFor positive integer $n$, an assignment is any function $a : [n] → {true, false}$ that assigns a truth value to each of the $n$ variables.

background

The R̂ SAT Encoding module models SAT via the Recognition operator R̂, which reaches zero J-cost for satisfiable k-CNF instances in O(n) steps while UNSAT instances exhibit a topological obstruction. J-cost of a formula under an assignment equals the number of unsatisfied clauses and is zero precisely on satisfying assignments. The module imports SAT.CNF, LedgerForcing, and Constants; upstream results include the active-edge count A from IntegrationGap and Masses.Anchor together with the similar Assignment type in SAT.CNF.

proof idea

The declaration is a one-line type abbreviation that identifies Assignment n with the function space Fin n → Bool. It directly supports the subsequent Literal.satisfiedBy, Clause.satisfiedBy, and CNFFormula.satisfiedBy definitions that appear in the same file.

why it matters in Recognition Science

This type supplies the domain for every satisfiability predicate and J-cost function in the module, feeding directly into CircuitSeparation (which proves R̂ reaches zero cost in ≤ n steps for SAT formulas) and CircuitLedgerCert (which bundles the moat-width and capacity bounds). It realizes the foundational object in the module's partial theorem that recognition-time complexity separates from Turing time, while leaving open the informal link to natural-proof barriers.

scope and limits

formal statement (Lean)

  54def Assignment (n : ℕ) := Fin n → Bool

proof body

Definition body.

  55
  56/-- A literal is satisfied by an assignment. -/
  57def Literal.satisfiedBy {n : ℕ} (lit : Fin n × Bool) (a : Assignment n) : Bool :=
  58  if lit.2 then a lit.1 else !a lit.1
  59
  60/-- A clause is satisfied if at least one literal is satisfied. -/
  61def Clause.satisfiedBy {n : ℕ} (c : Clause n) (a : Assignment n) : Bool :=
  62  c.literals.any (fun lit => Literal.satisfiedBy lit a)
  63
  64/-- A CNF formula is satisfied if all clauses are satisfied. -/
  65def CNFFormula.satisfiedBy {n : ℕ} (f : CNFFormula n) (a : Assignment n) : Bool :=
  66  f.clauses.all (fun c => c.satisfiedBy a)
  67
  68/-- A formula is satisfiable if there exists a satisfying assignment. -/
  69def CNFFormula.isSAT {n : ℕ} (f : CNFFormula n) : Prop :=
  70  ∃ a : Assignment n, f.satisfiedBy a = true
  71
  72/-- A formula is UNSAT if no assignment satisfies it. -/
  73def CNFFormula.isUNSAT {n : ℕ} (f : CNFFormula n) : Prop :=
  74  ∀ a : Assignment n, f.satisfiedBy a = false
  75
  76/-! ## J-Cost Landscape for SAT -/
  77
  78/-- The J-cost of a formula under an assignment.
  79    J = 0 iff all clauses are satisfied (zero defect = satisfying assignment).
  80    J = (number of unsatisfied clauses) > 0 iff UNSAT under this assignment. -/

used by (40)

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

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.