geometric_isolation_enables_propagation_hypothesis
plain-language theorem explainer
The definition encodes the hypothesis that satisfiability of a CNF formula together with isolation by a linear-family XOR system implies the isolation invariant. Researchers in proof complexity would cite it when attempting to connect geometric isolation to backpropagation completeness. The definition is a direct Prop encoding that stands falsified by Tseitin formulas on expander graphs where the noStalls condition fails.
Claim. For a CNF formula $φ$ on $n$ variables and an XOR system $H$, if $φ$ is satisfiable, $H$ isolates $φ$, and $H$ belongs to the linear family, then the isolation invariant holds: at least one unit XOR constraint exists, the propagation graph is connected, and no stall configurations occur.
background
The module builds fully-determined backpropagation states from total assignments. IsolationInvariant is the structure requiring hasUnits (a unit XOR constraint from $H$), connected (the propagation graph reaches all variables from initial units), and noStalls (BPStep always advances an incomplete state). The isolates predicate asserts that $φ$ conjoined with $H$ has a unique solution. The linearFamily enumerates small-bias XOR systems via mask-parity pairs up to $(n+1)^2$ pairs. Upstream, Satisfiable is the existence of an assignment evaluating the CNF to true.
proof idea
The declaration is a definition that directly assembles the implication from satisfiability, isolation, and linear-family membership to the isolation invariant as a Prop.
why it matters
It is applied in the theorem geometric_isolation_enables_propagation_thm to conclude the isolation invariant from the three assumptions. The original intent was to support the geometric propagation theorem in the SAT completeness argument. The doc-comment records its falsification on 2026-04-07 via counterexamples from Ben-Sasson and Wigderson on expander Tseitin formulas, where noStalls cannot hold because local propagation stalls on incomplete states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.