Choosing the band-jump parameters

The edge-score parameters of Gaussian.Frontier bring the per-vertex straddling bound within any slack of the frontier coefficient. The band-jump decomposition multiplies it by exp (-c²/2); a long fine grid, small deviations, and a small Markov threshold bring every bag within any slack of exp (-c²/2) times the frontier coefficient, once the subcriticality hypothesis supplies a cluster size K and the graph is large enough that K is negligible.

At c = 4/25 the doubled coefficient is at most 5/18, because 2 p ≤ 9/32 and exp (-8/625) ≤ 80/81.

theorem Algebraic.Cutwidth.Gaussian.Internal.two_mul_sq_lt_one_of_le {q : ℝ} {R : ℕ} {ρ₀ : ℝ} (hρ₀ : 17 / 32 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) : 2 * q ^ 2 < 1

A correlation target of at least 17/32 forces a decay rate below 1/√2.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_band_of_parameters {q : ℝ} (hq0 : 0 ≤ q) (R : ℕ) {ρ₀ : ℝ} (hρ₀ : 17 / 32 ≤ ρ₀) (hρ : ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R) {c T ε η : ℝ} (hc : 0 < c) (hcT : c < T) (hε : 0 < ε) (hη : 0 < η) {M : ℕ} (hM : 0 < M) (hband : BandSubcritical q R c) : ∃ (N₀ : ℕ), ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj], H.IsRegularOfDegree 3 → N₀ < Fintype.card W → ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ (bandLayoutBound ρ₀ c T ε η M + ε) * ↑(Fintype.card W)

Fixed parameters. Under the subcriticality hypothesis, every large cubic graph has a band-jump decomposition with bags of at most (bandLayoutBound ρ₀ c T ε η M + ε) h vertices.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_band_parameters {c : ℝ} (hc : 0 < c) {ξ : ℝ} (hξ : 0 < ξ) : ∃ (q : ℝ) (R : ℕ) (ρ₀ : ℝ) (T : ℝ) (ε : ℝ) (η : ℝ) (M : ℕ), 0 ≤ q ∧ 17 / 32 ≤ ρ₀ ∧ ρ₀ ≤ 2 * q / (1 + q ^ 2) - 3 * (2 * q ^ 2) ^ R ∧ c < T ∧ 0 < ε ∧ 0 < η ∧ 0 < M ∧ bandLayoutBound ρ₀ c T ε η M + ε ≤ Real.exp (-c ^ 2 / 2) * frontierCoefficient + ξ

Parameters. For every positive slack some admissible parameters bring the band-jump bound within that slack of exp (-c²/2) times the frontier coefficient.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_pathwidthBound_band {c : ℝ} (hc : 0 < c) (hband : ∀ (q : ℝ) (R : ℕ), 0 ≤ q → 2 * q ^ 2 < 1 → BandSubcritical q R c) {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), PathwidthBound (Real.exp (-c ^ 2 / 2) * frontierCoefficient) ξ N₀

The band-jump cubic pathwidth bound, conditional on subcritical band clusters.

theorem Algebraic.Cutwidth.Gaussian.Internal.exp_neg_four_div_twentyFive_sq_le : Real.exp (-(4 / 25) ^ 2 / 2) ≤ 80 / 81

exp (-(4/25)²/2) = exp (-8/625) ≤ 80/81.

theorem Algebraic.Cutwidth.Gaussian.Internal.two_mul_exp_mul_frontierCoefficient_le : 2 * (Real.exp (-(4 / 25) ^ 2 / 2) * frontierCoefficient) ≤ 5 / 18

At c = 4/25 the doubled band-jump coefficient is at most 5/18.