From vertex scores to every prefix cut

A finite grid of threshold cuts, together with vertex window and tail counts, controls every prefix of a vertex-score ordering. Ties are broken by a fixed enumeration and are charged to the same window as the tied score.

theorem Complexity.Frontier.card_incidence_biUnion_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (degree : ∀ (v : W), H.degree v ≤ d) (S : Finset W) : (S.biUnion fun (v : W) => H.incidenceFinset v).card ≤ d * S.card

At most d |S| edges have an endpoint in S.

theorem Complexity.Frontier.card_cut_le_grid {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (degree : ∀ (v : W), H.degree v ≤ d) (score : W → ℝ) (P : Finset W) {m a δ : ℝ} (hP : ∀ v ∈ P, score v ≤ m) (hPc : ∀ v ∉ P, m ≤ score v) (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : ↑d * ↑{v : W | score v < a}.card ≤ B) (high : ↑d * ↑{v : W | a + ↑M * δ ≤ score v}.card ≤ B) (mid : ∀ i < M, ↑(H.crossingFinset {v : W | score v < a + ↑i * δ}).card + ↑d * ↑{v : W | a + ↑i * δ ≤ score v ∧ score v < a + (↑i + 1) * δ}.card ≤ B) : ↑(H.crossingFinset P).card ≤ B

A score-separated cut is controlled by the neighboring grid cut and the vertices in the intervening score window.

theorem Complexity.Frontier.exists_key_of_vertexScore {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {d : ℕ} (degree : ∀ (v : W), H.degree v ≤ d) (score : W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : ↑d * ↑{v : W | score v < a}.card ≤ B) (high : ↑d * ↑{v : W | a + ↑M * δ ≤ score v}.card ≤ B) (mid : ∀ i < M, ↑(H.crossingFinset {v : W | score v < a + ↑i * δ}).card + ↑d * ↑{v : W | a + ↑i * δ ≤ score v ∧ score v < a + (↑i + 1) * δ}.card ≤ B) : ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.crossingFinset {v : W | key v < t}).card ≤ B

Sorting vertex scores converts grid, window, and tail estimates into an actual layout.