hasCycle
The definition detects cycles in a stakeholder graph by returning true on any self-loop or any pair of distinct nodes that reach each other. Ethics modelers checking conflict-of-interest graphs would reference it to validate input structures before further analysis. The implementation is a direct disjunction of two list predicates, one for self-edges and one invoking mutual reachability on distinct pairs.
claimLet $G$ be a stakeholder graph with boolean edge relation $E$. For a finite list $N$ of stakeholders, the cycle indicator $C(G,N)$ is true if there exists $s$ in $N$ with $E(s,s)$, or if there exist distinct $s,t$ in $N$ such that $s$ reaches $t$ and $t$ reaches $s$.
background
Stakeholder is an abbreviation for the string type serving as a node label. A stakeholder graph is a structure whose only field is a boolean edge function between stakeholders, introduced for conflict-of-interest detection. mutualReachable is the conjunction of the two directed reachability checks between a pair of nodes restricted to the supplied list. The module supplies elementary graph predicates for ethics applications inside the Recognition Science development.
proof idea
The definition is a one-line boolean expression. It applies the any combinator once to test for a self-loop via the edge field, then applies any twice more to scan for any distinct pair satisfying the mutualReachable predicate.
why it matters in Recognition Science
The definition supplies the basic cycle test required for any conflict-of-interest analysis built on stakeholder graphs. No downstream theorems are recorded. It supplies a structural predicate that could later interface with uniqueness or fixed-point results from the forcing chain, though the ethics submodule remains isolated from the core T0-T8 landmarks at present.
scope and limits
- Does not compute transitive closure explicitly.
- Does not handle weighted or probabilistic edges.
- Does not accept infinite or non-list node collections.
- Does not certify acyclicity, only reports presence of a cycle.
formal statement (Lean)
35def hasCycle (G : StakeGraph) (nodes : List Stakeholder) : Bool :=
proof body
Definition body.
36 nodes.any (fun s => G.edge s s)
37 || nodes.any (fun s =>
38 nodes.any (fun t => (¬ decide (s = t)) && mutualReachable G nodes s t))
39
40end StakeGraph
41end Ethics
42end IndisputableMonolith
43