pith. machine review for the scientific record. sign in
def definition def or abbrev high

contains

show as:
view Lean formalization →

Defines list membership for stakeholder identifiers in conflict graphs. Modelers of ethical constraints in multi-agent systems reference it for basic containment checks during graph traversal. The implementation delegates to List.any with a decidable equality test on strings.

claimFor a list $xs$ of stakeholder labels and a stakeholder $s$, contains$(xs, s)$ returns true precisely when $s$ appears in $xs$.

background

The StakeGraph module models stakeholder relationships for conflict-of-interest detection, where each Stakeholder is a String label. This contains definition provides the primitive membership test on lists of such labels. It parallels the interval containment predicate from Numerics.Interval.Basic, which checks whether a real lies between lo and hi bounds, but here the domain is discrete string equality.

proof idea

One-line definition that applies List.any to the input list, using decide on structural equality to return a Bool.

why it matters in Recognition Science

This membership test underpins the reachable definition in the same module, which implements depth-first search for stakeholder connectivity. It appears in downstream results for cellular automata runtime hypotheses, J-cost calculations in complexity, and vertex cover instances, indicating its role in propagating ethical constraints across formal models. In the Recognition framework it supports the ethics layer that interfaces with complexity and cosmology pipelines.

scope and limits

Lean usage

def test : Bool := contains [``Alice``, ``Bob``] ``Alice``

formal statement (Lean)

  15def contains (xs : List Stakeholder) (s : Stakeholder) : Bool :=

proof body

Definition body.

  16  xs.any (fun x => decide (x = s))
  17

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.