Documentation

Complexity.Computability.Circuit.Frontier.Layouts.Gaussian.Coefficient

The Gaussian coefficient and its numerical bound #

The cubic layout coefficient of Gaussian edge scores is p = (3 / (2π)) arccos ((1 + 2√2)/4) ≈ 0.14035, the straddling bound at the limiting adjacent correlation 2√2/3 (Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient_eq). It is positive, and the circuit coefficient 1 + 1 / (2p) = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625 is at least 114/25 = 4.56 (Cslib.Circuits.Frontier.Gaussian.circuitCoefficient_ge_456), by rational bounds on √2, cos and π.

Main definitions #

Main results #

source
noncomputable def Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient :
ℝ

The cubic layout coefficient of Gaussian edge scores, (3 / (2π)) arccos ((1 + 2√2)/4).

Instances For
    source
    theorem Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient_eq :
    gaussianCoefficient = straddleBound (2 * √2 / 3)

    The Gaussian coefficient is the straddling bound at the limiting correlation 2√2/3.

    source
    theorem Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient_ge :
    1 / 20 ≤ gaussianCoefficient

    A crude lower bound, p ≥ 1/20, from cos (π/30) ≥ (1 + 2√2)/4.

    source
    theorem Cslib.Circuits.Frontier.Gaussian.gaussianCoefficient_pos :
    0 < gaussianCoefficient
    source
    theorem Cslib.Circuits.Frontier.Gaussian.one_add_inv_two_mul_gaussianCoefficient :
    1 + 1 / (2 * gaussianCoefficient) = 1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))

    The circuit coefficient 1 + 1 / (2p) of the cubic coefficient p.

    source
    theorem Cslib.Circuits.Frontier.Gaussian.circuitCoefficient_ge_456249 :
    456249 / 100000 ≤ 1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))

    The sharpened numerical bound. The circuit coefficient 1 + π / (3 arccos ((1 + 2√2)/4)) is at least 456249/100000 = 4.56249.

    With θ = arccos ((1 + 2√2)/4) = 0.29395038…, the bound θ ≤ 0.2939509 holds by bounding the cosine at 0.2939509 / 32 via cos_bound and doubling five times: cos (0.2939509) ≤ 0.9571067065 < 0.95710678 ≤ (1 + 2√2)/4. Then π / (3 · 0.2939509) > 3.1415926 / 0.8818527 > 3.56249.

    source
    theorem Cslib.Circuits.Frontier.Gaussian.circuitCoefficient_ge_456 :
    114 / 25 ≤ 1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4))

    The numerical bound. The circuit coefficient 1 + π / (3 arccos ((1 + 2√2)/4)) is at least 114/25 = 4.56.