isolates
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.
claimLet φ 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 in Recognition Science
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.
scope and limits
- Does not assert existence of an isolating H for arbitrary φ.
- Does not specify how to construct or select such an H.
- Does not address the computational cost of verifying isolation.
- Does not extend to non-XOR constraint systems.
formal statement (Lean)
13def isolates {n} (φ : CNF n) (H : XORSystem n) : Prop :=
proof body
Definition body.
14 UniqueSolutionXOR { φ := φ, H := H }
15
16/-- A family `𝓗` is isolating if for every satisfiable `φ`, some `H ∈ 𝓗 n` isolates `φ`. -/
used by (17)
-
geometric_isolation_enables_propagation_hypothesis -
geometric_isolation_enables_propagation_thm -
IsolatingFamily -
XORFamily -
log_aczel_data_of_laws -
dirichlet_form_eq_neg_quadratic -
frc_holds_on_RS_lattice_exists -
of_u4 -
U4BandBudgetControlledByInjectionRateHypothesis -
ProjectedPDEPairingHypothesisAt -
defect_topological_floor_unbounded -
realizedDefectCostBounded_of_charge_zero_and_excessBounded -
regularTail -
honestPhaseFamily_excess_bounded -
zeroInducedBridge_of_rh -
zetaFromThetaPhase4Cert -
unified_rh_cert_of_bridge