Lineage systems associated with certified progress sequences

The progress certificate supplies every field of the geometric mass-map sequence. A lower bound on event colors supplies the uniform cutoff needed for low-level ancestor bookkeeping.

noncomputable def EGZ.FlagDecomposition.Iteration.lineageMassMaps {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) : LineageMassMaps fun (i : ℕ) => (s i).decomposition

The lineage mass maps induced by a sequence of iteration progress steps.

Equations

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

theorem EGZ.FlagDecomposition.Iteration.cutoff_ge_of_colors_ge {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 : ℕ} (h : ∀ (i : ℕ), 2 * L ≤ (P i).event.color) (i : ℕ) : L ≤ (lineageMassMaps P).cutoff i

theorem EGZ.FlagDecomposition.Iteration.card_nodes_le_pow {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) (n : ℕ) : Fintype.card (s n).decomposition.flag.Node ≤ 2 ^ n * Fintype.card (s 0).decomposition.flag.Node

The certified node-count recurrence gives the usual doubling bound.