Invariance

SE.Persistence.Relation.Invariance

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

Generic observational equivalence is agreement on a family of predicates. Generated equivalence is its kernel for the family of all step invariants. Preservation and completeness are separate relational inclusions; no carrier or identity basis interpretation is supplied here.

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.relationInvariants {C : Type} (r : C → C → Prop) : MathlibMini.Set (C → Prop)

All predicates constant along the steps of a relation.

Equations

• SE.Persistence.relationInvariants r = MathlibMini.Set.ofPredicate fun (φ : C → Prop) => ∀ (x y : C), r x y → (φ x ↔ φ y)

def SE.Persistence.observationalEquivalence {C : Type} (Φ : MathlibMini.Set (C → Prop)) : C → C → Prop

Agreement on every observable in a family; no basis semantics is assumed.

Equations

• SE.Persistence.observationalEquivalence Φ x y = ∀ (φ : C → Prop), φ ∈ Φ → (φ x ↔ φ y)

theorem SE.Persistence.observationalEquivalence_equivalence {C : Type} (Φ : MathlibMini.Set (C → Prop)) : Equivalence (observationalEquivalence Φ)

Agreement on a family of observables is an equivalence relation.

theorem SE.Persistence.steps_respect_observables_iff {C : Type} (r : C → C → Prop) (Φ : MathlibMini.Set (C → Prop)) : (∀ (x y : C), r x y → observationalEquivalence Φ x y) ↔ Φ ⊆ relationInvariants r

Steps respect the observational kernel exactly when all observables are invariant.

theorem SE.Persistence.relationInvariants_generated {C : Type} (r : C → C → Prop) : relationInvariants (Generated r) = relationInvariants r

Taking equivalence closure does not change the invariant predicates.

theorem SE.Persistence.generated_eq_observationalEquivalence {C : Type} (r : C → C → Prop) : Generated r = observationalEquivalence (relationInvariants r)

Generated identity is exactly agreement on all step invariants.

theorem SE.Persistence.observables_invariant_iff_generated_respects {C : Type} (r : C → C → Prop) (Φ : MathlibMini.Set (C → Prop)) : Φ ⊆ relationInvariants r ↔ ∀ (x y : C), Generated r x y → observationalEquivalence Φ x y

Preservation: all observables are invariant iff generated identity respects them.

theorem SE.Persistence.observational_completeness_iff_invariant_saturation {C : Type} (r : C → C → Prop) (Φ : MathlibMini.Set (C → Prop)) : (∀ (x y : C), observationalEquivalence Φ x y → Generated r x y) ↔ relationInvariants r ⊆ relationInvariants (observationalEquivalence Φ)

Completeness means every step invariant is constant on observational classes.

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.identityRel_iff_all_invariants_agree {T C : Type} (c : Classification T) (d : Dynamics T C) (x y : C) : c.identityRel d x y ↔ ∀ (φ : C → Prop), c.Invariant d φ → (φ x ↔ φ y)

Identity holds exactly when every persistence invariant agrees at the two states.

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.