CubicPathwidth.Sw4.Defs

Source file CubicPathwidth/Sw4/Defs.lean of the Lean project (how it is built).

import CubicPathwidth.Sw4Spec
import CubicPathwidth.C3.Defs
import CubicPathwidth.T2.DefsB

/-!
# Plan interfaces for Theorem 8.2 (`thm:switched4`) and the seed `M` (not the approval surface)

Every `...Claim` below is a DEFINED proposition. Theorems using one take it as an
explicit hypothesis. No axiom is introduced.

Route (manuscript Appendix A.3 (`sec:switch-cert`)):
* `SwitchedLayout4Claim` (Q1, Lemma A.9 (`lem:median-layout4`)): the median-switched layout for `Δ ≤ 4`, with
  `D̂` (at least three neighbors across zero) in place of `D`.
* `PsiLowerClaim` (Q2, the part of Lemma A.11 (`lem:switch-cont`) used): a bound on `Ψ` over Gaussian
  vectors with incident correlations at least `r` gives the same bound up to `δ` for
  unit vectors with incident inner products at least `(1 - η) r`.
* `ZeroVertexClaim` (Q3, Lemma A.12 (`lem:switch4-zero`) per vertex): level-zero cost plus transfer `s`.
* `FrontierVertexClaim` (Q4, Lemma A.14 (`lem:switch4-means`) per vertex): frontier cost plus transfer at
  every nonzero threshold.
* `GoodLabelsSw` (Q5): one labeling with all loads at most `β + ε n`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace Sw4

open T2 T3

/-! ## Level-zero quantities of a labeling -/

section Layout

variable {n : ℕ} (G : SimpleGraph (Fin n))

/-- `D̂`: vertices with at least three neighbors on the other side of zero. -/
def hatD (y : Fin n → ℝ) : Finset (Fin n) := by
  classical
  exact Finset.univ.filter fun x =>
    (y x ≤ 0 ∧ 3 ≤ ((G.neighborFinset x).filter fun z => 0 < y z).card) ∨
      (0 < y x ∧ 3 ≤ ((G.neighborFinset x).filter fun z => y z ≤ 0).card)

/-- `L̂₀ = |U| + |D̂ ∩ W|`. -/
def hatL0 (y : Fin n → ℝ) : ℕ := by
  classical
  exact (C3.innerFrontier G y 0).card + ((hatD G y).filter fun x => 0 < y x).card

/-- `L̂₀' = |W| + |D̂ ∩ U|`. -/
def hatL0' (y : Fin n → ℝ) : ℕ := by
  classical
  exact (C3.outerFrontier G y 0).card + ((hatD G y).filter fun x => y x ≤ 0).card

end Layout

/-- (Q1, Lemma A.9 (`lem:median-layout4`)) The median-switched layout for maximum degree 4. -/
def SwitchedLayout4Claim : Prop :=
  ∀ (n : ℕ) (G : SimpleGraph (Fin n)), MaxDegreeAtMost 4 G →
    ∀ y : Fin n → ℝ, Function.Injective y → ∀ w : ℝ,
      (∀ t : ℝ, t < 0 → ((C3.innerFrontier G y t).card : ℝ) ≤ w) →
      (∀ t : ℝ, 0 < t → ((C3.outerFrontier G y t).card : ℝ) ≤ w) →
      (max (hatL0 G y) (hatL0' G y) : ℝ) + 1 ≤ w →
      HasPathwidthAtMost G w

/-! ## Vertex probabilities in the inner-product model -/

/-- The standard Gaussian measure on `Sample m`. -/
abbrev μ (m : ℕ) : Measure (GaussianField.Sample m) := stdGaussian (GaussianField.Sample m)

/-- `Pr(v ∈ U) + Pr(v ∈ D̂ ∩ W)` for a center `a` and neighbors `b`. -/
def zeroProb {m d : ℕ} (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m) :
    ℝ := by
  classical
  exact (μ m).real {x | ⟪a, x⟫ ≤ 0 ∧ ∃ i, 0 < ⟪b i, x⟫} +
    (μ m).real {x | 0 < ⟪a, x⟫ ∧ 3 ≤ (Finset.univ.filter fun i => ⟪b i, x⟫ ≤ 0).card}

/-- `Pr(v ∈ W) + Pr(v ∈ D̂ ∩ U)`. -/
def zeroProb' {m d : ℕ} (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m) :
    ℝ := by
  classical
  exact (μ m).real {x | 0 < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ 0} +
    (μ m).real {x | ⟪a, x⟫ ≤ 0 ∧ 3 ≤ (Finset.univ.filter fun i => 0 < ⟪b i, x⟫).card}

/-- The frontier probability at a nonzero threshold: outer frontier for `τ > 0`, inner
frontier for `τ < 0` (the sweep of Lemma A.9 (`lem:median-layout4`) uses these). -/
def frontierProb {m d : ℕ} (τ : ℝ) (a : GaussianField.Sample m)
    (b : Fin d → GaussianField.Sample m) : ℝ :=
  if 0 < τ then (μ m).real {x | τ < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ τ}
  else (μ m).real {x | ⟪a, x⟫ ≤ τ ∧ ∃ i, τ < ⟪b i, x⟫}

/-- (Q2) A bound `V` on `Ψ` over all Gaussian vectors with incident correlations at
least `r` gives `zeroProb, zeroProb' ≤ V + δ` for unit vectors whose incident inner
products are at least `(1 - η) r`. -/
def PsiLowerClaim : Prop :=
  ∀ (d : ℕ), d ≤ 4 → ∀ r : Fin d → ℝ, (∀ i, 0 < r i ∧ r i < 1) →
    ∀ V : ℝ, (∀ S : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ, SwitchAdmissible r S → psi S ≤ V) →
      ∀ δ : ℝ, 0 < δ → ∃ η : ℝ, 0 < η ∧
        ∀ (m : ℕ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
          ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) → (∀ i, (1 - η) * r i ≤ ⟪a, b i⟫) →
            zeroProb a b ≤ V + δ ∧ zeroProb' a b ≤ V + δ

/-- (Q3, Lemma A.12 (`lem:switch4-zero`) per vertex) Level-zero cost plus the transfer `s` is at most
`a_d + δ` for every `{3,4}`-type `(d; k₃, k₄)`. -/
def ZeroVertexClaim : Prop :=
  ∀ δ : ℝ, 0 < δ → ∃ η : ℝ, 0 < η ∧
    ∀ (m d k₃ k₄ : ℕ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
      (d = 3 ∨ d = 4) → k₃ + k₄ = d → ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) →
      (∀ i, (1 - η) * typeFloors d k₃ k₄ i ≤ ⟪a, b i⟫) →
        zeroProb a b + transferTerm d k₃ k₄ 0 sM 0 0 ≤ coeff C3.c3 aM 0 d + δ ∧
        zeroProb' a b + transferTerm d k₃ k₄ 0 sM 0 0 ≤ coeff C3.c3 aM 0 d + δ

/-- (Q4, Lemma A.14 (`lem:switch4-means`) per vertex) For every nonzero threshold there is a transfer with
frontier cost plus transfer at most `a_d + δ` for every `{3,4}`-type. The precision `η`
is uniform in `τ`. -/
def FrontierVertexClaim : Prop :=
  ∀ δ : ℝ, 0 < δ → ∃ η : ℝ, 0 < η ∧ ∀ τ : ℝ, τ ≠ 0 → ∃ t₃₄ : ℝ,
    ∀ (m d k₃ k₄ : ℕ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
      (d = 3 ∨ d = 4) → k₃ + k₄ = d → ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) →
      (∀ i, (1 - η) * typeFloors d k₃ k₄ i ≤ ⟪a, b i⟫) →
        frontierProb τ a b + transferTerm d k₃ k₄ 0 t₃₄ 0 0 ≤ coeff C3.c3 aM 0 d + δ

/-- (Q5) Good labels for the switched layout, minimum degree 3, maximum degree 4. -/
def GoodLabelsSw (a₃ a₄ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), MinDegreeAtLeast 3 G → MaxDegreeAtMost 4 G →
      ∃ y : Fin n → ℝ, Function.Injective y ∧
        (∀ t : ℝ, t < 0 → ((C3.innerFrontier G y t).card : ℝ) ≤
          a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n) ∧
        (∀ t : ℝ, 0 < t → ((C3.outerFrontier G y t).card : ℝ) ≤
          a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n) ∧
        ((hatL0 G y : ℕ) : ℝ) ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n ∧
        ((hatL0' G y : ℕ) : ℝ) ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n

end Sw4
end CubicPathwidth