Breakage

SE.Persistence.Relation.Breakage

A breaking step is a step of a transformation classified as breaking.

Breakage is not the negation of survival. On an arbitrary dynamics a breaking step can connect states that are identity-related by some other path (see SE.Persistence.Relation.NonCollapse). Only when no other path exists, as on the free dynamics, does a breaking step separate its endpoints.

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

One step of a breaking transformation of c.

Equations

• c.stepBrk d x y = ∃ (t : T), c.IsBrk t ∧ d.step t x y

theorem SE.Persistence.Classification.not_identityRel_of_stepBrk_free {T : Type} (c : Classification T) {x y : T × Bool} (h : c.stepBrk (freeDynamics T) x y) : ¬c.identityRel (freeDynamics T) x y

On the free dynamics, a breaking step separates its endpoints.