geometric_isolation_enables_propagation_thm
plain-language theorem explainer
Geometric isolation of a satisfiable CNF formula by a linear-family XOR system implies the isolation invariant, conditional on the propagation hypothesis. Researchers studying backpropagation completeness for SAT instances would cite this when checking invariant preservation under geometric constraints. The proof is a one-line term application of the hypothesis to the satisfiability, isolation, and family-membership assumptions.
Claim. Let $n$ be a natural number, let $φ$ be a satisfiable CNF formula over $n$ variables, let $H$ be an XOR system that isolates $φ$ and belongs to the linear family on $n$ variables. If the geometric isolation enables propagation hypothesis holds for $φ$ and $H$, then the isolation invariant holds for $φ$ and $H$.
background
The module builds fully-determined backpropagation states from total assignments. CNF is the structure whose clauses field holds a list of clauses over $n$ variables, with Satisfiable asserting existence of a total assignment meeting every clause. XORSystem $n$ encodes a collection of linear constraints over GF(2). The isolates predicate requires that $H$ geometrically separates satisfying from unsatisfying assignments. The linearFamily $n$ collects those XOR systems whose constraint matrices are linear. Upstream, BPStep is the inductive relation whose constructors include xor_push for propagating values along XOR constraints.
proof idea
This is a term-mode one-line wrapper. It applies the hypothesis geometric_isolation_enables_propagation_hypothesis directly to the satisfiability witness hsat, the isolation predicate hiso, and the linear-family membership hgeo, yielding IsolationInvariant $n$ $φ$ $H$.
why it matters
The declaration would feed the polynomial_time_3sat_algorithm_hypothesis by closing the link from isolation to invariant preservation. The module comment falsifies the underlying hypothesis on three grounds: deterministic isolation cannot be derandomized without implying NP ⊆ P/poly, propagation stalls on expander-Tseitin formulas, and the claim relativizes while Baker-Gill-Solovay oracles separate P from NP. No direct connection to the T0-T8 forcing chain or phi-ladder appears in this submodule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.