pith. machine review for the scientific record. sign in
def definition def or abbrev high

IsolatingFamily

show as:
view Lean formalization →

An isolating family of XOR systems ensures that for any satisfiable CNF formula on n variables, at least one system in the family, when conjoined, leaves exactly one satisfying assignment. Complexity theorists studying deterministic SAT reductions would reference this definition when building explicit polynomial-size isolating families. The definition consists of a universal quantification over all satisfiable CNF instances requiring the existence of an isolating XOR system from the family.

claimLet $H$ be a family of XOR systems. Then $H$ is isolating if for every $n$ and every satisfiable CNF formula $phi$ on $n$ variables, there exists a system $H$ in the family at size $n$ such that $phi$ conjoined with that system has exactly one satisfying assignment.

background

An XOR family maps each natural number $n$ to a list of XOR systems on $n$ variables. The isolates predicate holds for a system and CNF formula when their conjunction admits exactly one satisfying assignment. Satisfiability of a CNF formula means there exists at least one assignment to its variables that evaluates every clause to true. The module develops XOR families for SAT instances of fixed size, building on the CNF structure and the isolates relation.

proof idea

This is the direct definition of the isolating property. It states that the family satisfies the universal property that every satisfiable CNF is isolated by some member of the family at the corresponding size.

why it matters in Recognition Science

This definition supplies the isolates_all field inside the DeterministicIsolation structure, which further requires the family to be of polynomial size. It completes the isolating condition in the SAT isolation module and supports deterministic reductions that avoid nondeterminism. In the Recognition Science framework the construction connects to the cost algebra where the shifted cost $H(x) = J(x) + 1$ converts the Recognition Composition Law into d'Alembert's equation.

scope and limits

formal statement (Lean)

  17def IsolatingFamily (𝓗 : XORFamily) : Prop :=

proof body

Definition body.

  18  ∀ {n} (φ : CNF n), Satisfiable φ → ∃ H ∈ 𝓗 n, isolates φ H
  19
  20/-- Deterministic isolation: an explicit, uniformly constructible `𝓗` with polynomial size. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.