Observability

SE.Persistence.Relation.Observability

A presentation is a function π : C → O from states to what an observer receives. The predicates it can express are exactly those that depend on a state only through π.

This module relates a presentation to the identity relation ~_P using observationalEquivalence and relationInvariants from the Invariance module.

• Sound: identity-related states have equal presentations.
• Complete: states with equal presentations are identity-related.

Soundness and completeness are hypotheses. This module does not say how either is warranted. A sound presentation can certify non-identity. Certifying identity needs completeness. A presentation that is not complete is blind: some states it cannot separate are not identity-related, and presentation_blind_example shows this can happen.

def SE.Persistence.presentable {C O : Type} (π : C → O) : MathlibMini.Set (C → Prop)

The predicates a presentation can express: those of the form P (π x).

Equations

• SE.Persistence.presentable π = MathlibMini.Set.ofPredicate fun (φ : C → Prop) => ∃ (P : O → Prop), ∀ (x : C), φ x ↔ P (π x)

theorem SE.Persistence.observationalEquivalence_presentable_iff {C O : Type} (π : C → O) (x y : C) : observationalEquivalence (presentable π) x y ↔ π x = π y

Observational equivalence over the presentable predicates is equality of presentations.

def SE.Persistence.Classification.PresentationSound {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : Prop

Identity-related states have equal presentations.

Equations

• c.PresentationSound d π = ∀ (x y : C), c.identityRel d x y → π x = π y

def SE.Persistence.Classification.PresentationComplete {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : Prop

States with equal presentations are identity-related.

Equations

• c.PresentationComplete d π = ∀ (x y : C), π x = π y → c.identityRel d x y

theorem SE.Persistence.Classification.presentationSound_iff {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : c.PresentationSound d π ↔ presentable π ⊆ relationInvariants (c.stepRel d)

Soundness means every presentable predicate is a step invariant.

theorem SE.Persistence.Classification.presentationComplete_iff {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : c.PresentationComplete d π ↔ relationInvariants (c.stepRel d) ⊆ relationInvariants (observationalEquivalence (presentable π))

Completeness means every step invariant is constant on presentation classes.

theorem SE.Persistence.Classification.presentationComplete_iff_invariants_determined {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : c.PresentationComplete d π ↔ ∀ (φ : C → Prop), c.Invariant d φ → ∀ (x y : C), π x = π y → (φ x ↔ φ y)

Completeness means every identity invariant is determined by the presentation.

theorem SE.Persistence.Classification.not_identityRel_of_sound_of_ne {T C O : Type} {c : Classification T} {d : Dynamics T C} {π : C → O} (hs : c.PresentationSound d π) {x y : C} (hne : π x ≠ π y) : ¬c.identityRel d x y

Separation: a sound presentation that distinguishes two states certifies that they are not identity-related.

theorem SE.Persistence.Classification.identityRel_of_complete_of_eq {T C O : Type} {c : Classification T} {d : Dynamics T C} {π : C → O} (hc : c.PresentationComplete d π) {x y : C} (h : π x = π y) : c.identityRel d x y

Identification: a complete presentation that does not distinguish two states certifies that they are identity-related.

theorem SE.Persistence.Classification.not_presentationComplete_iff_blind {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : ¬c.PresentationComplete d π ↔ ∃ (x : C), ∃ (y : C), π x = π y ∧ ¬c.identityRel d x y

A presentation is not complete exactly when it is blind: it fails to separate some states that are not identity-related.

theorem SE.Persistence.Classification.presentationSound_of_factor {T C O O' : Type} {c : Classification T} {d : Dynamics T C} {π : C → O} (g : O → O') (hs : c.PresentationSound d π) : c.PresentationSound d fun (x : C) => g (π x)

A coarser presentation of a sound presentation is sound.

theorem SE.Persistence.Classification.presentationComplete_of_factor {T C O O' : Type} {c : Classification T} {d : Dynamics T C} {π : C → O} (g : O → O') (hc : c.PresentationComplete d fun (x : C) => g (π x)) : c.PresentationComplete d π

If a coarser presentation is complete, so is the finer one.

theorem SE.Persistence.presentation_blind_example : ∃ (c : Classification Unit), ∃ (d : Dynamics Unit Bool), ∃ (π : Bool → Unit), ∃ (x : Bool), ∃ (y : Bool), π x = π y ∧ ¬c.identityRel d x y

Blindness occurs: some classification, dynamics and presentation fail to separate two states that are not identity-related.