Counting large faces along a stable lineage

Coherent injective coordinate maps place all lineage polytopes in the first coordinate space. Stable node maps transport their masses and bound their loss by global mass loss. Passing to the final cumulative weight then gives the uniform common-measure large-face bound.

theorem EGZ.FlagDecomposition.cumulativeMass_le_retainedMass {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : natMass (Φ.cumulativeWeight x) ≤ Φ.retainedMass

theorem EGZ.FlagDecomposition.liftedMassOn_pos_nonempty {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (S : Set (RealCoord (Φ.flag.rank x))) (hS : 0 < Φ.liftedMassOn x S) : ((Φ.flag.polytope x).carrier ∩ S).Nonempty

Positive lifted mass witnesses an actual point of the node polytope.

theorem EGZ.FlagDecomposition.NodeMassMap.weightedMass_image {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.NodeMassMap Ψ x y) (hp : Odd p) (hM : Function.Injective ⇑M.coord.real) (S : Set (RealCoord (Ψ.flag.rank y))) : WeightedIncidence.mass (fun (v : FpCoord p d) => ↑(Ψ.cumulativeWeight y v)) ((fun (v : FpCoord p d) => ((Φ.representation.map x) v).centeredLift.real) ⁻¹' ⇑M.coord.real '' S) = ↑(Ψ.liftedMassOn y S)

Express image-set mass in the original node's centered coordinates.

theorem EGZ.FlagDecomposition.StableNodeMap.cumulativeMass_loss_nonneg {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.StableNodeMap Ψ x y) : 0 ≤ ↑(natMass (Φ.cumulativeWeight x)) - ↑(natMass (Ψ.cumulativeWeight y))

theorem EGZ.FlagDecomposition.StableNodeMap.retainedMass_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.StableNodeMap Ψ x y) : Ψ.retainedMass ≤ Φ.retainedMass

theorem EGZ.FlagDecomposition.StableNodeMap.largeFace_preimage_nonempty {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {x : Φ.flag.Node} {y : Ψ.flag.Node} (M : Φ.StableNodeMap Ψ x y) (hp : Odd p) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (Γ : (Φ.flag.polytope x).Face) (hlarge : Φ.IsLargeFace ε x Γ) (htail : ↑Φ.retainedMass - ↑Ψ.retainedMass ≤ ε ^ 2 / 4 * ↑Φ.retainedMass) : ((Ψ.flag.polytope y).carrier ∩ ⇑M.coord.real ⁻¹' Γ.carrier).Nonempty

The tail estimate ensures that every old large face has a nonempty pullback in a later node polytope. This supplies the nonemptiness needed when applying preservation of realized faces.

theorem EGZ.largeFaceBound_mono_dimension {ε : ℝ} (hε : 0 < ε) {r d : ℕ} (hrd : r ≤ d) : ((ε ^ 3)⁻¹ + ↑r + 2) ^ (r + 2) ≤ ((ε ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)

The explicit large-face bound is monotone in the ambient dimension.

theorem EGZ.FlagDecomposition.card_largeFaceChain_le {p d N : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : Fin (N + 1) → FlagDecomposition p d f) (x : (i : Fin (N + 1)) → (Φ i).flag.Node) (M : {i j : Fin (N + 1)} → i ≤ j → (Φ i).StableNodeMap (Φ j) (x i) (x j)) (hinj : ∀ {i j : Fin (N + 1)} (h : i ≤ j), Function.Injective ⇑(M h).coord.real) (hcomp : ∀ {i j k : Fin (N + 1)} (hij : i ≤ j) (hjk : j ≤ k), (M ⋯).coord = (M hij).coord.comp (M hjk).coord) (hp : Odd p) (ε : ℝ) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (Γ : (i : Fin (N + 1)) → ((Φ i).flag.polytope (x i)).Face) (hlarge : ∀ (i : Fin (N + 1)), (Φ i).IsLargeFace ε (x i) (Γ i)) (hdistinct : ∀ (i j : Fin (N + 1)) (hij : i < j), ((Φ j).flag.polytope (x j)).carrier ∩ ⇑(M ⋯).coord.real ⁻¹' (Γ i).carrier ≠ (Γ j).carrier) (htail : ∀ (i : Fin (N + 1)), ↑(Φ i).retainedMass - ↑(Φ (Fin.last N)).retainedMass ≤ ε ^ 2 / 4 * ↑(Φ i).retainedMass) : ↑(N + 1) ≤ (((ε / 2) ^ 3)⁻¹ + ↑d + 2) ^ (d + 2)

The face-counting step for one surviving lineage. Coordinate injectivity and the pullback no-repeat condition are explicit geometric inputs; all common-measure and dimension bookkeeping is proved here.