XORFamily
plain-language theorem explainer
An XOR family is a map sending each natural number n to a list of XOR constraint systems on n variables. Researchers constructing deterministic isolating families for SAT instances in the Recognition Science framework cite this when assembling polynomial-size collections that enforce unique solutions. The declaration is a direct type abbreviation that composes the existing XORSystem definition with no added structure or computation.
Claim. An XOR family is a function assigning to each natural number $n$ a list of XOR constraint systems, where each system is a collection of parity constraints on $n$ Boolean variables.
background
In the Complexity.SAT.Isolation module an XORSystem is the type List (XORConstraint n), a collection of parity constraints. The isolates predicate declares that an XORSystem H isolates a CNF formula φ precisely when φ ∧ H possesses exactly one satisfying assignment. This setup draws on the cost algebra H, which satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) obtained by shifting the Recognition Composition Law.
proof idea
The declaration is a one-line abbreviation that directly equates XORFamily to the function type (n : Nat) → List (XORSystem n). It performs no computation and invokes no lemmas beyond the prior definition of XORSystem.
why it matters
XORFamily supplies the carrier type for both IsolatingFamily and the DeterministicIsolation structure, which together assert the existence of an explicit, polynomial-size family that isolates every satisfiable CNF instance. The construction advances the Recognition Science program by furnishing deterministic uniqueness mechanisms that parallel the J-uniqueness step (T5) of the forcing chain. It leaves open the concrete polynomial bound and the explicit construction of the family members.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.