Face events on a surviving lineage

A resolved face event cannot repeat along its surviving low-level lineage: parent injectivity identifies the surviving child with the resolved target, and composed subdivisions preserve realization. This is the geometric no-repeat input for the uniform face-chain bound.

theorem EGZ.Lineages.card_eventTimes_le_of_ordered_bound {R : Type u_1} [Fintype R] (T : Finset ℕ) (label : ℕ → R) (C : ℕ) (hlineage : ∀ (N : ℕ) (time : Fin (N + 1) ↪o ℕ), (∀ (i : Fin (N + 1)), time i ∈ T) → (∀ (i j : Fin (N + 1)), label (time i) = label (time j)) → N + 1 ≤ C) : T.card ≤ Fintype.card R * C

Count finite event times by their ancestor labels, using a bound for each increasing sequence of events with one common label.

theorem EGZ.FlagDecomposition.faceAtNode_carrier {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (Γ : (Φ.flag.polytope x).Face) (h : y = x) : (Φ.faceAtNode Γ h).carrier = ⋯ ▸ Γ.carrier

theorem EGZ.FlagDecomposition.SubdivisionMap.preimage_faceAtNode_congr {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} {S T : Φ.SubdivisionMap Ψ} (h : S = T) (z : Ψ.flag.Node) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (hS : S.node z = x) (hT : T.node z = x) : ⇑(S.fibre z) ⁻¹' (Φ.faceAtNode Γ hS).carrier = ⇑(T.fibre z) ⁻¹' (Φ.faceAtNode Γ hT).carrier

Changing the subdivision by an equality also changes its dependent source-node face by the same equality.

theorem EGZ.FlagDecomposition.SubdivisionMap.comp_isRealizedFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ Ω : FlagDecomposition p d f} (S : Φ.SubdivisionMap Ψ) (T : Ψ.SubdivisionMap Ω) (z : Ω.flag.Node) (Γ : (Φ.flag.polytope ((S.comp T).node z)).Face) (hne : ((Ω.flag.polytope z).carrier ∩ ⇑((S.comp T).fibre z) ⁻¹' Γ.carrier).Nonempty) (hresolved : ∀ (hfirst : ((Ψ.flag.polytope (T.node z)).carrier ∩ ⇑(S.fibre (T.node z)) ⁻¹' Γ.carrier).Nonempty), Ψ.IsRealizedFace (T.node z) (S.face (T.node z) Γ hfirst)) : Ω.IsRealizedFace z ((S.comp T).face z Γ hne)

A face which is realized after the first subdivision remains realized under a composite subdivision. Nonemptiness of the final pullback supplies nonemptiness of both intermediate pullbacks.

theorem EGZ.FlagDecomposition.Iteration.Progress.face_no_repeat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s t u : State p d f} {ε δ : ℝ} {g : ℕ → ℕ} (P : Progress s t ε δ g) (x : s.decomposition.flag.Node) (Γ : (s.decomposition.flag.polytope x).Face) (hevent : P.event = State.Event.face x Γ) (T : t.decomposition.SubdivisionMap u.decomposition) (z : u.decomposition.flag.Node) (hnode : P.subdivision.node (T.node z) = x) (hlevel : t.decomposition.level (T.node z) ≤ s.decomposition.level x) (Δ : (u.decomposition.flag.polytope z).Face) (hunrealized : ¬u.decomposition.IsRealizedFace z Δ) : (u.decomposition.flag.polytope z).carrier ∩ ⇑((P.subdivision.comp T).fibre z) ⁻¹' (s.decomposition.faceAtNode Γ hnode).carrier ≠ Δ.carrier

A later unrealized face cannot equal the pullback of a resolved face when the surviving child remains below the selected level.

theorem EGZ.FlagDecomposition.Iteration.State.Event.exists_face_of_color_eq {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} (E : s.Event) {L : ℕ} (h : E.color = 2 * L + 1) : ∃ (x : s.decomposition.flag.Node) (Γ : (s.decomposition.flag.polytope x).Face), E = face x Γ ∧ s.decomposition.level x = L

Odd operation colors identify face events and their exact level.

structure EGZ.FlagDecomposition.Iteration.FaceOccurrence {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} (D : LineageMassMaps fun (i : ℕ) => (s i).decomposition) (L : ℕ) (ε : ℝ) (δ : ℕ → ℝ) (g : ℕ → ℕ) (i : ℕ) : Type

One actual face event, matching the comparison system at its selected time. Progress is required only at these event times.

• progress : Progress (s i) (s (i + 1)) ε (δ i) g

  The transition in which the specified face event occurs.

• node : (s i).decomposition.flag.Node

  The node at level L supporting this face event.

• face : ((s i).decomposition.flag.polytope self.node).Face

  The face selected by this occurrence of the event.

• level_eq : (s i).decomposition.level self.node = L
• event_eq : self.progress.event = State.Event.face self.node self.face
• subdivision_eq : self.progress.subdivision = D.step i

@[reducible, inline]

abbrev EGZ.FlagDecomposition.Iteration.FaceOccurrence.lowNode {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {D : LineageMassMaps fun (i : ℕ) => (s i).decomposition} {L : ℕ} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {i : ℕ} (E : FaceOccurrence D L ε δ g i) : D.system.LowNode L i

Regard the occurrence's node as a node of level at most L.

Equations

• E.lowNode = ⟨E.node, ⋯⟩

theorem EGZ.FlagDecomposition.Iteration.FaceOccurrence.isLargeFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {D : LineageMassMaps fun (i : ℕ) => (s i).decomposition} {L : ℕ} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {i : ℕ} (E : FaceOccurrence D L ε δ g i) : (s i).decomposition.IsLargeFace ε E.node E.face

theorem EGZ.FlagDecomposition.Iteration.FaceOccurrence.not_isRealizedFace {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {D : LineageMassMaps fun (i : ℕ) => (s i).decomposition} {L : ℕ} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {i : ℕ} (E : FaceOccurrence D L ε δ g i) : ¬(s i).decomposition.IsRealizedFace E.node E.face

theorem EGZ.FlagDecomposition.Iteration.FaceOccurrence.transport_no_repeat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {D : LineageMassMaps fun (i : ℕ) => (s i).decomposition} {L : ℕ} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (E : FaceOccurrence D L ε δ g i) (F : FaceOccurrence D L ε δ g j) (hij : i < j) (heq : (D.system.ancestry ⋯ i) E.lowNode = (D.system.ancestry ⋯ j) F.lowNode) : have hnode := ⋯; ((s j).decomposition.flag.polytope F.node).carrier ∩ ⇑((D.transport hL ⋯).subdivision.fibre F.node) ⁻¹' ((s i).decomposition.faceAtNode E.face hnode).carrier ≠ F.face.carrier

Two ordered face occurrences with the same ancestor label cannot have equal faces after pulling the old face through the composed subdivision.

theorem EGZ.FlagDecomposition.Iteration.FaceOccurrence.massMap_no_repeat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {D : LineageMassMaps fun (i : ℕ) => (s i).decomposition} {L : ℕ} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (E : FaceOccurrence D L ε δ g i) (F : FaceOccurrence D L ε δ g j) (hij : i < j) (heq : (D.system.ancestry ⋯ i) E.lowNode = (D.system.ancestry ⋯ j) F.lowNode) : ((s j).decomposition.flag.polytope F.node).carrier ∩ ⇑(D.mapOfSameAncestry hL ⋯ E.lowNode F.lowNode heq).coord.real ⁻¹' E.face.carrier ≠ F.face.carrier

The same no-repeat statement expressed in the stable map's integer coordinate realization, ready for the face-chain counting theorem.

theorem EGZ.FlagDecomposition.Iteration.card_ordered_faceOccurrences_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} (D : LineageMassMaps fun (i : ℕ) => (s i).decomposition) (L : ℕ) (ε : ℝ) (δ : ℕ → ℝ) (g : ℕ → ℕ) {N : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) (hp : Odd p) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (time : Fin (N + 1) ↪o ℕ) (E : (i : Fin (N + 1)) → FaceOccurrence D L ε δ g (time i)) (hsame : ∀ (i j : Fin (N + 1)), (D.system.ancestry ⋯ (time i)) (E i).lowNode = (D.system.ancestry ⋯ (time j)) (E j).lowNode) (htail : ∀ (i : Fin (N + 1)), ↑(s (time i)).decomposition.retainedMass - ↑(s (time (Fin.last N))).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s (time i)).decomposition.retainedMass) : N + 1 ≤ faceCapacity d ε

Uniform bound for ordered face events on one persistent lineage. Only the finite selected times need actual progress certificates.

theorem EGZ.FlagDecomposition.Iteration.card_faceOccurrences_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} (D : LineageMassMaps fun (i : ℕ) => (s i).decomposition) (L : ℕ) (ε : ℝ) (δ : ℕ → ℝ) (g : ℕ → ℕ) (hL : ∀ (i : ℕ), L ≤ D.cutoff i) (hp : Odd p) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (T : Finset ℕ) (E : (i : ℕ) → i ∈ T → FaceOccurrence D L ε δ g i) (htail : ∀ i ∈ T, ∀ j ∈ T, i ≤ j → ↑(s i).decomposition.retainedMass - ↑(s j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s i).decomposition.retainedMass) : T.card ≤ Fintype.card (s 0).decomposition.flag.Node * faceCapacity d ε

Group a finite set of actual face events by initial ancestor. Each group is ordered by event time and bounded by faceCapacity.

theorem EGZ.FlagDecomposition.Iteration.card_face_events_interval_le {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} (L : ℕ) (ε : ℝ) (δ : ℕ → ℝ) (g : ℕ → ℕ) {N a b : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (χ : ℕ → ℕ) (hχ : ∀ (i : ℕ) (hi : i < N), χ i = (P i hi).event.color) (hab : a ≤ b) (hbN : b < N) (hp : Odd p) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hcolors : ∀ i ∈ Finset.Icc a b, 2 * L + 1 ≤ χ i) (htail : ∀ (i j : ℕ), i ≤ j → j ≤ N → ↑(s i).decomposition.retainedMass - ↑(s j).decomposition.retainedMass ≤ ε ^ 2 / 4 * ↑(s i).decomposition.retainedMass) : {i ∈ Finset.Icc a b | χ i = 2 * L + 1}.card ≤ Fintype.card (s a).decomposition.flag.Node * faceCapacity d ε

Face-color capacity on a genuinely finite progress interval. The comparison sequence is restarted at a and extended by identities after b + 1; no progress is required outside the finite run.