Choice Sets (OR / Mutual Exclusivity)

@cite{hudson-2010} §3.3

OR-links partition values into mutually exclusive alternatives. The schematic example: male --or--> gender, female --or--> gender says that male and female are alternative values along the gender dimension.

Future work: this should be reframed as a Setoid/Partition quotient structure (see project_inheritance_consolidation.md). The current LinkKind.or case stores choice membership as a relation in the link list; a partition-class representation would make exhaustivity and disjointness definitional rather than provable.

def Core.Inheritance.choiceSet {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node : α) : List α

OR-alternatives of a node (§3.3): mutually exclusive choices. E.g., choiceSet net gender returns [male, female] if the network contains male --or--> gender and female --or--> gender.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Inheritance.mem_choiceSet_iff {α R : Type} [DecidableEq α] [DecidableEq R] (net : Network α R) (node a : α) : a ∈ choiceSet net node ↔ ∃ (label : Option R), { kind := LinkKind.or, source := a, target := node, label := label } ∈ net.links

Membership in choiceSet is exactly being the source of an or link into node.