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

Constraint

show as:
view Lean formalization →

Constraint is an inductive type that packages either a CNF clause or an XOR parity check over n variables. Workers encoding mixed satisfiability instances for ledger balance or crystal symmetry checks cite it when assembling input sets or testing variable determination. The definition is introduced directly by two constructors with no auxiliary lemmas or reductions.

claimFor $n$ a natural number, a constraint is either a CNF clause $C$ (disjunction of literals) or an XOR constraint $X$ (parity condition on a subset of the variables).

background

The module Complexity.SAT.PC works with mixed CNF+XOR instances. Upstream, Clause from CNF is an abbreviation for a list of literals while the RSatEncoding version adds a size bound of at most three literals with signs. XORConstraint is a structure holding a list of variables and a target parity bit. These pieces are imported to support encodings that combine disjunctive clauses with parity checks, as required by downstream functions such as constraintsOf and determinesVar.

proof idea

The declaration is a direct inductive definition. It introduces the two constructors cnf and xor by pattern matching on the supplied Clause and XORConstraint values; no tactics, lemmas, or reductions are invoked.

why it matters in Recognition Science

Constraint supplies the common carrier type for the PC properties that appear in thirty downstream declarations. It is consumed by constraintsOf to build the full list of mixed constraints and by determinesVar to articulate forcing conditions. The same type surfaces in LedgerAlgebra.paired_preserves_balance and in CrystalSymmetry.LatticeParams, indicating its role in carrying constraint data into algebraic and geometric settings. It completes the unification step needed before PeelingData and PeelingWitness can be defined.

scope and limits

formal statement (Lean)

  10inductive Constraint (n : Nat) where
  11  | cnf (C : Clause n)
  12  | xor (X : XORConstraint n)
  13deriving Repr
  14
  15/-- Whether a variable is mentioned in a literal. -/

used by (30)

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

depends on (7)

Lean names referenced from this declaration's body.