Layouts from scores

Sorting the vertices by a score, with ties broken by a fixed numbering, gives a layout every initial segment of which is a threshold set of the score: some m is at least every score inside it and at most every score outside it (Cslib.Circuits.Frontier.Layout.exists_threshold). Which window of a grid a, a + δ, ..., a + M δ a threshold falls in is decided by Cslib.Circuits.Frontier.exists_grid_index. Both turn estimates at the grid thresholds into bounds on every frontier of the layouts by Gaussian scores.

Main results

• Cslib.Circuits.Frontier.Layout.exists_threshold: the layout by a score.
• Cslib.Circuits.Frontier.exists_grid_index: the grid window of a threshold.
• Cslib.Circuits.Frontier.Multigraph.width_le_of_ncard_frontier_le: bounding the width by a real bound on the frontiers.

theorem Cslib.Circuits.Frontier.Layout.exists_threshold {V : Type u_1} [Finite V] {α : Type u_2} [LinearOrder α] (score : V → α) : ∃ (π : Layout V), ∀ t < Nat.card V, ∃ (m : α), (∀ v ∈ π.initial t, score v ≤ m) ∧ ∀ v ∉ π.initial t, m ≤ score v

Sorting by a score. Listing the vertices in increasing order of a score, with ties broken by a fixed numbering, gives a layout whose initial segments are threshold sets: for t < |V|, some m is at least the score of every vertex among the first t and at most the score of every other vertex.

theorem Cslib.Circuits.Frontier.exists_grid_index {a δ m : ℝ} (hδ : 0 < δ) {M : ℕ} (hlo : a ≤ m) (hhi : m < a + ↑M * δ) : ∃ i < M, a + ↑i * δ ≤ m ∧ m < a + (↑i + 1) * δ

Grid windows. A real number in [a, a + M δ) lies in one of the M windows [a + i δ, a + (i + 1) δ).

theorem Cslib.Circuits.Frontier.Multigraph.width_le_of_ncard_frontier_le {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (π : Layout V) [Finite E] {B : ℝ} (hB : 0 ≤ B) (h : ∀ t < Nat.card V, ↑(G.frontier π t).ncard ≤ B) : ↑(G.width π) ≤ B

A nonnegative real bound on the frontiers before the last vertex bounds the width.