Ordering multigraph vertices by scores #
Grid cuts and vertex windows control every prefix, with each parallel edge counted.
theorem
Complexity.Frontier.Multigraph.card_cut_le_grid
{W E : Type}
[Fintype W]
[Fintype E]
(G : Multigraph W E)
{d : ℕ}
(degree : G.MaxDegreeLE 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,
↑(G.crossingFinset {v : W | score v < a + ↑i * δ}).card + ↑d * ↑{v : W | a + ↑i * δ ≤ score v ∧ score v < a + (↑i + 1) * δ}.card ≤ B)
:
The finite-grid argument also counts parallel edges.
theorem
Complexity.Frontier.Multigraph.exists_key_of_vertexScore
{W E : Type}
[Fintype W]
[Fintype E]
(G : Multigraph W E)
{d : ℕ}
(degree : G.MaxDegreeLE 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,
↑(G.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 : ℕ), ↑(G.crossingFinset {v : W | key v < t}).card ≤ B
Sorting scores yields a layout without a distinct-score hypothesis.