XORConstraint
plain-language theorem explainer
XORConstraint n is a record pairing a list of variable indices from Fin n with a target Boolean parity, encoding a single linear equation over GF(2). Researchers constructing SAT solvers or backpropagation algorithms inside the Recognition Science complexity layer cite this structure when assembling parity systems for propagation or geometric families. The declaration is a bare structure definition carrying only the two fields and a Repr instance.
Claim. An XOR constraint over $n$ variables consists of a list $vars$ of elements from $Fin n$ together with a target parity $parity : Bool$, requiring that the XOR of the assigned values on those variables equals the given parity.
background
The Complexity.SAT.XOR module supplies data types for parity-augmented SAT problems and imports the Var abbreviation (Fin n) from the CNF layer together with Mathlib. Upstream structures include the nuclear-density tiers from NucleosynthesisTiers (quantities on discrete phi-powers) and the J-cost structure from PhiForcingDerived, which embed the combinatorial objects into the broader Recognition Science ledger. The immediate local setting is the representation of linear dependencies over GF(2) that appear when modeling information flow or constraint propagation in discrete physical systems.
proof idea
The declaration is a structure definition that directly introduces the fields vars : List (Var n) and parity : Bool with Repr derivation. No lemmas or tactics are applied; the type constructor is available for immediate use in downstream inductive relations.
why it matters
XORConstraint supplies the data type consumed by the BPStep inductive relation and the xorMissing function in the Backprop module, as well as by octantConstraint in GeoFamily. It thereby enables the encoding of parity constraints that arise in the Recognition Science treatment of complexity, linking to the eight-tick octave (T7) and dimensional forcing (T8) through the SAT infrastructure. The structure fills the interface between raw CNF clauses and parity-aware propagation steps without closing any open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.