Capacity of complete-event lineages #
At a fixed complete-event level, every selected lineage is killed. If all intervening event colors are at least that level's color, no lineage can return. A finite family of such events therefore has cardinality bounded by the initial node population.
theorem
EGZ.FlagDecomposition.Iteration.State.Event.exists_complete_of_color_eq
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : State p d f}
(E : s.Event)
{L : ℕ}
(hL : L < (d + 1) ^ 2)
(hcolor : E.color = 2 * L)
:
∃ (x : s.decomposition.flag.Node), E = complete x ∧ s.decomposition.level x = L
theorem
EGZ.FlagDecomposition.Iteration.card_complete_events_le_of_lineage
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
(D : LineageMassMaps fun (i : ℕ) => (s i).decomposition)
{L : ℕ}
(hcut : ∀ (i : ℕ), L ≤ D.cutoff i)
{E : Type u_1}
[Fintype E]
(time : E → ℕ)
(htime : Function.Injective time)
{ε : ℝ}
{δ : E → ℝ}
{g : ℕ → ℕ}
(P : (e : E) → Progress (s (time e)) (s (time e + 1)) ε (δ e) g)
(hstep : ∀ (e : E), D.step (time e) = (P e).subdivision)
(node : (e : E) → (s (time e)).decomposition.flag.Node)
(hevent : ∀ (e : E), (P e).event = State.Event.complete (node e))
(hlevel : ∀ (e : E), (s (time e)).decomposition.level (node e) = L)
:
Complete-event capacity only requires progress at the selected event times; all other comparisons may be identities after a finite endpoint.
theorem
EGZ.FlagDecomposition.Iteration.card_even_color_events_le_stopped
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
(n : ℕ)
(hstop : ∀ (i : ℕ), n ≤ i → s (i + 1) = s i)
(P : (i : ℕ) → i < n → Progress (s i) (s (i + 1)) ε (δ i) g)
{L : ℕ}
(hL : L < (d + 1) ^ 2)
(hcolors : ∀ (i : ℕ) (hi : i < n), 2 * L ≤ (P i hi).event.color)
{E : Type u_1}
[Fintype E]
(time : E → ℕ)
(htime : Function.Injective time)
(hbound : ∀ (e : E), time e < n)
(hcolor : ∀ (e : E), (P (time e) ⋯).event.color = 2 * L)
:
theorem
EGZ.FlagDecomposition.Iteration.card_complete_events_interval_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
{N : ℕ}
(P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g)
(χ : ℕ → ℕ)
(hχ : ∀ (i : ℕ) (hi : i < N), χ i = (P i hi).event.color)
{a b L : ℕ}
(hab : a ≤ b)
(hbN : b < N)
(hL : L < (d + 1) ^ 2)
(hcolors : ∀ i ∈ Finset.Icc a b, 2 * L ≤ χ i)
:
The number of complete events in an interval whose colors are all at least the selected color is bounded by the population at its left endpoint.
theorem
EGZ.FlagDecomposition.Iteration.card_complete_events_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
(P : (i : ℕ) → Progress (s i) (s (i + 1)) ε (δ i) g)
{L : ℕ}
(hcolors : ∀ (i : ℕ), 2 * L ≤ (P i).event.color)
{E : Type u_1}
[Fintype E]
(time : E → ℕ)
(htime : Function.Injective time)
(node : (e : E) → (s (time e)).decomposition.flag.Node)
(hevent : ∀ (e : E), (P (time e)).event = State.Event.complete (node e))
(hlevel : ∀ (e : E), (s (time e)).decomposition.level (node e) = L)
:
Distinct complete-event times at level L consume distinct initial
lineages. The argument uses only the certified resolution and parent data.
theorem
EGZ.FlagDecomposition.Iteration.card_even_color_events_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{s : ℕ → State p d f}
{ε : ℝ}
{δ : ℕ → ℝ}
{g : ℕ → ℕ}
(P : (i : ℕ) → Progress (s i) (s (i + 1)) ε (δ i) g)
{L : ℕ}
(hcolors : ∀ (i : ℕ), 2 * L ≤ (P i).event.color)
{E : Type u_1}
[Fintype E]
(hL : L < (d + 1) ^ 2)
(time : E → ℕ)
(htime : Function.Injective time)
(hcolor : ∀ (e : E), (P (time e)).event.color = 2 * L)
:
The finite family may be specified just by its complete-event color.