Invariance

SE.Persistence.Relation.Invariance

A property of states is a persistence invariant when every preserving step leaves it unchanged.

Main result: invariance under the preserving steps is the same as respecting the identity relation ~_P. Invariants are exactly the properties that cannot tell identity-related states apart.

This is a different notion from framework-invariance in the Neutral Substrate theory, which concerns consistency across admissible frameworks.

def SE.Persistence.Classification.Invariant {T C : Type} (c : Classification T) (d : Dynamics T C) (φ : C → Prop) : Prop

φ is unchanged by every preserving step of c on d.

Equations

• c.Invariant d φ = ∀ (x y : C), c.stepRel d x y → (φ x ↔ φ y)

theorem SE.Persistence.Classification.invariant_iff_respects_identityRel {T C : Type} (c : Classification T) (d : Dynamics T C) (φ : C → Prop) : c.Invariant d φ ↔ ∀ (x y : C), c.identityRel d x y → (φ x ↔ φ y)

Invariance under preserving steps is respect for ~_P.

theorem SE.Persistence.Classification.Invariant.survives {T C : Type} {c : Classification T} {d : Dynamics T C} {φ : C → Prop} (h : c.Invariant d φ) {x y : C} (hs : c.Survives d x y) : φ x ↔ φ y

An invariant does not change along survival.

theorem SE.Persistence.Classification.Invariant.not {T C : Type} {c : Classification T} {d : Dynamics T C} {φ : C → Prop} (h : c.Invariant d φ) : c.Invariant d fun (x : C) => ¬φ x

The negation of an invariant is an invariant.

theorem SE.Persistence.Classification.Invariant.and {T C : Type} {c : Classification T} {d : Dynamics T C} {φ ψ : C → Prop} (hφ : c.Invariant d φ) (hψ : c.Invariant d ψ) : c.Invariant d fun (x : C) => φ x ∧ ψ x

The conjunction of two invariants is an invariant.

theorem SE.Persistence.Classification.invariant_of_prs_subset {T C : Type} {c c' : Classification T} {d : Dynamics T C} (h : ∀ (t : T), c.IsPrs t → c'.IsPrs t) {φ : C → Prop} (hφ : c'.Invariant d φ) : c.Invariant d φ

A classification that preserves fewer transformations has more invariants.