Stakeholder
plain-language theorem explainer
Stakeholder provides a string label for nodes in a conflict-of-interest graph. Modelers of stakeholder relations in the Ethics module cite it when building graphs that support reachability and cycle checks. The declaration is a direct type abbreviation with no further structure or computation.
Claim. Let Stakeholder denote the set of string labels $s$ used to identify participants in a directed graph whose edges record potential conflicts.
background
The Ethics.StakeGraph module supplies graph primitives for conflict-of-interest detection. Stakeholder acts as the node type inside the StakeGraph structure, whose sole field is an edge relation of type Stakeholder → Stakeholder → Bool. The module imports the 'for' structure from UniversalForcingSelfReference, which records structural properties required for meta-realization instances.
proof idea
One-line abbreviation that directly equates Stakeholder to the String type.
why it matters
The definition supplies the node type for every downstream operation in the module: contains, neighbors, reachable, mutualReachable, hasCycle, and the StakeGraph structure itself. It thereby supplies the concrete representation needed for COI detection while inheriting the meta-realization context recorded by the imported 'for' structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.