Choosing the edge-score parameters #
For fixed parameters, a good sample exists once the cubic graph is large. As the edge
correlation target increases to 2√2/3, the per-vertex straddling bound
(3/(2π)) arccos ((1 + 3ρ₀)/4) decreases to (3/(2π)) arccos ((1 + 2√2)/4); a fine grid with
small deviations brings every bag within any positive slack of that coefficient.
theorem
Algebraic.Cutwidth.Gaussian.Internal.exists_frontier_of_parameters
{q : ℝ}
(hq0 : 0 ≤ q)
(R : ℕ)
{ρ₀ : ℝ}
(hρ₀ : 17 / 32 ≤ ρ₀)
(hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R)
{T ε : ℝ}
(hT : 0 < T)
(hε : 0 < ε)
{M : ℕ}
(hM : 0 < M)
:
∃ (N₀ : ℕ),
∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj],
H.IsRegularOfDegree 3 →
N₀ < Fintype.card W →
∃ (D : PathDecomposition H),
∀ (k : Fin D.length), ↑(D.bag k).card ≤ frontierLayoutBound ρ₀ T ε M * ↑(Fintype.card W)
Fixed parameters. Every large cubic graph has an edge-score decomposition with bags
of at most frontierLayoutBound ρ₀ T ε M times the number of vertices.
The frontier ordering coefficient 2p is at most 9/32.
Parameters. For every positive slack some admissible parameters bring the edge-score bound within that slack of the frontier coefficient.
theorem
Algebraic.Cutwidth.Gaussian.Internal.exists_pathwidthBound_frontier
{ξ : ℝ}
(hξ : 0 < ξ)
:
∃ (N₀ : ℕ), PathwidthBound frontierCoefficient ξ N₀
The Gaussian cubic pathwidth bound.