Extracting the decomposition from the bounded iteration

theorem EGZ.FlagDecomposition.Iteration.boundedRun.hasConclusion_of_capacity {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) {ε : ℝ} (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hg : Monotone g) (hf : f ≠ 0) (hprime : P.primeHorizon 1 (stoppingBound d ε) < p) (hp : Nat.Prime p) (hcapacity : ∀ (Q : (i : ℕ) → i < stoppingBound d ε → Progress (state P hd hε hεhalf hg hf (stoppingBound d ε) hprime i) (state P hd hε hεhalf hg hf (stoppingBound d ε) hprime (i + 1)) ε (stageScale d ε i) g), HasIntervalCapacity (progressColor Q) (intervalCapacity d ε) (stoppingBound d ε)) : HasFlagDecompositionConclusion hp f ε (finalScale d ε) g (2 ^ stoppingBound d ε) (P.radiusHorizon 1 (stoppingBound d ε))

The interval-capacity theorem rules out a full horizon of unfinished steps, so one of the actual bounded states supplies the public conclusion.