Observation as Distinct-Commitments

SE.Persistence.Commitment.Observed

A presentation π : C → O separates two states when it gives them different values. Treat those pairs as asserted distinct: SeparatedBy π x y := π x ≠ π y.

• A presentation is sound for a classification exactly when the preserving steps are consistent with SeparatedBy π.
• A presentation is complete exactly when every pair it does not separate is required to be identical.
• When a presentation separates two states, they are forbidden to be identical.

Soundness of a presentation is therefore an instance of consistency, in which the distinct-commitments come from what an observer sees. Completeness is a separate hypothesis about the presentation. It is not implied by having no distinct-commitments: a presentation that separates nothing and a dynamics with no preserving steps leave distinct states unrelated (presentation_blind_example).

Several observers give several sources of distinct-commitments, combined by consistent_union_iff.

This module restates existing notions in the language of commitments. It adds no hypothesis about how any presentation is warranted.

def SE.Persistence.SeparatedBy {C O : Type} (π : C → O) : C → C → Prop

The pairs separated by a presentation, read as distinct-commitments.

Equations

• SE.Persistence.SeparatedBy π x y = (π x ≠ π y)

theorem SE.Persistence.Classification.presentationSound_iff_consistent {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : c.PresentationSound d π ↔ Consistent (c.stepRel d) (SeparatedBy π)

Soundness of a presentation is consistency with the pairs it separates.

theorem SE.Persistence.Classification.presentationComplete_iff_required {T C O : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) : c.PresentationComplete d π ↔ ∀ (x y : C), π x = π y → Required (c.stepRel d) x y

Completeness of a presentation is: every pair it does not separate is required to be identical.

theorem SE.Persistence.Classification.forbidden_of_separated {T C O : Type} (c : Classification T) (d : Dynamics T C) {π : C → O} {x y : C} (h : π x ≠ π y) : Forbidden (c.stepRel d) (SeparatedBy π) x y

A pair a presentation separates is forbidden to be identical.

theorem SE.Persistence.Classification.two_presentations_sound_iff {T C O O' : Type} (c : Classification T) (d : Dynamics T C) (π : C → O) (π' : C → O') : c.PresentationSound d π ∧ c.PresentationSound d π' ↔ Consistent (c.stepRel d) fun (x y : C) => SeparatedBy π x y ∨ SeparatedBy π' x y

Two presentations are both sound exactly when the preserving steps are consistent with the pairs that either one separates.