Classification

SE.Persistence.Domain.Classification

A persistence classification over an abstract transformation domain T.

The domain is a parameter. This module does not decide which transformation vocabulary is classified, and it does not define identity regimes or regime profiles: a regime profile is a classification together with a carrier and an identity basis, and belongs downstream.

Applicability and classification are encoded together as T → Option ClassificationValue:

• none is inapplicable; no classification exists;
• some v is applicable with class v.

N/A is the absence of a value, and IGN is a value.

structure SE.Persistence.Classification (T : Type) : Type

A persistence classification over the transformation domain T.

pattern t is the applicability-and-class pair for t. persist is the declared persistence set. Its relation to the preserving transformations is the predicate Classification.WellFormed, stated separately rather than carried as a field.

• pattern : T → Option ClassificationValue

  Applicability and class: none is inapplicable, some v is applicable with class v.

• persist : T → Prop

  The declared persistence set.

def SE.Persistence.Classification.Applicable {T : Type} (c : Classification T) (t : T) : Prop

t is applicable under c.

Equations

• c.Applicable t = (c.pattern t ≠ none)

def SE.Persistence.Classification.IsPrs {T : Type} (c : Classification T) (t : T) : Prop

t is applicable and identity-preserving under c.

Equations

• c.IsPrs t = (c.pattern t = some SE.Persistence.ClassificationValue.prs)

def SE.Persistence.Classification.IsBrk {T : Type} (c : Classification T) (t : T) : Prop

t is applicable and identity-breaking under c.

Equations

• c.IsBrk t = (c.pattern t = some SE.Persistence.ClassificationValue.brk)

def SE.Persistence.Classification.WellFormed {T : Type} (c : Classification T) : Prop

The declared persistence set contains only identity-preserving transformations.

Equations

• c.WellFormed = ∀ (t : T), c.persist t → c.IsPrs t

def SE.Persistence.Classification.coarse {T : Type} (c : Classification T) (t : T) : ClassificationValue

The total three-valued matrix obtained by sending inapplicable to ign.

This forgets applicability. coarse_eq_prs_iff shows it preserves the preserving set.

Equations

• c.coarse t = (c.pattern t).getD SE.Persistence.ClassificationValue.ign

@[implicit_reducible]

instance SE.Persistence.instDecidableApplicable {T : Type} (c : Classification T) (t : T) : Decidable (c.Applicable t)

Applicability is decidable, so finite statements can be checked with decide.

Equations

• SE.Persistence.instDecidableApplicable c t = SE.Persistence.instDecidableApplicable._aux_1 c t

@[implicit_reducible]

instance SE.Persistence.instDecidableIsPrs {T : Type} (c : Classification T) (t : T) : Decidable (c.IsPrs t)

Preservation is decidable, so finite statements can be checked with decide.

Equations

• SE.Persistence.instDecidableIsPrs c t = SE.Persistence.instDecidableIsPrs._aux_1 c t

@[implicit_reducible]

instance SE.Persistence.instDecidableIsBrk {T : Type} (c : Classification T) (t : T) : Decidable (c.IsBrk t)

Breakage is decidable, so finite statements can be checked with decide.

Equations

• SE.Persistence.instDecidableIsBrk c t = SE.Persistence.instDecidableIsBrk._aux_1 c t

theorem SE.Persistence.Classification.applicable_iff {T : Type} (c : Classification T) (t : T) : c.Applicable t ↔ ∃ (v : ClassificationValue), c.pattern t = some v

Applicable means some classification exists.

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

A preserving transformation is applicable.

theorem SE.Persistence.Classification.applicable_of_isBrk {T : Type} {c : Classification T} {t : T} (h : c.IsBrk t) : c.Applicable t

A breaking transformation is applicable.

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

A transformation is not both preserving and breaking.

theorem SE.Persistence.Classification.coarse_of_pattern_none {T : Type} {c : Classification T} {t : T} (h : c.pattern t = none) : c.coarse t = ClassificationValue.ign

An inapplicable transformation has coarse value ign.

theorem SE.Persistence.Classification.coarse_of_pattern_some {T : Type} {c : Classification T} {t : T} {v : ClassificationValue} (h : c.pattern t = some v) : c.coarse t = v

An applicable transformation keeps its value under the coarse matrix.

theorem SE.Persistence.Classification.coarse_eq_prs_iff {T : Type} (c : Classification T) (t : T) : c.coarse t = ClassificationValue.prs ↔ c.IsPrs t

The coarse matrix preserves exactly the preserving set.

theorem SE.Persistence.Classification.coarse_eq_brk_iff {T : Type} (c : Classification T) (t : T) : c.coarse t = ClassificationValue.brk ↔ c.IsBrk t

The coarse matrix preserves exactly the breaking set.

theorem SE.Persistence.Classification.coarse_eq_of_pattern_eq {T : Type} {c c' : Classification T} (h : ∀ (t : T), c.pattern t = c'.pattern t) (t : T) : c.coarse t = c'.coarse t

Equal patterns have equal coarse values.

theorem SE.Persistence.Classification.pattern_ne_of_coarse_ne {T : Type} {c c' : Classification T} (h : ∃ (t : T), c.coarse t ≠ c'.coarse t) : ∃ (t : T), c.pattern t ≠ c'.pattern t

Distinct coarse rows force distinct patterns.