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

Var

show as:
view Lean formalization →

Variable indices for SAT instances with n variables are formalized as the finite set of size n. Researchers formalizing SAT solvers, unit propagation, or backpropagation algorithms in the Recognition framework cite this when defining assignments and constraints. The declaration is a direct type abbreviation to the standard finite set with no additional obligations.

claimFor a natural number $n$, the set of variable indices is the finite set $Fin(n) = {0, 1, ..., n-1}$.

background

The CNF module encodes SAT problems over a fixed number of variables. Variables receive indices from this finite set, which then parametrizes literals, clauses, partial assignments, and evaluation functions. The module imports Mathlib to access the standard finite type construction.

proof idea

Direct abbreviation to the standard finite type Fin n from the library, with no lemmas or tactics required.

why it matters in Recognition Science

This indexing underpins all downstream SAT constructions, including the inductive BPStep relation for backpropagation steps and the clauseUnit function for detecting unit clauses. It supports proved results such as clauseUnit_correct, which verifies that unit propagation returns the correct value under a satisfying assignment. The definition anchors the complexity formalization that feeds into broader Recognition Science claims about computational structure.

scope and limits

formal statement (Lean)

   8abbrev Var (n : Nat) := Fin n

proof body

Definition body.

   9
  10/-- Literals over `n` variables. -/

used by (39)

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

… and 9 more