Structural Setting

SE.Individuation.Structural.Setting

A setting for the exclusive-whole construction at a fixed granularity. It supplies, for atoms A and candidate presentations Presentation:

• an eligible domain eligible ⊆ A;
• a presentation-admissibility predicate admissible;
• a support function support : Presentation → Set A;
• containment of admissible supports in eligible;
• an equivalence relation E on the subtype of eligible atoms.

E is whole co-membership under the proposed criterion. It is not equality or strict identity of atoms.

Setting.CoMember lifts E to all atoms. It holds only between eligible atoms.

structure SE.Individuation.Structural.Setting (A Presentation : Type u) : Type u

A structural setting: eligible atoms, admissibility, support, and whole co-membership.

• eligible : MathlibMini.Set A

  The eligible domain: atoms inside the selected boundary.

• admissible : Presentation → Prop

  Eligibility of a candidate presentation for individuation evaluation.

• support : Presentation → MathlibMini.Set A

  The atoms represented by a presentation at this setting.

• support_subset_eligible (p : Presentation) : self.admissible p → self.support p ⊆ self.eligible

  Admissible supports lie inside the eligible domain.

• E : { a : A // a ∈ self.eligible } → { a : A // a ∈ self.eligible } → Prop

  Whole co-membership on eligible atoms.

• E_equivalence : Equivalence self.E

  Whole co-membership is an equivalence relation on eligible atoms.

def SE.Individuation.Structural.Setting.CoMember {A Presentation : Type u} (s : Setting A Presentation) (a b : A) : Prop

Whole co-membership lifted to all atoms: both atoms are eligible and E-related.

Equations

• s.CoMember a b = ∃ (ha : a ∈ s.eligible), ∃ (hb : b ∈ s.eligible), s.E ⟨a, ha⟩ ⟨b, hb⟩

theorem SE.Individuation.Structural.Setting.CoMember.left_eligible {A Presentation : Type u} {s : Setting A Presentation} {a b : A} (h : s.CoMember a b) : a ∈ s.eligible

The left element of a co-member pair is eligible.

theorem SE.Individuation.Structural.Setting.CoMember.right_eligible {A Presentation : Type u} {s : Setting A Presentation} {a b : A} (h : s.CoMember a b) : b ∈ s.eligible

The right element of a co-member pair is eligible.

theorem SE.Individuation.Structural.Setting.CoMember.refl {A Presentation : Type u} {s : Setting A Presentation} {a : A} (ha : a ∈ s.eligible) : s.CoMember a a

Co-membership is reflexive on eligible atoms.

theorem SE.Individuation.Structural.Setting.CoMember.symm {A Presentation : Type u} {s : Setting A Presentation} {a b : A} (h : s.CoMember a b) : s.CoMember b a

Co-membership is symmetric.

theorem SE.Individuation.Structural.Setting.CoMember.trans {A Presentation : Type u} {s : Setting A Presentation} {a b c : A} (h1 : s.CoMember a b) (h2 : s.CoMember b c) : s.CoMember a c

Co-membership is transitive.

theorem SE.Individuation.Structural.Setting.CoMember.to_E {A Presentation : Type u} {s : Setting A Presentation} {a b : A} (h : s.CoMember a b) (ha : a ∈ s.eligible) (hb : b ∈ s.eligible) : s.E ⟨a, ha⟩ ⟨b, hb⟩

Co-membership of eligible atoms is E on the corresponding subtype elements.

theorem SE.Individuation.Structural.Setting.CoMember.of_E {A Presentation : Type u} {s : Setting A Presentation} {x y : { a : A // a ∈ s.eligible }} (h : s.E x y) : s.CoMember x.val y.val

E on subtype elements gives co-membership of their underlying atoms.