DeterministicIsolation
DeterministicIsolation packages an explicit XOR family that isolates every satisfiable CNF formula while obeying a uniform polynomial size bound. Complexity researchers working on derandomization of SAT would cite the structure when they need a concrete, uniformly constructible isolating family. The definition is a direct structure bundling the family, an existential size witness, and the isolating property with no further proof obligations.
claimA deterministic isolation consists of an XOR family $H : Nat → List(XORSystem)$ together with constants $c,k ∈ Nat$ such that $|H(n)| ≤ c n^k$ for all $n$, and the family satisfies the isolating property: for every satisfiable CNF formula $φ$ on $n$ variables there exists $H ∈ H(n)$ such that $φ ∧ H$ has exactly one satisfying assignment.
background
XORFamily is the abbreviation for a map sending each natural number $n$ to a list of XOR systems on $n$ variables. IsolatingFamily is the predicate asserting that for every satisfiable CNF formula $φ$ some member of the list isolates $φ$, meaning the conjunction has a unique satisfying assignment. The module supplies the local setting of XOR families for instances of size $n$, importing the CNF and XOR modules to define the basic objects.
proof idea
This is a structure definition with three fields and no proof body. The first field holds the family, the second supplies an existential witness for the polynomial size bound, and the third asserts the isolating property directly from the referenced IsolatingFamily definition.
why it matters in Recognition Science
The structure supplies the target notion of deterministic isolation referenced in the module doc-comment. It provides the explicit, polynomial-size object needed for further complexity arguments inside the SAT isolation development. No downstream uses are recorded, so its integration with larger Recognition Science results remains open.
scope and limits
- Does not construct any concrete family.
- Does not prove existence of such a family.
- Does not bound the constants $c$ or $k$.
- Does not connect to specific algorithms or solvers.
formal statement (Lean)
21structure DeterministicIsolation where
22 𝓗 : XORFamily
23 polySize : ∃ c k : Nat, ∀ n, (𝓗 n).length ≤ c * n^k
24 isolates_all : IsolatingFamily 𝓗
25
26end SAT
27end Complexity
28end IndisputableMonolith