Persistence Connection: Successful Presentations #

SE.Individuation.Structural.Commitments

At a setting, the carrier is the subtype of successful presentations. With

P the same-unit judgments,
D the distinct-unit judgments,
E support equality,

this module proves, using Persistence's commitment calculus:

E is Persistence-admissible for P and D;
the commitments are consistent;
E is the unique admissible relation;
no pair is undetermined under these exact commitments;
D coincides with the pairs separated by the support observation map.

Hypotheses used: nonemptiness of successful supports, and the same-or-distinct dichotomy (for uniqueness and for unequal implies disjoint). The coincidence of D with the separated pairs depends on exclusivity through the dichotomy.

This is a soundness construction and establishes mathematical correctness only. One criterion determines both P and D, so consistency does not independently validate the criterion against practice.

Persistence's calculus is stated for carriers in Type, so this module specializes atoms and presentations to universe 0.

source

def SE.Individuation.Structural.Setting.samePairs {A Presentation : Type} (s : Setting A Presentation) :

{ p : Presentation // s.Succeeds p } → { p : Presentation // s.Succeeds p } → Prop

Same-unit judgments on successful presentations.

Equations

s.samePairs x y = s.SameUnit x.val y.val

Instances For

source

def SE.Individuation.Structural.Setting.distinctPairs {A Presentation : Type} (s : Setting A Presentation) :

{ p : Presentation // s.Succeeds p } → { p : Presentation // s.Succeeds p } → Prop

Distinct-unit judgments on successful presentations.

Equations

s.distinctPairs x y = s.DistinctUnits x.val y.val

Instances For

source

def SE.Individuation.Structural.Setting.supportEquality {A Presentation : Type} (s : Setting A Presentation) :

{ p : Presentation // s.Succeeds p } → { p : Presentation // s.Succeeds p } → Prop

Support equality on successful presentations.

Equations

s.supportEquality x y = (s.support x.val = s.support y.val)

Instances For

source

def SE.Individuation.Structural.Setting.supportObservation {A Presentation : Type} (s : Setting A Presentation) :

{ p : Presentation // s.Succeeds p } → MathlibMini.Set A

The support observation map on successful presentations.

Equations

s.supportObservation x = s.support x.val

Instances For

source

theorem SE.Individuation.Structural.Setting.supportEquality_equivalence {A Presentation : Type} (s : Setting A Presentation) :

Equivalence s.supportEquality

Equality of support is an equivalence relation.

source

theorem SE.Individuation.Structural.Setting.supportEquality_admissible {A Presentation : Type} (s : Setting A Presentation) :

Persistence.Admissible s.samePairs s.distinctPairs s.supportEquality

Support equality is Persistence-admissible for same-unit and distinct-unit judgments.

source

theorem SE.Individuation.Structural.Setting.commitments_consistent {A Presentation : Type} (s : Setting A Presentation) :

Persistence.Consistent s.samePairs s.distinctPairs

The same-unit and distinct-unit commitments are consistent.

source

theorem SE.Individuation.Structural.Setting.supportEquality_unique {A Presentation : Type} (s : Setting A Presentation) {E : { p : Presentation // s.Succeeds p } → { p : Presentation // s.Succeeds p } → Prop} (hE : Persistence.Admissible s.samePairs s.distinctPairs E) (x y : { p : Presentation // s.Succeeds p }) :

E x y ↔ s.supportEquality x y

Support equality is the only admissible relation. Uses the same-or-distinct dichotomy.

source

theorem SE.Individuation.Structural.Setting.no_undetermined {A Presentation : Type} (s : Setting A Presentation) (x y : { p : Presentation // s.Succeeds p }) :

¬Persistence.Undetermined s.samePairs s.distinctPairs x y

No pair of successful presentations is undetermined under these exact commitments.

source

theorem SE.Individuation.Structural.Setting.distinctPairs_iff_separated {A Presentation : Type} (s : Setting A Presentation) (x y : { p : Presentation // s.Succeeds p }) :

s.distinctPairs x y ↔ Persistence.SeparatedBy s.supportObservation x y

The distinct-unit commitments coincide with the pairs separated by the support observation map.