StakeGraph
plain-language theorem explainer
StakeGraph supplies a directed graph structure on stakeholder labels to enable conflict-of-interest detection. Ethics and governance formalizations cite it when encoding dependency relations among parties. The declaration is a direct structure definition consisting of a single Boolean edge field.
Claim. A stakeholder graph consists of a binary relation $E : S → S → Bool$, where $S$ is the type of stakeholder labels.
background
Stakeholder is an abbreviation for the String type and functions as a label for any interested party. The module introduces StakeGraph to represent directed graphs used in COI detection. The sole upstream dependency is the Stakeholder abbreviation, which supplies the node type for the edge predicate.
proof idea
The declaration is a direct structure definition introducing the single edge field. No lemmas or tactics are applied.
why it matters
StakeGraph serves as the foundational type for the ethics module. It is used by the downstream definitions hasCycle, mutualReachable, neighbors, and reachable to implement graph traversal and cycle detection on stakeholder relations. The structure thereby supplies the data model required for formal COI checks within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.