A finished bounded state supplies the public decomposition conclusion

theorem EGZ.FlagDecomposition.Iteration.State.hasConclusion {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (s : State p d f) (hp : Nat.Prime p) {ε δ : ℝ} {g : ℕ → ℕ} {Bcard BK : ℕ} (h : s.Finished ε δ g) (hcard : Fintype.card s.decomposition.flag.Node ≤ Bcard) (hK : s.radius ≤ BK) (hmass : (1 - ε) * ↑(natMass f) ≤ ↑s.decomposition.retainedMass) : HasFlagDecompositionConclusion hp f ε δ g Bcard BK

theorem EGZ.FlagDecomposition.Iteration.BoundedState.hasConclusion {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) (hp : Nat.Prime p) (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hi : i ≤ stoppingBound d ε) (hfinished : s.Finished ε (stageScale d ε i) g) : HasFlagDecompositionConclusion hp f ε (finalScale d ε) g (2 ^ stoppingBound d ε) (P.radiusHorizon 1 (stoppingBound d ε))