CubicPathwidth.T2Spec

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

import CubicPathwidth
import Mathlib.Probability.Distributions.Gaussian.Multivariate
import Mathlib.Probability.Distributions.Gaussian.Real

/-!
# APPROVED specification: Theorem 7.1 (`thm:deg4`) (maximum degree 4)

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 `target2a`, `target2b`, `target2c` in `T2/TargetA.lean`, `T2/TargetBC.lean`.


The original specification `CubicPathwidth.lean` is imported unchanged, so
`PathDecomposition` and `HasPathwidthAtMost` keep their existing, reviewed
meaning: a graph on `Fin n` has pathwidth at most the REAL number `w` when some
path decomposition has every bag of size at most `w + 1`.

This file is the APPROVAL SURFACE. Proof-plan interfaces will live in separate
files; they may change during proof work without renewed approval, provided
this file, its imports and the trust boundary are unchanged.

Statement (Theorem 7.1, `thm:deg4`):
if `Δ(G) ≤ 4` then
  (a) `pw(G) ≤ F₄ n + o(n)`;
  (b) `pw(G) ≤ F n₃ + 0.2575 n₄ + o(n)`;
  (c) `pw(G) ≤ (5/32) n₃ + (1/4) n₄ + o(n)`.
-/

noncomputable section
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2

/-! ## 1. The graph class and degree counts -/

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

/-- `degreeCount G d` is `n_d`, the number of vertices of degree exactly `d`. -/
def degreeCount {n : ℕ} (G : SimpleGraph (Fin n)) (d : ℕ) : ℕ := by
  classical
  exact (Finset.univ.filter fun v : Fin n => G.degree v = d).card

/-! ## 2. Uniform asymptotic bounds (all quantifiers visible) -/

/-- `pw(G) ≤ a n + o(n)` over graphs of maximum degree at most 4.
For every `ε > 0`, ONE threshold `N` works for every `n ≥ N` and every such
graph on `Fin n`. -/
def UniformDegreeFourBound (a : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ G : SimpleGraph (Fin n), MaxDegreeAtMost 4 G →
        HasPathwidthAtMost G ((a + ε) * (n : ℝ))

/-- `pw(G) ≤ a₃ n₃ + a₄ n₄ + o(n)` over graphs of maximum degree at most 4.
Vertices of degree 0, 1 or 2 carry coefficient zero. -/
def UniformDegreeCountBound (a₃ a₄ : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ G : SimpleGraph (Fin n), MaxDegreeAtMost 4 G →
        HasPathwidthAtMost G
          (a₃ * (degreeCount G 3 : ℝ) + a₄ * (degreeCount G 4 : ℝ) + ε * (n : ℝ))

/-! ## 3. Gaussian vocabulary -/

/-- Standard normal distribution function `Φ(x) = Pr(Z ≤ x)`. -/
def Phi (x : ℝ) : ℝ := (gaussianReal 0 1).real (Set.Iic x)

/-- Standard normal density `φ`. -/
def phi (x : ℝ) : ℝ := gaussianPDFReal 0 1 x

/-- `gaussProb S A` is the probability that a centered Gaussian vector with
covariance matrix `S` lies in `A`. Mathlib's `multivariateGaussian 0 S` is
`N(0, S)` when `S` is positive semidefinite (singular `S` allowed); for any
other `S` it is the point mass at `0`, so every use below has a positive
semidefinite `S`. -/
def gaussProb {m : ℕ} (S : Matrix (Fin m) (Fin m) ℝ)
    (A : Set (EuclideanSpace ℝ (Fin m))) : ℝ :=
  (multivariateGaussian 0 S A).toReal

/-- A correlation matrix: positive semidefinite with unit diagonal. -/
def IsCorrelation {m : ℕ} (C : Matrix (Fin m) (Fin m) ℝ) : Prop :=
  C.PosSemidef ∧ ∀ i, C i i = 1

/-! ## 4. Ideal stars and the constants `F₄` and `F` -/

/-- Covariance of the ideal `d`-star on coordinates `0, …, d`: coordinate `0`
is the center; every center-leaf correlation is `r`; every leaf-leaf
correlation is `r² - (1 - r²)/(d - 1)`, the regular-simplex value. -/
def idealStarCov (d : ℕ) (r : ℝ) : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ :=
  fun i j =>
    if i = j then 1
    else if i = 0 ∨ j = 0 then r
    else r ^ 2 - (1 - r ^ 2) / ((d : ℝ) - 1)

/-- The frontier event at level `τ`: the center is above `τ` and some leaf is at
or below `τ`. -/
def frontierEvent (d : ℕ) (τ : ℝ) : Set (EuclideanSpace ℝ (Fin (d + 1))) :=
  {x | τ < x 0 ∧ ∃ i : Fin (d + 1), i ≠ 0 ∧ x i ≤ τ}

/-- The ideal `d`-star function `f_{d,r}(τ)`. -/
def idealStarFn (d : ℕ) (r τ : ℝ) : ℝ :=
  gaussProb (idealStarCov d r) (frontierEvent d τ)

/-- Edge-correlation floors of the labels: degrees (3,3), (3,4), (4,4).
`r₃₄ = sech(¼ ln 6)`. -/
def r33 : ℝ := 2 * Real.sqrt 2 / 3

def r34 : ℝ := 1 / Real.cosh (Real.log 6 / 4)

def r44 : ℝ := Real.sqrt 3 / 2

/-- `F₄ = sup_τ f_{4, √3/2}(τ) ≈ 0.2457719747`. The supremum of a set of
probabilities, hence of a nonempty set bounded above by `1`. -/
def F4 : ℝ := sSup (Set.range fun τ : ℝ => idealStarFn 4 r44 τ)

/-- `F = sup_τ f_{3, 2√2/3}(τ) ≈ 0.1401582523`, the cubic plain-sweep constant. -/
def Fcubic : ℝ := sSup (Set.range fun τ : ℝ => idealStarFn 3 r33 τ)

/-! ## 5. External inputs, stated as explicit hypotheses -/

/-- The regular-simplex Gram matrix in `m` variables: unit diagonal and
off-diagonal entries `-1/(m-1)`. Written exactly as in Mulgund's
`WeakSimplex.regularSimplexGram`. -/
def regularSimplexGram (m : ℕ) : Matrix (Fin m) (Fin m) ℝ :=
  ((m : ℝ) / ((m : ℝ) - 1)) •
    ((1 : Matrix (Fin m) (Fin m) ℝ) - (1 / (m : ℝ)) • Matrix.of fun _ _ => (1 : ℝ))

/-- `{x | x i ≤ t for all i}`. -/
def lowerOrthant {m : ℕ} (t : ℝ) : Set (EuclideanSpace ℝ (Fin m)) :=
  {x | ∀ i, x i ≤ t}

/-- HYPOTHESIS H1 (the case `d = 4` of Lemma 6.5 (`lem:simplex`); Mulgund's
`FSC.cdf_simplex_le` at `n = 4`). Among all 4×4 correlation matrices, the
regular simplex minimizes `Pr(max_i U_i ≤ t)`, for every real `t`.
Checked in Lean in a separate environment (Lean 4.31.0, its own mathlib);
it cannot be imported here. Naming it does NOT prove it. -/
def SimplexFourClaim : Prop :=
  ∀ C : Matrix (Fin 4) (Fin 4) ℝ, IsCorrelation C → ∀ t : ℝ,
    gaussProb (regularSimplexGram 4) (lowerOrthant t) ≤ gaussProb C (lowerOrthant t)

/-- `P_min(a)`: the infimum, over all `m×m` correlation matrices `C`, of
`Pr(U_i > a_i for all i)` with `U ~ N(0, C)`. -/
def pMin {m : ℕ} (a : Fin m → ℝ) : ℝ :=
  ⨅ C : {C : Matrix (Fin m) (Fin m) ℝ // IsCorrelation C},
    gaussProb C.1 {x | ∀ i, a i < x i}

/-- The center bound Equation (6.2) (`eq:center-bound`, `C_d(τ; r)` of Section 6 (`sec:stars`)) for incident correlation floors
`r i`: `Φ(-τ) - ∫_τ^∞ φ(z) P_min(a(z)) dz` with `a_i(z) = (τ - r_i z)/√(1-r_i²)`. -/
def starBound {m : ℕ} (r : Fin m → ℝ) (τ : ℝ) : ℝ :=
  Phi (-τ) -
    ∫ z in Set.Ioi τ, phi z * pMin (fun i => (τ - r i * z) / Real.sqrt (1 - r i ^ 2))

/-- Vertex types for minimum degree 3 and maximum degree 4. A degree-3 vertex
with `k` degree-4 neighbors has floors `r₃₄` (k times) and `r₃₃`; a degree-4
vertex with `j` degree-3 neighbors has floors `r₃₄` (j times) and `r₄₄`. -/
def floorsThree (k : ℕ) : Fin 3 → ℝ := fun i => if (i : ℕ) < k then r34 else r33

def floorsFour (j : ℕ) : Fin 4 → ℝ := fun i => if (i : ℕ) < j then r34 else r44

/-- HYPOTHESIS H2 (`prop:certificate`, restricted to maximum degree 4): the pair
`(a₃, a₄)` is admissible. For every threshold `τ ∈ [-3, 3]` there is a transfer
`t` (per edge joining degrees 3 and 4) such that every type satisfies its
charging inequality. Established outside Lean by the Arb-based star-bound
certificate. Naming it does NOT prove it. -/
def AdmissiblePair (a₃ a₄ : ℝ) : Prop :=
  ∀ τ : ℝ, τ ∈ Set.Icc (-3 : ℝ) 3 → ∃ t : ℝ,
    (∀ k : ℕ, k ≤ 3 → starBound (floorsThree k) τ - (k : ℝ) * t ≤ a₃) ∧
    (∀ j : ℕ, j ≤ 4 → starBound (floorsFour j) τ + (j : ℝ) * t ≤ a₄)

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

/-- Theorem 7.1 (`thm:deg4`)(a). (Without a comparison conjunct.) -/
def Theorem2a : Prop := UniformDegreeFourBound F4

/-- Theorem 7.1 (`thm:deg4`)(b). `0.2575 = 103/400`. -/
def Theorem2b : Prop := UniformDegreeCountBound Fcubic (103 / 400)

/-- Theorem 7.1 (`thm:deg4`)(c). -/
def Theorem2c : Prop := UniformDegreeCountBound (5 / 32) (1 / 4)

/-- PROOF TARGETS. These are the propositions the proof work must establish.
(a) depends on H1 only; (b) and (c) depend on H2 only, at their own pair. -/
def Target2a : Prop := SimplexFourClaim → Theorem2a

def Target2b : Prop := AdmissiblePair Fcubic (103 / 400) → Theorem2b

def Target2c : Prop := AdmissiblePair (5 / 32) (1 / 4) → Theorem2c

end T2
end CubicPathwidth

/-! ## 7. Elaboration checks (not proofs of the claims) -/
#check CubicPathwidth.T2.Target2a
#check CubicPathwidth.T2.Target2b
#check CubicPathwidth.T2.Target2c
#print CubicPathwidth.T2.SimplexFourClaim
#print CubicPathwidth.T2.AdmissiblePair
#print CubicPathwidth.T2.UniformDegreeCountBound