XORFamily
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not construct any concrete list of XOR systems for any n.
- Does not prove that any family member isolates a given formula.
- Does not impose or verify a polynomial size bound on the lists.
- Does not connect the family to the cost function H or the phi-ladder.
formal statement (Lean)
10abbrev XORFamily := (n : Nat) → List (XORSystem n)
proof body
Definition body.
11
12/-- A system `H` isolates `φ` when `φ ∧ H` has exactly one satisfying assignment. -/