CubicPathwidth.T3Spec

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

import CubicPathwidth.T2Spec

/-!
# APPROVED specification: Theorem 7.2 (`thm:deg5`) (maximum degree 5)

STATUS: approved by the author on 2026-10-09. Every `def ... : Prop` below is a proposition that
we DEFINE. Nothing here is proved, and nothing is assumed as an axiom. This file
only checks that the definitions elaborate against the pinned project library
(Lean 4.34.0, mathlib 5ed2965256430c3649e86755f9576b54eca72435).
The proofs are `target3P`, `target3R`, `target3S` in `T3/Targets.lean`.


It imports the approved Theorem 7.1 (`thm:deg4`) specification `T2Spec.lean` unchanged and reuses
its vocabulary: `MaxDegreeAtMost`, `degreeCount`, `Phi`, `phi`, `gaussProb`,
`IsCorrelation`, `pMin`, `starBound`, `Fcubic`, and `HasPathwidthAtMost` from the
frozen `CubicPathwidth.lean`.

Statement (Theorem 7.2, `thm:deg5`): if `Δ(G) ≤ 5` then
`pw(G) ≤ a₃ n₃ + a₄ n₄ + a₅ n₅ + o(n)` for each of
`P = (F, 0.2575, 0.3667)`, `R = (0.1455, 0.2530, 0.3600)`, `S = (5/32, 1/4, 11/32)`.

This file is the APPROVAL SURFACE.
-/

noncomputable section

namespace CubicPathwidth
namespace T3

open T2

/-! ## 1. The uniform bound for maximum degree 5 -/

/-- `pw(G) ≤ a₃ n₃ + a₄ n₄ + a₅ n₅ + o(n)` over graphs of maximum degree at most 5,
uniformly: for every `ε > 0`, ONE threshold `N` works for every `n ≥ N` and every
such graph on `Fin n`. Vertices of degree 0, 1 or 2 carry coefficient zero. -/
def UniformDegreeCountBound5 (a₃ a₄ a₅ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ G : SimpleGraph (Fin n), MaxDegreeAtMost 5 G →
        HasPathwidthAtMost G
          (a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) +
            a₅ * (degreeCount G 5 : ℝ) + ε * (n : ℝ))

/-! ## 2. Edge-correlation floors and vertex types -/

/-- `r_{ij} = sech(¼ ln((i-1)(j-1)))`, the floor for an edge joining degrees `i`, `j`.
For `(3,3)`, `(3,4)`, `(4,4)` it equals `T2.r33`, `T2.r34`, `T2.r44`. -/
def rFloor (i j : ℕ) : ℝ := 1 / Real.cosh (Real.log (((i : ℝ) - 1) * ((j : ℝ) - 1)) / 4)

/-- Floors of a vertex of degree `d` with `k₃` neighbors of degree 3, `k₄` of
degree 4 and the remaining `d - k₃ - k₄` of degree 5, listed in that order. -/
def typeFloors (d k₃ k₄ : ℕ) : Fin d → ℝ := fun i =>
  if (i : ℕ) < k₃ then rFloor d 3
  else if (i : ℕ) < k₃ + k₄ then rFloor d 4
  else rFloor d 5

/-- Transfer term `λ_T(t)` of the type `(d; k₃, k₄, k₅)`: a vertex of degree `i`
sends `t_{ij}` along each edge to a neighbor of degree `j > i`. -/
def transferTerm (d k₃ k₄ k₅ : ℕ) (t₃₄ t₃₅ t₄₅ : ℝ) : ℝ :=
  if d = 3 then -(k₄ : ℝ) * t₃₄ - (k₅ : ℝ) * t₃₅
  else if d = 4 then (k₃ : ℝ) * t₃₄ - (k₅ : ℝ) * t₄₅
  else (k₃ : ℝ) * t₃₅ + (k₄ : ℝ) * t₄₅

/-- The coefficient of degree `d ∈ {3,4,5}`. -/
def coeff (a₃ a₄ a₅ : ℝ) (d : ℕ) : ℝ := if d = 3 then a₃ else if d = 4 then a₄ else a₅

/-! ## 3. External input, stated as an explicit hypothesis -/

/-- HYPOTHESIS H3 (`prop:certificate` for `D = {3,4,5}`): the
triple is admissible. For every `τ ∈ [-3, 3]` there are transfers
`t₃₄, t₃₅, t₄₅` such that every type `(d; k₃, k₄, k₅)` with `d ∈ {3,4,5}` and
`k₃ + k₄ + k₅ = d` satisfies `C_T(τ) + λ_T(t) ≤ a_d`, where `C_T` is the exact
center bound `starBound`. Established outside Lean by the Arb certificate.
Naming it does NOT prove it. -/
def AdmissibleTriple (a₃ a₄ a₅ : ℝ) : Prop :=
  ∀ τ : ℝ, τ ∈ Set.Icc (-3 : ℝ) 3 → ∃ t₃₄ t₃₅ t₄₅ : ℝ,
    ∀ d k₃ k₄ k₅ : ℕ, (d = 3 ∨ d = 4 ∨ d = 5) → k₃ + k₄ + k₅ = d →
      starBound (typeFloors d k₃ k₄) τ + transferTerm d k₃ k₄ k₅ t₃₄ t₃₅ t₄₅ ≤
        coeff a₃ a₄ a₅ d

/-! ## 4. The headline claims (approval surface) -/

def Theorem3P : Prop := UniformDegreeCountBound5 Fcubic (103 / 400) (3667 / 10000)

def Theorem3R : Prop := UniformDegreeCountBound5 (291 / 2000) (253 / 1000) (9 / 25)

def Theorem3S : Prop := UniformDegreeCountBound5 (5 / 32) (1 / 4) (11 / 32)

/-- PROOF TARGETS. -/
def Target3P : Prop := AdmissibleTriple Fcubic (103 / 400) (3667 / 10000) → Theorem3P

def Target3R : Prop := AdmissibleTriple (291 / 2000) (253 / 1000) (9 / 25) → Theorem3R

def Target3S : Prop := AdmissibleTriple (5 / 32) (1 / 4) (11 / 32) → Theorem3S

end T3
end CubicPathwidth

/-! ## 5. Elaboration checks (not proofs of the claims) -/
#check CubicPathwidth.T3.Target3P
#check CubicPathwidth.T3.Target3R
#check CubicPathwidth.T3.Target3S
#print CubicPathwidth.T3.AdmissibleTriple
#print CubicPathwidth.T3.UniformDegreeCountBound5
Back to top