isolates
plain-language theorem explainer
The definition isolates(φ, H) asserts that the conjunction of a CNF formula φ and an XOR constraint system H has exactly one satisfying assignment. Complexity theorists studying SAT propagation and isolation in the Recognition Science framework would cite this predicate when analyzing uniqueness properties in hybrid constraint systems. The definition is realized as a direct wrapper around the UniqueSolutionXOR predicate from the XOR module.
Claim. Let φ be a CNF formula on n variables and H an XOR system on the same variables. The predicate isolates(φ, H) holds precisely when there is a unique assignment satisfying both φ and all constraints in H.
background
In this module an XOR family provides, for each instance size n, a list of possible XOR systems. A CNF is a conjunction of clauses over n variables. An XORSystem is a list of XOR constraints, each specifying the parity of a subset of variables. The predicate isolates is defined in terms of UniqueSolutionXOR, which states that exactly one assignment satisfies the combined CNF and XOR system. This builds on the cost algebra H, reparametrized as H(x) = J(x) + 1, though here H denotes the constraint system rather than the cost function.
proof idea
The definition is a one-line wrapper that directly invokes UniqueSolutionXOR on the structure combining the input CNF formula φ and the XOR system H.
why it matters
This definition underpins the IsolatingFamily predicate, which requires that for every satisfiable φ there exists some H in the family that isolates it. It is invoked in the geometric_isolation_enables_propagation_hypothesis and theorem in the Completeness module. Within Recognition Science it supports the analysis of deterministic isolation as a step toward completeness results, linking to the uniqueness properties arising from the J-functional equation, though the downstream propagation hypothesis was later falsified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.