Non-Collapse #

SE.Persistence.Relation.NonCollapse

Results that two notions do not coincide.

Between classifications: two classifications collapse on a dynamics when they generate the same identity relation.

on every dynamics, a difference in generated relations forces a difference in preserving sets (equal preserving sets never separate classifications);
on the free dynamics, the converse holds.

Between relations:

survival is strictly weaker than the identity relation: on the free dynamics a preserving step survives forward but not backward;
breakage does not separate: a breaking step and an identity-relating path can coexist.

Scope: both classifications act on one shared carrier. A carrier that differs per classification is not modeled here, so a pair separated only by carrier is outside these results.

source

def SE.Persistence.Classification.NonCollapsing {T C : Type} (d : Dynamics T C) (c c' : Classification T) :

Prop

The classifications generate different identity relations on d.

Equations

SE.Persistence.Classification.NonCollapsing d c c' = (c.identityRel d ≠ c'.identityRel d)

Instances For

source

theorem SE.Persistence.Classification.prs_difference_of_nonCollapsing {T C : Type} {c c' : Classification T} {d : Dynamics T C} (h : NonCollapsing d c c') :

∃ (t : T), ¬(c.IsPrs t ↔ c'.IsPrs t)

Non-collapse on any dynamics forces a preserving-set difference.

source

theorem SE.Persistence.Classification.nonCollapsing_free_iff {T : Type} (c c' : Classification T) :

NonCollapsing (freeDynamics T) c c' ↔ ∃ (t : T), ¬(c.IsPrs t ↔ c'.IsPrs t)

On the free dynamics, two classifications are non-collapsing exactly when their preserving sets differ.

source

theorem SE.Persistence.Classification.survives_free_iff {T : Type} (c : Classification T) (t : T) :

c.Survives (freeDynamics T) (t, false ) (t, true ) ↔ c.IsPrs t

On the free dynamics, survival of a private pair is exactly preservation.

source

theorem SE.Persistence.Classification.survives_ne_identityRel_free {T : Type} (c : Classification T) {t : T} (h : c.IsPrs t) :

c.Survives (freeDynamics T) (t, false ) (t, true ) ∧ ¬c.Survives (freeDynamics T) (t, true ) (t, false ) ∧ c.identityRel (freeDynamics T) (t, true ) (t, false )

Survival is strictly weaker than the identity relation: for a preserving transformation, its private pair survives forward, does not survive backward, and is identity-related backward.

source

theorem SE.Persistence.Classification.stepBrk_not_separating :

∃ (c : Classification Bool), ∃ (d : Dynamics Bool Unit), ∃ (x : Unit ), ∃ (y : Unit ), c.stepBrk d x y ∧ c.identityRel d x y

Breakage does not separate in general: some classification and dynamics have a breaking step between states that are also identity-related.