isolates
plain-language theorem explainer
A CNF formula φ paired with an XOR constraint list H isolates when their conjunction admits exactly one satisfying assignment. Researchers analyzing deterministic SAT completeness via isolating families would cite this predicate to express the uniqueness condition. The definition is realized as a direct wrapper around the unique-solution predicate on the augmented system.
Claim. For a CNF formula $φ$ over $n$ variables and a list $H$ of XOR constraints on the same variables, the isolation property holds if and only if there exists a unique assignment satisfying both $φ$ and every constraint in $H$.
background
CNF is the structure consisting of a list of clauses over a fixed number of variables. XORSystem is an abbreviation for a list of parity (XOR) constraints on $n$ variables. UniqueSolutionXOR asserts existence of a unique assignment that satisfies the CNF and all constraints in the XOR list simultaneously.
proof idea
The definition is a one-line wrapper that applies UniqueSolutionXOR to the combined record of φ and H.
why it matters
This predicate supplies the core isolation condition used by IsolatingFamily to require that every satisfiable CNF possesses some H from the family that isolates it. It is invoked directly by the geometric isolation hypothesis and its associated theorem in the Completeness module (the hypothesis was later falsified). In the Recognition framework the definition supports deterministic isolation constructions inside the SAT complexity analysis, independent of the T0-T8 forcing chain and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.