CubicPathwidth.T3.Defs

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

import CubicPathwidth.T3Spec
import CubicPathwidth.T2.DefsB

/-!
# Plan interfaces for Theorem 3 (not the approval surface)

Every `...Claim` below is a DEFINED proposition. Theorems using one take it as an
explicit hypothesis. No axiom is introduced. The analogues for maximum degree 4
are in `T2/DefsB.lean`; `T2.HetStarClaim`, `T2.StarBoundContClaim` and
`T2.PlainLayoutClaim` are reused unchanged (they do not mention degrees).

* `DegreeLabels5Claim` (C1): degree-sensitive labels for `3 ≤ δ`, `Δ ≤ 5`.
* `Charging5Claim` (C3): charging with three degrees and three transfers.
* `GoodLabelsCount5` (C5): good labels in degree-count form.
* `Reduction5Claim` (C6): vertices of degree at most 2 cost `o(n)`.
-/

noncomputable section
open scoped RealInnerProductSpace

namespace CubicPathwidth
namespace T3

open T2

/-- (C1) A label scheme for `3 ≤ δ`, `Δ ≤ 5` at precision `η`, locality radius `K`. -/
def LabelScheme5 (η : ℝ) (K : ℕ) : Prop := by
  classical
  exact ∀ (n : ℕ) (G : SimpleGraph (Fin n)), MinDegreeAtLeast 3 G → MaxDegreeAtMost 5 G →
    ∃ vec : Fin n → GaussianField.Sample n,
      (∀ v, ‖vec v‖ = 1) ∧
      (∀ u v, G.Adj u v → (1 - η) * rFloor (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 DegreeLabels5Claim : Prop := ∀ η : ℝ, 0 < η → ∃ K : ℕ, LabelScheme5 η K

/-- (C3) Charging along edges joining different degrees in `{3,4,5}`. -/
def Charging5Claim : Prop := by
  classical
  exact ∀ (n : ℕ) (G : SimpleGraph (Fin n)), MinDegreeAtLeast 3 G → MaxDegreeAtMost 5 G →
    ∀ (C : Fin n → ℝ) (a₃ a₄ a₅ t₃₄ t₃₅ t₄₅ : ℝ),
      (∀ v, C v + transferTerm (G.degree v) (nbrCount G v 3) (nbrCount G v 4)
          (nbrCount G v 5) t₃₄ t₃₅ t₄₅ ≤ coeff a₃ a₄ a₅ (G.degree v)) →
      ∑ v, C v ≤ a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
        a₅ * (degreeCount G 5 : ℝ)

/-- (C5) Good labels for `3 ≤ δ`, `Δ ≤ 5`, degree-count form. -/
def GoodLabelsCount5 (a₃ a₄ a₅ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
    ∀ G : SimpleGraph (Fin n), MinDegreeAtLeast 3 G → MaxDegreeAtMost 5 G →
      ∃ y : Fin n → ℝ, Function.Injective y ∧
        ∀ t : ℝ, ((C3.outerFrontier G y t).card : ℝ) ≤
          a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
            a₅ * (degreeCount G 5 : ℝ) + ε * n

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

/-- (C6) Reductions for maximum degree 5. -/
def Reduction5Claim : Prop :=
  ∀ a₃ a₄ a₅ : ℝ, 0 ≤ a₃ → a₃ ≤ a₄ → a₄ ≤ a₅ →
    MinDegThreeBound5 a₃ a₄ a₅ → UniformDegreeCountBound5 a₃ a₄ a₅

/-- (C5) as a statement about its children, proved in `T3/GoodLabelsCount5.lean`. -/
def GoodLabelsCount5Step : Prop :=
  DegreeLabels5Claim → HetStarClaim → StarBoundContClaim → Charging5Claim →
    ∀ a₃ a₄ a₅ : ℝ, AdmissibleTriple a₃ a₄ a₅ → 5 * Phi (-3) ≤ a₃ → a₃ ≤ a₄ → a₄ ≤ a₅ →
      GoodLabelsCount5 a₃ a₄ a₅

end T3
end CubicPathwidth
Back to top