DeterministicIsolation
plain-language theorem explainer
An explicit uniformly constructible XOR family that isolates every satisfiable CNF formula while keeping list length polynomial in n is recorded by this structure. Complexity researchers studying derandomization or explicit constructions for SAT isolation would cite the definition. The structure is introduced directly as a record whose three fields package the family, the size bound, and the isolation property.
Claim. A deterministic isolation is a map $H : ℕ → List(XORSystem_n)$ equipped with constants $c,k ∈ ℕ$ such that $|H(n)| ≤ c n^k$ for all $n$, together with the property that for every satisfiable CNF formula $φ$ on $n$ variables there exists $H ∈ H(n)$ such that $φ ∧ H$ has exactly one satisfying assignment.
background
The module defines an XOR family as a map from instance size $n$ to a list of XOR systems. The isolating-family property states that for every satisfiable CNF $φ$, at least one member of the list isolates $φ$, meaning the conjunction has a unique satisfying assignment. Deterministic isolation strengthens the notion by requiring the family to be uniformly constructible with polynomial list length.
proof idea
The declaration is a structure definition with no proof body. Its three fields directly encode the required map, the polynomial-size witness, and the isolating-family predicate. No lemmas or tactics are applied.
why it matters
This definition supplies the target object for deterministic isolation results inside the SAT isolation module. It encodes the requirement of an explicit polynomial-size isolating family, matching the module doc-comment on XOR families for instances of size $n$. No downstream uses are recorded among the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.