Documentation

Complexitylib.Circuits.Frontier.Layouts.VertexParameters

The bounded-degree vertex-layout coefficient #

The limiting adjacent correlation is 2 sqrt(d - 1) / d. Consequently Gaussian vertex layouts have at most arccos(2 sqrt(d - 1) / d) / pi times the number of edges, plus an arbitrarily small linear error. At degree four this per-edge coefficient is exactly 1/6.

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

The kernel correlation 2√(d - 1)/d of adjacent vertices in degree d.

Equations
Instances For
    source
    noncomputable def Complexity.Frontier.Gaussian.vertexCoefficient (d : ℕ) :
    ℝ

    The edge-crossing probability arccos(ρ_d)/π of Gaussian vertex scores.

    Equations
    Instances For
      source
      theorem Complexity.Frontier.Gaussian.vertexCorrelation_pos {d : ℕ} (hd : 2 ≤ d) :
      0 < vertexCorrelation d
      source
      theorem Complexity.Frontier.Gaussian.exists_decay_radius_degree {d : ℕ} (hd : 2 ≤ d) {ρ : ℝ} (hρ : ρ < vertexCorrelation d) :
      ∃ (q : ℝ) (R : ℕ), 0 ≤ q ∧ ρ ≤ 2 * q / (1 + q ^ 2) - ↑d * (↑(d - 1) * q ^ 2) ^ R

      The radial kernel reaches every correlation strictly below its limiting value.

      source
      theorem Complexity.Frontier.Gaussian.vertexLayout_bound {d : ℕ} (hd : 2 ≤ d) {ξ : ℝ} (hξ : 0 < ξ) :
      ∃ (N₀ : ℕ), ∀ (W : Type) [inst : Fintype W] (H : SimpleGraph W) [inst_1 : DecidableRel H.Adj], (∀ (v : W), H.degree v ≤ d) → N₀ < Fintype.card W → ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.crossingFinset {v : W | key v < t}).card ≤ vertexCoefficient d * ↑H.edgeFinset.card + ξ * ↑(Fintype.card W)

      Gaussian vertex layouts in every fixed degree. The error is measured per vertex; the leading coefficient is measured per edge.

      source
      theorem Complexity.Frontier.Gaussian.vertexCoefficient_four :
      vertexCoefficient 4 = 1 / 6

      Degree four gives an exact per-edge crossing coefficient of one sixth.