Persistence Connection: Whole Co-membership Constraints #

SE.Individuation.Structural.BoundaryCompatibility

A second use of Persistence's generic commitment calculus operates on eligible atoms. For the connectivity instance:

P is the bond relation, read as same-whole co-membership commitments;
D is independently warranted commitments that two atoms belong to different wholes.

D does not mean that two atoms are unequal. Different atoms can belong to the same whole. The generated equivalence is whole co-membership, not strict identity of atoms.

This module proves that BondClosure agrees with Persistence's Generated at universe 0, so Persistence's results apply: the finite-path characterization, consistency as compatibility with separation commitments, forbidden proposed bonds, and the generator-comparison witness.

A rejecting result identifies disagreement among the proposed bonds and independently warranted boundaries. Determining which input is defective needs further investigation. A witness localizes a difference. It does not identify a scientifically erroneous bond.

Comparisons across eligible domains need an explicit common carrier or transport. Inclusion of atoms alone does not establish preservation or reflection of connectivity.

source

theorem SE.Individuation.Structural.bondClosure_iff_generated {C : Type} {r : C → C → Prop} {x y : C} :

BondClosure r x y ↔ Persistence.Generated r x y

BondClosure is Persistence's Generated at universe 0.

source

theorem SE.Individuation.Structural.bondClosure_iff_reach_symmStep {C : Type} {r : C → C → Prop} {x y : C} :

BondClosure r x y ↔ Persistence.Reach (Persistence.SymmStep r) x y

Finite-path characterization: bonded atoms are co-members exactly when a finite chain of bonds, each used in either direction, connects them. The chain explains the co-membership.

source

theorem SE.Individuation.Structural.consistent_iff_no_separated_connected {C : Type} {P D : C → C → Prop} :

Persistence.Consistent P D ↔ ∀ (x y : C), D x y → ¬BondClosure P x y

Boundary compatibility: bonds and separation commitments are consistent exactly when no pair asserted to be in different wholes lies in the generated co-membership.

source

theorem SE.Individuation.Structural.forbidden_iff_extend_connects {C : Type} {P D : C → C → Prop} {x y : C} :

Persistence.Forbidden P D x y ↔ ∃ (u : C), ∃ (v : C), D u v ∧ BondClosure (Persistence.Extend P x y) u v

A forbidden proposed bond is one whose addition would connect a prohibited pair.

source

theorem SE.Individuation.Structural.exists_bond_difference {C : Type} {P Q : C → C → Prop} (h : ¬∀ (x y : C), BondClosure P x y ↔ BondClosure Q x y) :

∃ (x : C), ∃ (y : C), P x y ∧ ¬BondClosure Q x y ∨ Q x y ∧ ¬BondClosure P x y

Generator-comparison witness: if two bond sets generate different co-membership relations, a single bond on one side has endpoints not connected on the other.

source

theorem SE.Individuation.Structural.Setting.BondGenerated.admissible_of_consistent {A Presentation : Type} {s : Setting A Presentation} {bond : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (hs : s.BondGenerated bond) {D : { a : A // a ∈ s.eligible } → { a : A // a ∈ s.eligible } → Prop} (h : Persistence.Consistent bond D) :

Persistence.Admissible bond D s.E

Consistent bonds and separation commitments make the setting's co-membership admissible.