reachable
plain-language theorem explainer
Defines a boolean reachability check on a stakeholder graph by depth-first search over a supplied node list. Conflict-of-interest analysis and SAT completeness arguments cite this primitive for connectivity queries. The implementation uses a local recursive dfs that expands the frontier with unvisited neighbors until the target appears or the list empties.
Claim. Let $G$ be a directed graph on stakeholder labels whose edges are given by a boolean predicate. For a finite list of labels $nodes$ and two labels $src, dst$, the function returns true if and only if a directed path from $src$ to $dst$ exists whose intermediate vertices all lie in $nodes$.
background
Stakeholder is an alias for String used as a vertex label. StakeGraph is the structure whose sole field is the edge predicate Stakeholder → Stakeholder → Bool; the module deploys it for conflict-of-interest detection. The sibling definitions contains and neighbors supply list membership and out-neighbor extraction, respectively, both built from standard list combinators.
proof idea
The definition introduces an auxiliary recursive function dfs that takes a frontier list and a visited list. On each step it matches the head of the frontier: if the head equals the target it returns true; otherwise it computes the fresh unvisited neighbors of that vertex and recurses on the concatenated tail plus fresh neighbors, prepending the current vertex to the visited list. The top-level call seeds the frontier with the source and the visited list with empty.
why it matters
The definition supplies the connectivity test required by mutualReachable and by the PropagationGraph inductive construction used in SAT completeness lemmas. It also appears in generator-preservation arguments for finite lattice enumerations of virtues. Within the Recognition framework it furnishes the graph-theoretic substrate for ethical constraint propagation and consistency verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.