Var
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.