Same-Unit and Distinct-Unit Judgments

SE.Individuation.Structural.SameUnit

Two presentations identify the same unit exactly when both succeed and their supports are equal. They identify distinct units exactly when both succeed and their supports share no atom.

Both are guarded by success. Same-unit identity is an equivalence relation on successful presentations only; its extension to all candidate presentations is not globally reflexive (not_sameUnit_refl_of_not_succeeds).

The mathematical complement of same-unit on successful presentations is distinctness (distinctUnits_iff_not_sameUnit). This does not justify treating failure to establish sameness from evidence as established distinctness.

This construction is exclusive-whole and extensional. Neither commitment is a requirement of Individuation in general.

def SE.Individuation.Structural.Setting.SameUnit {A Presentation : Type u} (s : Setting A Presentation) (p q : Presentation) : Prop

Both presentations succeed and their supports are equal.

Equations

• s.SameUnit p q = (s.Succeeds p ∧ s.Succeeds q ∧ s.support p = s.support q)

def SE.Individuation.Structural.Setting.DistinctUnits {A Presentation : Type u} (s : Setting A Presentation) (p q : Presentation) : Prop

Both presentations succeed and their supports share no atom.

Equations

• s.DistinctUnits p q = (s.Succeeds p ∧ s.Succeeds q ∧ ∀ (a : A), a ∈ s.support p → ¬a ∈ s.support q)

theorem SE.Individuation.Structural.Setting.SameUnit.symm {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (h : s.SameUnit p q) : s.SameUnit q p

SameUnit is symmetric.

theorem SE.Individuation.Structural.Setting.SameUnit.trans {A Presentation : Type u} {s : Setting A Presentation} {p q r : Presentation} (h1 : s.SameUnit p q) (h2 : s.SameUnit q r) : s.SameUnit p r

SameUnit is transitive.

theorem SE.Individuation.Structural.Setting.sameUnit_refl_iff {A Presentation : Type u} (s : Setting A Presentation) (p : Presentation) : s.SameUnit p p ↔ s.Succeeds p

Same-unit identity at p with itself is exactly success of p.

theorem SE.Individuation.Structural.Setting.sameUnit_equivalence {A Presentation : Type u} (s : Setting A Presentation) : Equivalence fun (x y : { p : Presentation // s.Succeeds p }) => s.SameUnit x.val y.val

Same-unit identity is an equivalence relation on the subtype of successful presentations.

theorem SE.Individuation.Structural.Setting.not_sameUnit_refl_of_not_succeeds {A Presentation : Type u} {s : Setting A Presentation} {p : Presentation} (h : ¬s.Succeeds p) : ¬s.SameUnit p p

The success-guarded relation is not reflexive at a presentation that fails.

theorem SE.Individuation.Structural.Setting.sameUnit_iff_overlap {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.Succeeds p) (hq : s.Succeeds q) : s.SameUnit p q ↔ ∃ (a : A), a ∈ s.support p ∧ a ∈ s.support q

Overlap characterization: on successful presentations, same unit is exactly overlap of supports. The success hypotheses are essential.

theorem SE.Individuation.Structural.Setting.sameUnit_or_distinctUnits {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.Succeeds p) (hq : s.Succeeds q) : s.SameUnit p q ∨ s.DistinctUnits p q

Same-or-distinct dichotomy on successful presentations: at least one holds.

theorem SE.Individuation.Structural.Setting.not_sameUnit_and_distinctUnits {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.Succeeds p) : ¬(s.SameUnit p q ∧ s.DistinctUnits p q)

Same-or-distinct dichotomy on successful presentations: not both.

theorem SE.Individuation.Structural.Setting.distinctUnits_iff_not_sameUnit {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.Succeeds p) (hq : s.Succeeds q) : s.DistinctUnits p q ↔ ¬s.SameUnit p q

On successful presentations, distinct units is exactly failure of same unit.

theorem SE.Individuation.Structural.Setting.succeeds_iff_of_support_eq {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.admissible p) (hq : s.admissible q) (h : s.support p = s.support q) : s.Succeeds p ↔ s.Succeeds q

Lossless re-presentation: admissible presentations with equal supports have the same success status.

theorem SE.Individuation.Structural.Setting.sameUnit_of_support_eq {A Presentation : Type u} {s : Setting A Presentation} {p q : Presentation} (hp : s.Succeeds p) (hq : s.admissible q) (h : s.support p = s.support q) : s.SameUnit p q

Lossless re-presentation: when one succeeds, an admissible presentation with equal support identifies the same unit, whatever its format, labels, or annotation.