A gap cleanup cannot be followed by another gap cleanup

theorem EGZ.FlagDecomposition.Iteration.State.GapCondition.mono_delta {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {s : State p d f} {δ δ' : ℝ} (h : s.GapCondition δ) (hδ' : 0 ≤ δ') (hδ : δ' ≤ δ) : s.GapCondition δ'

theorem EGZ.FlagDecomposition.Iteration.State.Event.eq_gap_of_color_ge {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : State p d f} (E : s.Event) (h : 2 * (d + 1) ^ 2 ≤ E.color) : E = gap

theorem EGZ.FlagDecomposition.Iteration.no_consecutive_gap {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) (Q : Progress t u ε δ' g) (hδ' : 0 ≤ δ') (hδ : δ' ≤ δ) : ¬(P.event = State.Event.gap ∧ Q.event = State.Event.gap)

theorem EGZ.FlagDecomposition.Iteration.card_gap_interval_le_one {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {s : ℕ → State p d f} {ε : ℝ} {δ : ℕ → ℝ} {g : ℕ → ℕ} {N a b : ℕ} (P : (i : ℕ) → i < N → Progress (s i) (s (i + 1)) ε (δ i) g) (hδ : Antitone δ) (hδnonneg : ∀ (i : ℕ), 0 ≤ δ i) (hab : a ≤ b) (hb : b < N) (hcolor : ∀ (i : ℕ) (hi : i ∈ Finset.Icc a b), 2 * (d + 1) ^ 2 ≤ (P i ⋯).event.color) : (Finset.Icc a b).card ≤ 1

An interval consisting only of gap colors contains a single stage.