Reachable
plain-language theorem explainer
The declaration defines an inductive predicate capturing which variables can be reached from an initial set by following directed edges in a propagation graph on n variables. Researchers proving completeness of backpropagation or isolation-based SAT solvers cite this construction to establish that every variable is determined. The definition is given directly by two constructors that encode the base case and the inductive closure along edges.
Claim. Let $G$ be a propagation graph whose edges relate variables in the finite set $V = {0,…,n-1}$. For an initial set $I ⊆ V$, the predicate $R(v)$ holds precisely when $v ∈ I$ or there exists a reachable $u$ such that $G$ contains the edge $u → v$.
background
The module constructs fully-determined backpropagation states from total assignments. A PropagationGraph is the structure whose sole field is a binary relation edges : Var n → Var n → Prop; an edge from v₁ to v₂ records that fixing v₁ forces the value of v₂. Variables are simply Fin n. The inductive predicate is introduced to guarantee that reachability is well-founded and therefore terminates when used to propagate values.
proof idea
The declaration is an inductive definition. The base constructor directly asserts membership in the supplied initial set. The step constructor closes under the edge relation of the propagation graph. No external lemmas are invoked; the two constructors alone generate the transitive closure starting from init.
why it matters
Reachable supplies the inductive core of AllReachable, the invariant that every variable is reachable from the initial units. This invariant is the combinatorial guarantee promised by the geometric-isolation construction in the same module and is invoked by the hypothesis that isolation enables complete propagation. The construction therefore sits inside the track that aims at a polynomial-time 3SAT algorithm.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.