Neutral Substrate Adapter

SE.Individuation.Structural.Account

Constructs SE.Substrate.IndividuationAccount (Set A) from the structural construction:

• Context: the structural setting;
• Presentation: the fixed presentation type;
• admissiblePresentation: the setting's admissibility predicate;
• one: success (admissibility and the whole conditions);
• sameUnit: successful presentations with equal support;
• presents: success, with the complete support equal to the set-valued referent.

Set-valued referents are a local extensional realization. They do not identify carrier equality with identity throughout the framework. Assigning this account to one of the three referent kinds belongs to construction of a particular IndividuationRegime (IR-CARRIER).

def SE.Individuation.Structural.individuationAccount (A Presentation : Type u) : Substrate.IndividuationAccount (MathlibMini.Set A)

The structural individuation account over set-valued referents.

Equations

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

Adapter equations

theorem SE.Individuation.Structural.individuationAccount.admissiblePresentation_iff {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} : (individuationAccount A Presentation).admissiblePresentation c p ↔ c.admissible p

A presentation is admissible exactly when the account's admissibility condition holds.

theorem SE.Individuation.Structural.individuationAccount.one_iff {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} : (individuationAccount A Presentation).one c p ↔ c.Succeeds p

An element counts as one exactly when the account's unity condition holds.

theorem SE.Individuation.Structural.individuationAccount.sameUnit_iff {A Presentation : Type u} {c : Setting A Presentation} {p q : Presentation} : (individuationAccount A Presentation).sameUnit c p q ↔ c.SameUnit p q

Two elements are in the same unit exactly when the account's same-unit condition holds.

theorem SE.Individuation.Structural.individuationAccount.presents_iff {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} {W : MathlibMini.Set A} : (individuationAccount A Presentation).presents c p W ↔ c.Succeeds p ∧ c.support p = W

A presentation presents a whole exactly when the account's presentation condition holds.

Success guards

theorem SE.Individuation.Structural.individuationAccount.one_admissible {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} (h : (individuationAccount A Presentation).one c p) : (individuationAccount A Presentation).admissiblePresentation c p

Whatever counts as one is admissible.

theorem SE.Individuation.Structural.individuationAccount.presents_one {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} {W : MathlibMini.Set A} (h : (individuationAccount A Presentation).presents c p W) : (individuationAccount A Presentation).one c p

Whatever a presentation presents counts as one.

theorem SE.Individuation.Structural.individuationAccount.sameUnit_one_left {A Presentation : Type u} {c : Setting A Presentation} {p q : Presentation} (h : (individuationAccount A Presentation).sameUnit c p q) : (individuationAccount A Presentation).one c p

If two elements are in the same unit, the left one counts as one.

theorem SE.Individuation.Structural.individuationAccount.sameUnit_one_right {A Presentation : Type u} {c : Setting A Presentation} {p q : Presentation} (h : (individuationAccount A Presentation).sameUnit c p q) : (individuationAccount A Presentation).one c q

If two elements are in the same unit, the right one counts as one.

theorem SE.Individuation.Structural.individuationAccount.one_iff_presents_support {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} : (individuationAccount A Presentation).one c p ↔ (individuationAccount A Presentation).presents c p (c.support p)

A successful presentation presents exactly its support, and nothing else.

theorem SE.Individuation.Structural.individuationAccount.presents_unique {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} {W W' : MathlibMini.Set A} (h : (individuationAccount A Presentation).presents c p W) (h' : (individuationAccount A Presentation).presents c p W') : W = W'

A presentation presents at most one whole.

theorem SE.Individuation.Structural.individuationAccount.sameUnit_iff_common_presents {A Presentation : Type u} {c : Setting A Presentation} {p q : Presentation} : (individuationAccount A Presentation).sameUnit c p q ↔ ∃ (W : MathlibMini.Set A), (individuationAccount A Presentation).presents c p W ∧ (individuationAccount A Presentation).presents c q W

Same unit is exactly: both presentations present a common set-valued referent.

theorem SE.Individuation.Structural.individuationAccount.sameUnit_self_iff {A Presentation : Type u} {c : Setting A Presentation} {p : Presentation} : (individuationAccount A Presentation).sameUnit c p p ↔ (individuationAccount A Presentation).one c p

The adapter's same-unit relation at a presentation with itself is exactly its success.