Choosing the layout parameters

For fixed parameters, a good sample exists once the graph is large enough. As the decay rate q increases to 1/√2, the kernel correlation 2q/(1+q²) increases to 2√2/3, where √(1-ρ)/√(1+ρ) = 3 - 2√2; the truncation error 3 (2q²)^R vanishes as R grows. A fine threshold grid with small deviations then brings the prefix-cut coefficient within any positive slack of (3/π)(3 - 2√2).

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_key_of_parameters {q : ℝ} (hq0 : 0 ≤ q) (R : ℕ) {ρ₀ : ℝ} (hρ₀ : -1 < ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) {T ε : ℝ} (hT : 0 < T) (hε : 0 < ε) {M : ℕ} (hM : 0 < M) : ∃ (N₀ : ℕ), ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj], H.IsRegularOfDegree 3 → N₀ < Fintype.card W → ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.cutFinset {w : W | key w < t}).card ≤ layoutBound ρ₀ T ε M * ↑(Fintype.card W)

Fixed parameters. Every large cubic graph has an injective key whose prefix cuts are at most layoutBound ρ₀ T ε M times the number of vertices.

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.crossRatio (ρ : ℝ) : ℝ

The crossing ratio √(1-ρ)/√(1+ρ).

Equations

• Algebraic.Cutwidth.Gaussian.Internal.crossRatio ρ = √(1 - ρ) / √(1 + ρ)

theorem Algebraic.Cutwidth.Gaussian.Internal.crossBound_eq (ρ : ℝ) : crossBound ρ = 2 / Real.pi * crossRatio ρ

theorem Algebraic.Cutwidth.Gaussian.Internal.crossRatio_limit : crossRatio (2 * √2 / 3) = 3 - 2 * √2

theorem Algebraic.Cutwidth.Gaussian.Internal.continuousAt_crossRatio {ρ : ℝ} (hρ : -1 < ρ) : ContinuousAt crossRatio ρ

theorem Algebraic.Cutwidth.Gaussian.Internal.continuous_correlation : Continuous fun (q : ℝ) => 2 * q / (1 + q ^ 2)

theorem Algebraic.Cutwidth.Gaussian.Internal.correlation_limit : 2 * (√2 / 2) / (1 + (√2 / 2) ^ 2) = 2 * √2 / 3

theorem Algebraic.Cutwidth.Gaussian.Internal.cutwidthCoefficient_ge : 3 / 40 ≤ cutwidthCoefficient

theorem Algebraic.Cutwidth.Gaussian.Internal.cutwidthCoefficient_pos : 0 < cutwidthCoefficient

theorem Algebraic.Cutwidth.Gaussian.Internal.one_add_inv_two_mul_cutwidthCoefficient : 1 + 1 / (2 * cutwidthCoefficient) = 1 + Real.pi * (3 + 2 * √2) / 6

The circuit coefficient of the Gaussian ordering coefficient 2c.

theorem Algebraic.Cutwidth.Gaussian.Internal.two_mul_cutwidthCoefficient_le : 2 * cutwidthCoefficient ≤ 20 / 61

The Gaussian ordering coefficient is at most 20/61.

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

Decay rate and radius. Every correlation target below 2√2/3 is met by the truncated kernel for some decay rate q < 1/√2 and some radius.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_parameters {ξ : ℝ} (hξ : 0 < ξ) : ∃ (q : ℝ) (R : ℕ) (ρ₀ : ℝ) (T : ℝ) (ε : ℝ) (M : ℕ), 0 ≤ q ∧ -1 < ρ₀ ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R ∧ 0 < T ∧ 0 < ε ∧ 0 < M ∧ layoutBound ρ₀ T ε M ≤ cutwidthCoefficient + ξ

Parameters. For every positive slack some admissible parameters bring the layout bound within that slack of (3/π)(3 - 2√2).

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_key_bound {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj], H.IsRegularOfDegree 3 → N₀ < Fintype.card W → ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.cutFinset {w : W | key w < t}).card ≤ (cutwidthCoefficient + ξ) * ↑(Fintype.card W)

The Gaussian cubic cutwidth bound. For every positive slack, every large cubic graph has an injective key whose prefix cuts are at most ((3/π)(3 - 2√2) + ξ) h.