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

Assignment

show as:
view Lean formalization →

An assignment on n variables is a function from Fin n to Bool. Researchers analyzing the Recognition Science SAT encoding cite this when constructing the J-cost landscape and satisfaction predicates for CNF formulas. The definition is a direct type alias that enables the module's downstream results on polytime recognition for satisfiable instances.

claimAn assignment for $n$ variables is a function $a : {0,1,2,…,n-1} → {true,false}$.

background

The RS SAT encoding module defines assignments to represent Boolean valuations over n variables in CNF formulas. This supports the J-cost landscape where cost equals the number of unsatisfied clauses and reaches zero exactly on satisfying assignments. The local setting is the partial theorem that R̂ supplies a non-natural O(n)-step certifier for SAT, separating recognition time from Turing time. Upstream, the CNF module supplies a parallel Assignment as Var n → Bool, while LedgerForcing and IntegrationGap supply the active-edge and forcing machinery that the J-cost construction later invokes.

proof idea

The declaration is a direct type definition with no further computation or proof obligations.

why it matters in Recognition Science

This definition is the domain type for all downstream CircuitLedger results, including BooleanCircuitWithEval, CircuitDecides, CircuitSeparation, and moat_width_unsat. It supplies the concrete objects needed for the module's core claim that R̂ reaches zero J-cost in ≤ n steps on SAT formulas while UNSAT formulas retain a positive defect moat. The placement anchors the Recognition Science separation of recognition-time complexity from circuit complexity.

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.