DeterministicIsolation
plain-language theorem explainer
Deterministic isolation packages an explicit map from instance size n to a list of XOR systems that isolates every satisfiable CNF formula while keeping list length bounded by a polynomial in n. Complexity researchers working on explicit derandomization of SAT would cite the structure when packaging uniform constructions. The declaration is a plain structure definition assembling three fields with no additional proof obligations.
Claim. A deterministic isolation consists of a family map $H : nmapsto$ list of XOR systems on $n$ variables, constants $c,k$ such that the list length is at most $c n^k$ for every $n$, and the isolating property that every satisfiable CNF formula on $n$ variables is isolated by at least one system in the list (i.e., adjoining the XOR clauses leaves exactly one satisfying assignment).
background
XORFamily denotes the type of functions sending each natural number $n$ to a list of XOR systems on $n$ variables. IsolatingFamily applied to such a map asserts that for every satisfiable CNF formula on $n$ variables there exists at least one system $H$ in the list such that adjoining the XOR clauses to the CNF leaves exactly one satisfying assignment. The module develops tools for isolating families built from XOR constraints, with the goal of obtaining deterministic, polynomial-size families that work uniformly for all instances of a given size. The upstream definitions supply the basic notions of XOR families and the isolating property without any size bound.
proof idea
This declaration is a structure definition that directly records the three components: the family map, the polynomial-size witness, and the isolating property. No lemmas are applied; the structure simply packages the data.
why it matters
This structure captures the notion of an explicit, polynomial-size isolating family for SAT, as described in the module documentation. It provides a formal interface for deterministic constructions that could be used in proofs of derandomization or isolation lemmas within the Complexity.SAT hierarchy. No downstream uses are recorded yet, leaving open how it will be instantiated with concrete families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.