Documentation

Complexitylib.Circuits.Frontier.Layouts.BoundedDegree

Gaussian cycle-rank constants in every fixed degree #

Terminal compression and Gaussian vertex ordering give A_d = 3d/(2d-3) * arccos(2 sqrt(d-1)/d)/pi for every fixed d ≥ 3. All multigraph edges are retained in both the compression and the probabilistic proof.

source
noncomputable def Complexity.Frontier.Gaussian.degreeCoefficient (d : ℕ) :
ℝ

The cycle-rank coefficient obtained from terminal compression and vertex scores.

Equations
Instances For
    source
    theorem Complexity.Frontier.Gaussian.vertexCorrelation_lt_one {d : ℕ} (hd : 3 ≤ d) :
    vertexCorrelation d < 1
    source
    theorem Complexity.Frontier.Gaussian.vertexCoefficient_pos {d : ℕ} (hd : 3 ≤ d) :
    0 < vertexCoefficient d
    source
    theorem Complexity.Frontier.Gaussian.degreeCoefficient_pos {d : ℕ} (hd : 3 ≤ d) :
    0 < degreeCoefficient d
    source
    theorem Complexity.Frontier.Gaussian.degreeCoefficient_four :
    degreeCoefficient 4 = 2 / 5
    source
    theorem Complexity.Frontier.Gaussian.degreeCoefficient_lt_three_quarters {d : ℕ} (hd : 3 ≤ d) :
    degreeCoefficient d < 3 / 4

    The coefficients are uniformly below 3/4, improving coefficient one in every degree.

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

    The general-degree Gaussian layout theorem.