Gaussian cycle-rank coefficients in every fixed degree

Saturated compression and Gaussian vertex layouts give the layout hypothesis for maximum degree d ≥ 3 with coefficient

A_d = (3d / (2d - 3)) · arccos (2 √(d - 1) / d) / π

(Cslib.Circuits.Frontier.layoutBound_degree). Let G be a connected multigraph of maximum degree d with cycle rank β₁. A saturated compression of G with budget d has a core, its quotient, with at most 3d β₁ / (2d - 3) edges and at most as many blocks (Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.mul_card_external_le). Gaussian vertex layouts give the core a layout of width vertexCoefficient d · |E(core)| + o(|blocks|) (Cslib.Circuits.Frontier.Gaussian.exists_width_le_vertexCoefficient), and expanding it costs d log₂ |V| edges at each frontier.

At d = 3 the coefficient 3 arccos (2√2/3) / π ≈ 0.3245 is at most 1/3 (Cslib.Circuits.Frontier.Gaussian.degreeCoefficient_three_le), so the layout hypothesis for maximum degree three holds with coefficient 1/3 (Cslib.Circuits.Frontier.layoutBound_one_third).

Main definitions

• Cslib.Circuits.Frontier.Gaussian.degreeCoefficient: the coefficient A_d.

Main results

• Cslib.Circuits.Frontier.Gaussian.degreeCoefficient_three_le: A_3 ≤ 1/3.
• Cslib.Circuits.Frontier.layoutBound_degree: the layout hypothesis for maximum degree d ≥ 3 with coefficient A_d.
• Cslib.Circuits.Frontier.layoutBound_one_third: the layout hypothesis for maximum degree three with coefficient 1/3.

noncomputable def Cslib.Circuits.Frontier.Gaussian.degreeCoefficient (d : ℕ) : ℝ

The layout coefficient A_d = (3d / (2d - 3)) · arccos (2 √(d - 1) / d) / π of saturated compression and Gaussian vertex scores in maximum degree d.

theorem Cslib.Circuits.Frontier.Gaussian.vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) : vertexCorrelation d < 1

The limiting adjacent correlation 2 √(d - 1) / d is less than one for d ≥ 3.

theorem Cslib.Circuits.Frontier.Gaussian.vertexCoefficient_pos {d : ℕ} (hd : 3 ≤ d) : 0 < vertexCoefficient d

theorem Cslib.Circuits.Frontier.Gaussian.degreeCoefficient_pos {d : ℕ} (hd : 3 ≤ d) : 0 < degreeCoefficient d

theorem Cslib.Circuits.Frontier.Gaussian.degreeCoefficient_three_le : degreeCoefficient 3 ≤ 1 / 3

In degree three the coefficient 3 arccos (2√2/3) / π ≈ 0.3245 is at most 1/3, since cos (π/9) ≤ 2√2/3.

theorem Cslib.Circuits.Frontier.layoutBound_degree {d : ℕ} (hd : 3 ≤ d) : LayoutBound d (Gaussian.degreeCoefficient d)

Gaussian vertex-score layouts. For d ≥ 3, connected, loopless multigraphs of maximum degree d have layouts of width (A_d + o(1)) β₁ + o(|V|), where β₁ is the cycle rank and A_d = (3d / (2d - 3)) · arccos (2 √(d - 1) / d) / π is Gaussian.degreeCoefficient d.

theorem Cslib.Circuits.Frontier.layoutBound_one_third : LayoutBound 3 (1 / 3)

The layout hypothesis with coefficient one third for maximum degree three, from Gaussian vertex-score layouts: A_3 = 3 arccos (2√2/3) / π ≤ 1/3.