mutualReachable
plain-language theorem explainer
mutualReachable returns true precisely when two stakeholders can reach each other inside a supplied node list. It is invoked by cycle-detection code in the ethics layer for conflict-of-interest checks. The definition is a direct conjunction of the module's forward and reverse reachability tests.
Claim. In a graph whose edges are given by a Boolean predicate on string-labeled nodes, for stakeholders $s$ and $t$ drawn from a list $nodes$, bidirectional reachability holds if and only if a directed path exists from $s$ to $t$ and from $t$ to $s$ within the subgraph induced by $nodes$.
background
Stakeholder is a type alias for strings used as node labels. The graph structure stores a single Boolean edge predicate on pairs of these labels. Reachability is implemented by a recursive depth-first search that traverses only the nodes appearing in the supplied list.
proof idea
It is a one-line wrapper that applies the reachable predicate once in each direction and returns the conjunction of the two Boolean results.
why it matters
The predicate is used inside hasCycle to flag cycles via mutual reachability between distinct stakeholders (or via self-loops). It supplies a basic graph primitive for the ethics module's conflict-of-interest detection. The module lies outside the T0-T8 forcing chain and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.