neighbors
plain-language theorem explainer
neighbors extracts the direct connections from a stakeholder s within a supplied list of nodes using the edge predicate of a StakeGraph. It is referenced in constructions of bounded step relations for causal cones. The implementation consists of a single List.filter application on the edge condition.
Claim. Let $G$ be a stakeholder graph with edge relation $e$. For list $N$ and stakeholder $s$, the neighbors are the sublist of $N$ consisting of those $t$ such that $e(s,t)$ holds.
background
Stakeholder is an abbreviation for String, serving as a label for participants. StakeGraph is the structure whose sole field is the edge predicate mapping pairs of stakeholders to Bool, supplied for conflict-of-interest detection. The module provides elementary graph operations on these labels. Upstream results include several definitions of the constant G, but they are unrelated to the graph primitives.
proof idea
One-line wrapper that applies List.filter to the predicate fun t => G.edge s t.
why it matters
Supplies the neighbor extraction primitive required by the BoundedStep class, which supports cardinality bounds on forward cones such as card_ballFS_succ_le and card_bind_neighbors_le. It connects the ethics module to causality constructions. No direct link to the T0-T8 chain or RCL appears, yet it enables concrete finite models for step relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.