Primes of a stable family

A complete prime is a configuration that is the history of one of its own events, so a set with a greatest element. Ordered by inclusion, with conflict given by incompatibility, the complete primes form a prime event structure with the same configurations.

def Stable.CoincidenceFree {L : Type u_1} (F : ConfFamily L) : Prop

Distinct events of a configuration are separated by a subconfiguration.

Equations

• Stable.CoincidenceFree F = ∀ {c : Set F.Event}, F.Config c → ∀ {x y : F.Event}, x ∈ c → y ∈ c → x ≠ y → ∃ (m : Set F.Event), F.Config m ∧ m ⊆ c ∧ (x ∈ m ↔ y ∉ m)

theorem Stable.coincidenceFree_ges {L : Type u_1} (G : GES L) : CoincidenceFree G.toFamily

Every general event structure is coincidence-free: rank separates two distinct events of a configuration.

theorem Stable.hist_finite {L : Type u_1} (G : GES L) (hF : Stable G.toFamily) {c : Set G.Event} (hc : G.isConf c) {x : G.Event} (hx : x ∈ c) : (hist G.toFamily c x).Finite

Histories in a general event structure are finite.

def Stable.IsPrime {L : Type u_1} (F : ConfFamily L) (p : Set F.Event) : Prop

A complete prime: a configuration which is the history of one of its events.

Equations

• Stable.IsPrime F p = (F.Config p ∧ ∃ x ∈ p, p = Stable.hist F p x)

def Stable.Prime {L : Type u_1} (F : ConfFamily L) : Type u_2

The complete primes, ordered by inclusion.

Equations

• Stable.Prime F = { p : Set F.Event // Stable.IsPrime F p }

@[instance_reducible]

instance Stable.instPartialOrderPrime {L : Type u_1} {F : ConfFamily L} : PartialOrder (Prime F)

Equations

• Stable.instPartialOrderPrime = Subtype.partialOrder fun (p : Set F.Event) => Stable.IsPrime F p

theorem Stable.Prime.config {L : Type u_1} {F : ConfFamily L} (p : Prime F) : F.Config ↑p

@[simp]

theorem Stable.Prime.le_iff {L : Type u_1} {F : ConfFamily L} {p q : Prime F} : p ≤ q ↔ ↑p ⊆ ↑q

noncomputable def Stable.Prime.top {L : Type u_1} {F : ConfFamily L} (p : Prime F) : F.Event

The greatest element of a complete prime.

Equations

• p.top = Classical.choose ⋯

theorem Stable.Prime.top_mem {L : Type u_1} {F : ConfFamily L} (p : Prime F) : p.top ∈ ↑p

theorem Stable.Prime.eq_hist_top {L : Type u_1} {F : ConfFamily L} (p : Prime F) : ↑p = hist F (↑p) p.top

theorem Stable.Prime.eq_top {L : Type u_1} {F : ConfFamily L} (hcf : CoincidenceFree F) (p : Prime F) {y : F.Event} (hy : y ∈ ↑p) (hh : ↑p = hist F (↑p) y) : y = p.top

Any event witnessing primeness is the greatest one.

def Stable.Compat {L : Type u_1} {F : ConfFamily L} (p q : Prime F) : Prop

Two primes are compatible when a single configuration contains both.

Equations

• Stable.Compat p q = ∃ (c : Set F.Event), F.Config c ∧ ↑p ⊆ c ∧ ↑q ⊆ c

theorem Stable.compat_self {L : Type u_1} {F : ConfFamily L} (p : Prime F) : Compat p p

theorem Stable.Compat.symm {L : Type u_1} {F : ConfFamily L} {p q : Prime F} : Compat p q → Compat q p

@[reducible]

noncomputable def Stable.toPES {L : Type u_1} (F : ConfFamily L) : PES L

The prime event structure of complete primes.

Equations

• One or more equations did not get rendered due to their size.

theorem Stable.hist_hist {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) {x : F.Event} (hx : x ∈ c) : hist F c x = hist F (hist F c x) x

A history is its own history.

theorem Stable.isPrime_hist {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) {x : F.Event} (hx : x ∈ c) : IsPrime F (hist F c x)

Inside a configuration, every history is a complete prime.

noncomputable def Stable.histPrime {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) {x : F.Event} (hx : x ∈ c) : Prime F

The history of x in c, as a prime.

Equations

• hF.histPrime hc hx = ⟨Stable.hist F c x, ⋯⟩

theorem Stable.prime_val_finite {L : Type u_1} (G : GES L) (hF : Stable G.toFamily) (p : Prime G.toFamily) : (↑p).Finite

Complete primes have finite carriers.

Agreement of configurations

def Stable.primesOf {L : Type u_1} (F : ConfFamily L) (c : Set F.Event) : Set (Prime F)

The primes below a set of events.

Equations

• Stable.primesOf F c = {p : Stable.Prime F | ↑p ⊆ c}

def Stable.flatten {L : Type u_1} (F : ConfFamily L) (S : Set (Prime F)) : Set F.Event

The events covered by a set of primes.

Equations

• Stable.flatten F S = ⋃ p ∈ S, ↑p

theorem Stable.subset_flatten {L : Type u_1} {F : ConfFamily L} {S : Set (Prime F)} {p : Prime F} (hp : p ∈ S) : ↑p ⊆ flatten F S

theorem Stable.primesOf_isConf {L : Type u_1} {F : ConfFamily L} {c : Set F.Event} (hc : F.Config c) : isConf (toPES F) (primesOf F c)

Configurations map to configurations.

theorem Stable.mem_flatten_primesOf {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) {x : F.Event} (hx : x ∈ c) : x ∈ flatten F (primesOf F c)

Every event of a configuration is the top of a prime inside it.

theorem Stable.flatten_primesOf {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) : flatten F (primesOf F c) = c

Flattening recovers the configuration.

theorem Stable.eq_hist_of_subset {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {c : Set F.Event} (hc : F.Config c) {p : Prime F} (hp : ↑p ⊆ c) : ↑p = hist F c p.top

Inside a configuration, a prime is the history of its top.

theorem Stable.toPES_finitary {L : Type u_1} (G : GES L) (hF : Stable G.toFamily) (p : (toPES G.toFamily).Event) : ((toPES G.toFamily).past p).Finite

The prime event structure of complete primes has finite causes.

theorem Stable.primesOf_flatten {L : Type u_1} {F : ConfFamily L} (hF : Stable F) {S : Set (Prime F)} (hS : isConf (toPES F) S) (hflat : F.Config (flatten F S)) : primesOf F (flatten F S) = S

A set of primes whose union is a configuration is recovered from it.

theorem Stable.label_histPrime {L : Type u_1} {F : ConfFamily L} (hF : Stable F) (hcf : CoincidenceFree F) {c : Set F.Event} (hc : F.Config c) {x : F.Event} (hx : x ∈ c) : (toPES F).label (histPrime ⋯ hc hx) = F.label x

The label of a history-prime is the label of the event it is the history of.

Firing one prime

Adding an enabled prime to a configuration adds exactly one event, its top.

theorem Stable.histPrime_lt {L : Type u_1} {F : ConfFamily L} (hF : Stable F) (hcf : CoincidenceFree F) (p : Prime F) {t : F.Event} (ht : t ∈ ↑p) (hne : t ≠ p.top) : histPrime ⋯ ⋯ ht < p

A non-top event of a prime is the top of a strictly smaller prime.

theorem Stable.val_subset_flatten {L : Type u_1} {F : ConfFamily L} (hF : Stable F) (hcf : CoincidenceFree F) {c : Set (Prime F)} {p : Prime F} (hpast : ∀ q < p, q ∈ c) : ↑p ⊆ flatten F c ∪ {p.top}

Every event of an enabled prime other than its top is already present.

theorem Stable.flatten_insert {L : Type u_1} {F : ConfFamily L} (hF : Stable F) (hcf : CoincidenceFree F) {c : Set (Prime F)} {p : Prime F} (hpast : ∀ q < p, q ∈ c) : flatten F (c ∪ {p}) = flatten F c ∪ {p.top}

Firing a prime adds exactly its top.