CubicPathwidth.T2.DefsB

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

import CubicPathwidth.T2.Defs

/-!
# Plan interfaces for Theorem 2(b) and 2(c) (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 (main results, Steps 2–6, and the reduction lemma):
* `DegreeLabelsClaim` (B1): degree-sensitive unit label vectors with edge
  correlations at least `(1-η)` times the floor of the edge's degree pair,
  local at a bounded graph radius, pairwise distinct.
* `HetStarClaim` (O4 with unequal floors): frontier probability of a star is at
  most `starBound r τ`.
* `StarBoundContClaim` (B2): `starBound` is continuous from below in the floors,
  uniformly for `τ ∈ [-3, 3]`.
* `ChargingClaim` (B3): admissible transfers give `∑ C_v ≤ a₃ n₃ + a₄ n₄`.
* `GoodLabelsCount a₃ a₄`: for `3 ≤ δ`, `Δ ≤ 4`, injective labels with every
  frontier at most `a₃ n₃ + a₄ n₄ + ε n`.
* `ReductionClaim` (B5): bounds for minimum degree 3 transfer to all graphs of
  maximum degree 4.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2

/-- Every vertex has at least `k` neighbors. -/
def MinDegreeAtLeast {n : ℕ} (k : ℕ) (G : SimpleGraph (Fin n)) : Prop := by
  classical
  exact ∀ v : Fin n, k ≤ G.degree v

/-- Number of neighbors of `v` of degree exactly `d`. -/
def nbrCount {n : ℕ} (G : SimpleGraph (Fin n)) (v : Fin n) (d : ℕ) : ℕ := by
  classical
  exact ((G.neighborFinset v).filter fun u => G.degree u = d).card

/-- Edge-correlation floor for an edge joining degrees `i` and `j`
(`r₃₃`, `r₃₄`, `r₄₄`; other degrees are irrelevant and get `r₄₄`). -/
def edgeFloor (i j : ℕ) : ℝ :=
  if i = 3 ∧ j = 3 then r33 else if i = 4 ∧ j = 4 then r44
  else if (i = 3 ∧ j = 4) ∨ (i = 4 ∧ j = 3) then r34 else r44

/-- (B1) A label scheme at precision `η` and locality radius `K`. -/
def LabelScheme (η : ℝ) (K : ℕ) : Prop := by
  classical
  exact ∀ (n : ℕ) (G : SimpleGraph (Fin n)), MinDegreeAtLeast 3 G → MaxDegreeAtMost 4 G →
    ∃ vec : Fin n → GaussianField.Sample n,
      (∀ v, ‖vec v‖ = 1) ∧
      (∀ u v, G.Adj u v → (1 - η) * edgeFloor (G.degree u) (G.degree v) ≤ ⟪vec u, vec v⟫) ∧
      (∀ v w, w ∉ Locality.ball G v K → vec v w = 0) ∧
      (∀ u v, u ≠ v → vec u ≠ vec v)

def DegreeLabelsClaim : Prop := ∀ η : ℝ, 0 < η → ∃ K : ℕ, LabelScheme η K

/-- (O4 general) Star bound with one floor per neighbor. -/
def HetStarClaim : Prop :=
  ∀ (m d : ℕ) (r : Fin d → ℝ), (∀ i, 0 < r i ∧ r i < 1) →
    ∀ (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m),
      ‖a‖ = 1 → (∀ i, ‖b i‖ = 1) → (∀ i, r i ≤ ⟪a, b i⟫) →
      ∀ τ : ℝ,
        (stdGaussian (GaussianField.Sample m)).real
            {x | τ < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ τ} ≤ starBound r τ

/-- (B2) Continuity of the star bound from below in the floors. -/
def StarBoundContClaim : Prop :=
  ∀ (d : ℕ) (r : Fin d → ℝ), (∀ i, 0 < r i ∧ r i < 1) →
    ∀ δ : ℝ, 0 < δ → ∃ η : ℝ, 0 < η ∧
      ∀ r' : Fin d → ℝ, (∀ i, (1 - η) * r i ≤ r' i ∧ r' i ≤ r i) →
        ∀ τ ∈ Set.Icc (-3 : ℝ) 3, starBound r' τ ≤ starBound r τ + δ

/-- (B3) Charging along edges joining degrees 3 and 4. -/
def ChargingClaim : Prop := by
  classical
  exact ∀ (n : ℕ) (G : SimpleGraph (Fin n)), MinDegreeAtLeast 3 G → MaxDegreeAtMost 4 G →
    ∀ (C : Fin n → ℝ) (a₃ a₄ t : ℝ),
      (∀ v, G.degree v = 3 → C v - (nbrCount G v 4 : ℝ) * t ≤ a₃) →
      (∀ v, G.degree v = 4 → C v + (nbrCount G v 3 : ℝ) * t ≤ a₄) →
      ∑ v, C v ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ)

/-- Good labels for minimum degree 3 and maximum degree 4, degree-count form. -/
def GoodLabelsCount (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 : ℝ, ((C3.outerFrontier G y t).card : ℝ) ≤
          a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n

/-- The degree-count bound restricted to minimum degree at least 3. -/
def MinDegThreeBound (a₃ a₄ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), MinDegreeAtLeast 3 G → MaxDegreeAtMost 4 G →
      HasPathwidthAtMost G (a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * n)

/-- (B5) Reductions: vertices of degree at most 2 cost `o(n)`. -/
def ReductionClaim : Prop :=
  ∀ a₃ a₄ : ℝ, 0 ≤ a₃ → a₃ ≤ a₄ → MinDegThreeBound a₃ a₄ → UniformDegreeCountBound a₃ a₄

end T2
end CubicPathwidth
Back to top