Gaussian layouts of cubic graphs

Every large loopless multigraph on h vertices in which every vertex has three edges, parallel edges allowed, has a layout of width at most (p + ξ) h, for every ξ > 0, where

p = (3 / (2π)) arccos ((1 + 2√2)/4) ≈ 0.14035

is Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient (Cslib.Circuits.Frontier.Gaussian.exists_width_le_gaussianCoefficient). In particular p is a cubic layout coefficient (Cslib.Circuits.Frontier.Gaussian.cubicLayoutBound_gaussian), and through the cubic quotient of a subcubic multigraph, 2p ≈ 0.2807 is a layout coefficient for maximum degree three (Cslib.Circuits.Frontier.layoutBound_gaussian).

The random layout. Give each vertex v its unit kernel row x_v (Cslib.Circuits.Frontier.Gaussian.unitKernelRow): the normalized vector of distance weights q ^ dist(v, z), truncated at radius R. Give each edge uv the unit vector y_uv in the direction of x_u + x_v. Draw a standard Gaussian vector ω and score each edge by ⟪y_e, ω⟫. List the vertices by the median of their three edge scores (Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_edgeScore).

One vertex. A vertex straddles a threshold when two of its edge scores fall on opposite sides. The three edge vectors at v have inner product at least √((1 + ρ)/2) with x_v, where ρ bounds the inner products of adjacent rows; by Sheppard's bound [She99] and the concavity of arccos in a spherical cap, v straddles any fixed threshold with probability at most (3 / (2π)) arccos ((1 + 3ρ)/4) (Cslib.Circuits.Frontier.Gaussian.measureReal_straddleEvent_le).

All thresholds at once. Each event depends only on the coordinates of ω in a ball of bounded radius, so each count of events has variance O(h) and is within ε h of its mean with probability 1 - O(1/h). For large h one sample keeps the straddling counts at a grid of thresholds, the window counts between them, and the tails near their means (Cslib.Circuits.Frontier.Gaussian.exists_good_sample); the median layout of that sample has width at most (p_ρ + O(δ) + O(ε) + O(1/T ^ 2)) h.

The limit. As q increases to 1/√2 and R grows, the adjacent correlation tends to 2√2/3, the neighbour correlation of Gaussian waves on the 3-regular tree, and (1 + 3 · 2√2/3)/4 = (1 + 2√2)/4. No girth assumption is needed.

Main results

• Cslib.Circuits.Frontier.Gaussian.exists_parameters: parameters bringing the width per vertex within any ξ > 0 of gaussianCoefficient.
• Cslib.Circuits.Frontier.Gaussian.exists_width_le_gaussianCoefficient: Gaussian layouts of loopless multigraphs whose vertices have three edges.
• Cslib.Circuits.Frontier.Gaussian.cubicLayoutBound_gaussian: the cubic layout bound with coefficient gaussianCoefficient.
• Cslib.Circuits.Frontier.Gaussian.exists_ncard_edgeCut_le: large cubic multigraphs have bisections, and more generally sets of any size, cut off by at most (gaussianCoefficient + ξ) |V| edges.
• Cslib.Circuits.Frontier.layoutBound_gaussian: the layout hypothesis for maximum degree three with coefficient 2 gaussianCoefficient.

References

• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation

Parameters

theorem Cslib.Circuits.Frontier.Gaussian.exists_decay_radius {ρ₀ : ℝ} (hρ₀ : ρ₀ < 2 * √2 / 3) : ∃ (q : ℝ) (R : ℕ), 0 ≤ q ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R

Decay rate and radius. Every ρ₀ < 2√2/3 admits a decay rate q ≥ 0 and a radius R with ρ₀ ≤ 2 q / (1 + q ^ 2) - 3 (2 q ^ 2) ^ R.

theorem Cslib.Circuits.Frontier.Gaussian.exists_parameters {ξ : ℝ} (hξ : 0 < ξ) : ∃ (q : ℝ) (R : ℕ) (ρ₀ : ℝ) (T : ℝ) (ε : ℝ) (M : ℕ), 0 ≤ q ∧ 1 / 8 ≤ ρ₀ ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R ∧ 0 < T ∧ 0 < ε ∧ 0 < M ∧ cubicBound ρ₀ T ε M ≤ gaussianCoefficient + ξ

Parameters. For every ξ > 0, some admissible parameters bring the width per vertex of a good sample within ξ of gaussianCoefficient.

The layout bounds

theorem Cslib.Circuits.Frontier.Gaussian.exists_width_le_gaussianCoefficient {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), ∀ (V : Type u_1) (E : Type u_2) [Finite V] [inst : Finite E] (G : Multigraph V E), G.Loopless → (∀ (v : V), (G.incidenceSet v).ncard = 3) → N₀ < Nat.card V → ∃ (σ : Layout V), ↑(G.width σ) ≤ (gaussianCoefficient + ξ) * ↑(Nat.card V)

Gaussian layouts of cubic multigraphs. For every ξ > 0, every large enough loopless multigraph in which every vertex has three edges, parallel edges allowed, has a layout of width at most (gaussianCoefficient + ξ) |V|.

theorem Cslib.Circuits.Frontier.Gaussian.cubicLayoutBound_gaussian : CubicLayoutBound gaussianCoefficient

Gaussian layouts of cubic graphs. For every ξ > 0, every large enough cubic graph on h vertices has a layout of width at most (gaussianCoefficient + ξ) h, where gaussianCoefficient = (3 / (2π)) arccos ((1 + 2√2)/4).

theorem Cslib.Circuits.Frontier.Gaussian.exists_ncard_edgeCut_le {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), ∀ (V : Type u_1) (E : Type u_2) [Finite V] [Finite E] (G : Multigraph V E), G.Loopless → (∀ (v : V), (G.incidenceSet v).ncard = 3) → N₀ < Nat.card V → ∀ k ≤ Nat.card V, ∃ (L : Set V), L.ncard = k ∧ ↑(G.edgeCut L).ncard ≤ (gaussianCoefficient + ξ) * ↑(Nat.card V)

Bisections of cubic multigraphs. For every ξ > 0, every large enough loopless multigraph whose vertices have three edges each, parallel edges allowed, has for every k ≤ |V| a set of k vertices cut off by at most (p + ξ) |V| edges, where p = (3/(2π)) arccos((1 + 2√2)/4) is gaussianCoefficient: take the first k vertices of a Gaussian layout. In particular its bisection width is at most (p + ξ) |V|, with p ≈ 0.1404.

theorem Cslib.Circuits.Frontier.layoutBound_gaussian : LayoutBound 3 (2 * Gaussian.gaussianCoefficient)

Gaussian layouts. Connected, loopless multigraphs of maximum degree three have layouts of width (2p + o(1)) β₁ + o(|V|), where β₁ is the cycle rank and p = (3 / (2π)) arccos ((1 + 2√2)/4), so 2p ≈ 0.2807.