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

Var

show as:
view Lean formalization →

Var n is the type of variable indices for an n-variable SAT instance, identified with the finite set Fin n. Formalizers of SAT solvers and backpropagation relations cite this when building literals, clauses, and partial assignments. The declaration is a direct one-line abbreviation to Mathlib's Fin n.

claimFor a conjunctive normal form instance with $n$ variables, the set of variable indices is the finite set $Fin(n)$.

background

This abbrev sits in the CNF module of the Complexity.SAT component, which imports Mathlib and supplies the basic types for SAT encoding. Sibling declarations include Lit, Clause, CNF, Assignment, evalLit, evalClause, and Satisfiable, all of which are indexed by the same n. No upstream lemmas are required; the type simply re-exports the standard finite set so that downstream functions such as PartialAssignment and setVar can treat variables uniformly as elements of Fin n.

proof idea

One-line abbreviation that directly equates Var n to Fin n.

why it matters in Recognition Science

The declaration supplies the indexing type used by 39 downstream declarations, including the inductive BPStep relation, clauseUnit, compatible_setVar, and clauseUnit_correct. It anchors the SAT backpropagation machinery inside the monolith, allowing guarded update rules and compatibility checks to be stated over a concrete finite domain. No direct link to the T0-T8 forcing chain or RCL appears here; the type instead supports the complexity-analysis layer that sits alongside the core Recognition Science derivations.

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