Lineages of nodes below a fixed level

Parent maps which do not increase level backwards, and are injective on the low-level nodes, embed every later low-level population in the initial one. Event counts therefore reduce to counts for initial ancestor labels. A killed lineage cannot label any later event.

structure EGZ.Lineages.System : Type (u + 1)

The abstract data needed for lineage bookkeeping. No geometric properties of the nodes or parent maps are assumed.

• Node : ℕ → Type u

  The finite node type at each stage of the lineage system.

• finiteNode (i : ℕ) : Fintype (self.Node i)
• level (i : ℕ) : self.Node i → ℕ

  The level assigned to each node at its stage.

• parent (i : ℕ) : self.Node (i + 1) → self.Node i

  The predecessor of a node in the preceding stage.

• level_parent (i : ℕ) (x : self.Node (i + 1)) : self.level i (self.parent i x) ≤ self.level (i + 1) x

@[reducible, inline]

abbrev EGZ.Lineages.System.LowNode (S : System) (L i : ℕ) : Type u_1

Nodes at or below the chosen level cutoff.

Equations

• S.LowNode L i = { x : S.Node i // S.level i x ≤ L }

def EGZ.Lineages.System.InjectiveBelow (S : System) (L : ℕ) : Prop

Later low-level nodes have distinct old parents.

Equations

• S.InjectiveBelow L = ∀ (i : ℕ), Set.InjOn (S.parent i) {x : S.Node (i + 1) | S.level (i + 1) x ≤ L}

def EGZ.Lineages.System.parentEmbedding (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) : S.LowNode L (i + 1) ↪ S.LowNode L i

The restricted parent map is an embedding.

Equations

• S.parentEmbedding hinj i = { toFun := fun (x : S.LowNode L (i + 1)) => ⟨S.parent i ↑x, ⋯⟩, inj' := ⋯ }

@[simp]

theorem EGZ.Lineages.System.parentEmbedding_val (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) (x : S.LowNode L (i + 1)) : ↑((S.parentEmbedding hinj i) x) = S.parent i ↑x

def EGZ.Lineages.System.ancestor (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {i j : ℕ} (h : i ≤ j) : S.LowNode L j ↪ S.LowNode L i

Follow a low-level node back to any earlier stage.

Equations

• S.ancestor hinj h = Nat.leRecOn h (fun {k : ℕ} (e : S.LowNode L k ↪ S.LowNode L i) => (S.parentEmbedding hinj k).trans e) (Function.Embedding.refl (S.LowNode L i))

@[simp]

theorem EGZ.Lineages.System.ancestor_self (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) : S.ancestor hinj ⋯ = Function.Embedding.refl (S.LowNode L i)

theorem EGZ.Lineages.System.ancestor_succ (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {i j : ℕ} (h : i ≤ j) : S.ancestor hinj ⋯ = (S.parentEmbedding hinj j).trans (S.ancestor hinj h)

theorem EGZ.Lineages.System.ancestor_trans (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : S.LowNode L k) : (S.ancestor hinj hij) ((S.ancestor hinj hjk) x) = (S.ancestor hinj ⋯) x

Following parents in two stages agrees with following them directly.

def EGZ.Lineages.System.ancestry (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) : S.LowNode L i ↪ S.LowNode L 0

The original low-level ancestor labels each surviving lineage.

Equations

• S.ancestry hinj i = S.ancestor hinj ⋯

@[simp]

theorem EGZ.Lineages.System.ancestry_zero (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) : S.ancestry hinj 0 = Function.Embedding.refl (S.LowNode L 0)

@[simp]

theorem EGZ.Lineages.System.ancestry_succ (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) (x : S.LowNode L (i + 1)) : (S.ancestry hinj (i + 1)) x = (S.ancestry hinj i) ((S.parentEmbedding hinj i) x)

theorem EGZ.Lineages.System.ancestry_ancestor (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {i j : ℕ} (h : i ≤ j) (x : S.LowNode L j) : (S.ancestry hinj i) ((S.ancestor hinj h) x) = (S.ancestry hinj j) x

theorem EGZ.Lineages.System.card_lowNode_le_initial (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (i : ℕ) : Fintype.card (S.LowNode L i) ≤ Fintype.card (S.Node 0)

def EGZ.Lineages.System.IsKilled (S : System) {L : ℕ} (i : ℕ) (x : S.LowNode L i) : Prop

A selected node is killed when it has no child below the cutoff in the next stage. Higher-level replacements are permitted.

Equations

• S.IsKilled i x = ∀ (y : S.LowNode L (i + 1)), S.parent i ↑y ≠ ↑x

theorem EGZ.Lineages.System.ancestry_ne_of_killed (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {i j : ℕ} (hij : i < j) (x : S.LowNode L i) (y : S.LowNode L j) (hx : S.IsKilled i x) : (S.ancestry hinj i) x ≠ (S.ancestry hinj j) y

Killing a lineage prevents its ancestor label from appearing later.

def EGZ.Lineages.System.eventLabel (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {E : Type u_1} (time : E → ℕ) (selected : (e : E) → S.LowNode L (time e)) (e : E) : S.Node 0

Label an event by the original ancestor of its selected low-level node.

Equations

• S.eventLabel hinj time selected e = ↑((S.ancestry hinj (time e)) (selected e))

theorem EGZ.Lineages.System.card_events_le (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {E : Type u_1} [Fintype E] (time : E → ℕ) (selected : (e : E) → S.LowNode L (time e)) (C : ℕ) (hcount : ∀ (r : S.Node 0), {e : E | S.eventLabel hinj time selected e = r}.card ≤ C) : Fintype.card E ≤ Fintype.card (S.Node 0) * C

A uniform bound per ancestor gives a total event bound.

theorem EGZ.Lineages.System.eventLabel_injective_of_killed (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {E : Type u_1} (time : E → ℕ) (selected : (e : E) → S.LowNode L (time e)) (htime : Function.Injective time) (hkilled : ∀ (e : E), S.IsKilled (time e) (selected e)) : Function.Injective (S.eventLabel hinj time selected)

Events at distinct times which kill their selected lineage have distinct original ancestor labels.

theorem EGZ.Lineages.System.card_killed_events_le (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) {E : Type u_1} [Fintype E] (time : E → ℕ) (selected : (e : E) → S.LowNode L (time e)) (htime : Function.Injective time) (hkilled : ∀ (e : E), S.IsKilled (time e) (selected e)) : Fintype.card E ≤ Fintype.card (S.Node 0)

There is at most one killing event for each initial lineage.

def EGZ.Lineages.System.shift (S : System) (start : ℕ) : System

Restart the bookkeeping at any stage, as needed for a color interval.

Equations

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

theorem EGZ.Lineages.System.injectiveBelow_shift (S : System) {L : ℕ} (hinj : S.InjectiveBelow L) (start : ℕ) : (S.shift start).InjectiveBelow L