AllReachable
plain-language theorem explainer
AllReachable defines the property that every variable is reachable from an initial set of units in a propagation graph. Researchers establishing connectivity for SAT backpropagation completeness cite it when constructing isolation invariants. The definition is a direct universal quantification over the inductive Reachable relation on graph edges.
Claim. Let $G$ be a propagation graph on $n$ variables with edges forming a binary relation on variables, and let $init$ be an initial set of variables. Then AllReachable$(G, init)$ holds if and only if every variable $v$ is reachable from $init$ via the transitive closure of the edges.
background
PropagationGraph is a structure whose sole field is the relation edges : Var n → Var n → Prop, where an edge indicates that determining one variable forces another. Reachable is the inductive predicate capturing the transitive closure starting from the initial set, defined to guarantee termination. The module builds fully-determined backpropagation states from total assignments over CNF and XOR systems. Upstream, BPStep supplies the guarded single-step rules for propagation, while IsolationInvariant requires existence of a connected graph satisfying AllReachable.
proof idea
One-line definition that directly sets AllReachable to the universal quantification ∀ v, Reachable G init v over the inductive Reachable predicate.
why it matters
AllReachable supplies the connectivity clause inside the connected field of IsolationInvariant, which encodes the geometric isolation guarantees for Track A. It is referenced by BackpropCompleteUnderInvariant and the polynomial_time_3sat_algorithm_hypothesis. The construction supports algebraic propagation tools in the Recognition Science framework, though the module notes that the accompanying noStalls condition is unsatisfiable for Tseitin formulas on expander graphs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.