Connectivity Instance

SE.Individuation.Structural.Connectivity

One construction of the equivalence relation E: the equivalence relation generated by a structural bond relation on eligible atoms. The direction of a bond is immaterial, because the generated equivalence closes it symmetrically.

BondClosure is universe-polymorphic. Its agreement with Persistence's Generated at universe 0, and the finite-path characterization, are in BoundaryCompatibility.

Using this construction scientifically requires independently justifying why bond-connected atoms belong to the same intended whole. Nothing here does that.

inductive SE.Individuation.Structural.BondClosure {C : Type u} (r : C → C → Prop) : C → C → Prop

The equivalence relation generated by r.

• rel {C : Type u} {r : C → C → Prop} {x y : C} : r x y → BondClosure r x y
• refl {C : Type u} {r : C → C → Prop} (x : C) : BondClosure r x x
• symm {C : Type u} {r : C → C → Prop} {x y : C} : BondClosure r x y → BondClosure r y x
• trans {C : Type u} {r : C → C → Prop} {x y z : C} : BondClosure r x y → BondClosure r y z → BondClosure r x z

theorem SE.Individuation.Structural.BondClosure.equivalence {C : Type u} (r : C → C → Prop) : Equivalence (BondClosure r)

BondClosure r is an equivalence relation.

theorem SE.Individuation.Structural.BondClosure.le_of_equivalence {C : Type u} {r s : C → C → Prop} (hs : Equivalence s) (h : ∀ (x y : C), r x y → s x y) {x y : C} (hg : BondClosure r x y) : s x y

BondClosure r is the least equivalence relation containing r.

theorem SE.Individuation.Structural.BondClosure.map {C : Type u} {D : Type v} {r : C → C → Prop} {r' : D → D → Prop} (g : C → D) (h : ∀ (x y : C), r x y → r' (g x) (g y)) {x y : C} (hg : BondClosure r x y) : BondClosure r' (g x) (g y)

A map preserving generators preserves the generated relation.

theorem SE.Individuation.Structural.BondClosure.eq_of_isolated {C : Type u} {r : C → C → Prop} {a : C} (hiso : ∀ (y : C), ¬r a y ∧ ¬r y a) {x y : C} (h : BondClosure r x y) : (x = a → y = a) ∧ (y = a → x = a)

An element with no bond in either direction is connected only to itself.

def SE.Individuation.Structural.Setting.BondGenerated {A Presentation : Type u} (s : Setting A Presentation) (bond : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop) : Prop

A setting whose co-membership is the equivalence generated by bond.

Equations

• s.BondGenerated bond = ∀ (x y : { a : A // a ∈ s.eligible }), s.E x y ↔ SE.Individuation.Structural.BondClosure bond x y

def SE.Individuation.Structural.Setting.ofBonds {A Presentation : Type u} (eligible : MathlibMini.Set A) (admissible : Presentation → Prop) (support : Presentation → MathlibMini.Set A) (support_subset_eligible : ∀ (p : Presentation), admissible p → support p ⊆ eligible) (bond : { a : A // a ∈ eligible } → { a : A // a ∈ eligible } → Prop) : Setting A Presentation

The connectivity instance: co-membership is the equivalence generated by bond.

Equations

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

theorem SE.Individuation.Structural.Setting.ofBonds_bondGenerated {A Presentation : Type u} (eligible : MathlibMini.Set A) (admissible : Presentation → Prop) (support : Presentation → MathlibMini.Set A) (support_subset_eligible : ∀ (p : Presentation), admissible p → support p ⊆ eligible) (bond : { a : A // a ∈ eligible } → { a : A // a ∈ eligible } → Prop) : (ofBonds eligible admissible support support_subset_eligible bond).BondGenerated bond

A setting built from bonds is bond-generated.

theorem SE.Individuation.Structural.Setting.BondGenerated.coMember_of_bond {A Presentation : Type u} {s : Setting A Presentation} {bond : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (hs : s.BondGenerated bond) {x y : { a : A // a ∈ s.eligible }} (h : bond x y) : s.CoMember x.val y.val

Bonded atoms are co-members.

theorem SE.Individuation.Structural.Setting.BondGenerated.le_of_equivalence {A Presentation : Type u} {s : Setting A Presentation} {bond : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (hs : s.BondGenerated bond) {R : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (hR : Equivalence R) (hb : ∀ (x y : { a : A // a ∈ s.eligible }), bond x y → R x y) {x y : { a : A // a ∈ s.eligible }} (h : s.E x y) : R x y

Co-membership is the least equivalence relation containing the bonds.

theorem SE.Individuation.Structural.Setting.wholeConditions_singleton_of_isolated {A Presentation : Type u} {s : Setting A Presentation} {a : A} (ha : a ∈ s.eligible) (hiso : ∀ (b : A), s.CoMember a b → b = a) : s.WholeConditions {a}

If the class of an eligible atom is only that atom, the singleton meets the whole conditions. Whether a singleton is a whole of the intended kind is decided by independently warranted judgments for that kind, not by this construction.

theorem SE.Individuation.Structural.Setting.BondGenerated.wholeConditions_singleton_of_no_bond {A Presentation : Type u} {s : Setting A Presentation} {bond : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (hs : s.BondGenerated bond) {a : A} (ha : a ∈ s.eligible) (hiso : ∀ (y : { a : A // a ∈ s.eligible }), ¬bond ⟨a, ha⟩ y ∧ ¬bond y ⟨a, ha⟩) : s.WholeConditions {a}

In a bond-generated setting, an eligible atom with no bond forms a singleton whole.