CubicPathwidth.Sw4Spec

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

import CubicPathwidth.PwSeqSpec

/-!
# Specification: Theorem 8.2 (`thm:switched4`) (the switched sweep for maximum degree 4) and
# Theorem 9.2 (`thm:pw-seq`) for the seed `M = (c₃, 0.2627)`

STATUS: approved by the author on 2026-10-16. 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 `targetThm62`, `targetThm1M` in `Sw4/Targets.lean`.


It imports the approved specification `PwSeqSpec.lean` (and through it `T4Spec.lean`,
`T3Spec.lean`, `T2Spec.lean`, `C3Spec.lean`) unchanged, and reuses `HasPathwidthAtMost`,
`UniformDegreeCountBound`, `IsCorrelation`, `starBound`, `typeFloors`, `transferTerm`,
`coeff`, `c3` and `PathwidthSequence`.

Research statements (the paper):
* Theorem 8.2 (`thm:switched4`): if `Δ(G) ≤ 4`, then
  `pw(G) ≤ c₃ n₃ + 0.2627 n₄ + o(n)`;
* Theorem 9.2 (`thm:pw-seq`), seed `M = (c₃, 0.2627)`: a pathwidth sequence.
The proof uses two computer-assisted certificates, stated below as explicit
hypotheses: Lemma A.10 (`lem:switch-mixed`) (box certificates of Appendix A.3.2 (`sec:switch-cert-intro`)) and
Proposition A.13 (`prop:certificate-switched`) (Arb problem `S-switched`).

This file is the APPROVAL SURFACE.
-/

noncomputable section

namespace CubicPathwidth
namespace Sw4

open MeasureTheory ProbabilityTheory T2 T3 PwSeq

/-! ## 1. Constants -/

/-- The degree-4 coefficient `0.2627`. -/
def aM : ℝ := 2627 / 10000

/-- The amount `s = 0.1529003 - c₃ ≈ 0.0130782` that a vertex of degree 3 sends to each
neighbor of degree 4 at threshold zero. -/
def sM : ℝ := 1529003 / 10000000 - C3.c3

/-! ## 2. The switch quantity at threshold zero -/

/-- `N(x)`: the number of neighbor coordinates `1, …, d` that are strictly positive. -/
def posCount {d : ℕ} (x : EuclideanSpace ℝ (Fin (d + 1))) : ℕ := by
  classical
  exact (Finset.univ.filter fun i : Fin d => 0 < x i.succ).card

/-- `Ψ(Y₀; Y₁, …, Y_d) = E[1{Y₀ ≤ 0} ⌈N/2⌉]` for a centered Gaussian vector
`(Y₀, …, Y_d)` with covariance matrix `S`, where `N = #{i ≥ 1 : Y_i > 0}`.
`⌈N/2⌉` is written `(N + 1) / 2` (division of natural numbers rounds down). -/
def psi {d : ℕ} (S : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ) : ℝ :=
  ∫ x, (if x 0 ≤ 0 then (((posCount x + 1) / 2 : ℕ) : ℝ) else 0)
    ∂(multivariateGaussian 0 S)

/-- The class of vectors of Lemma A.10 (`lem:switch-mixed`): `S` is the covariance matrix of a centered Gaussian
vector with unit variances (a correlation matrix) and `Corr(Y₀, Y_{i+1}) ≥ r_i`. -/
def SwitchAdmissible {d : ℕ} (r : Fin d → ℝ) (S : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ) :
    Prop :=
  IsCorrelation S ∧ ∀ i : Fin d, r i ≤ S 0 i.succ

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

/-- HYPOTHESIS H6 (`lem:switch-mixed`, as stated; certificates of
Appendix A.3.2 (`sec:switch-cert-intro`)). Let `(Y₀, …, Y_d)` be a centered Gaussian vector with unit variances and
`Corr(Y₀, Y_i) ≥ r_i`.
(a) If `d = 3` and `r` is a permutation of `(r₃₃, r₃₃, r₃₄)`, then `Ψ ≤ 0.1529003`.
(b) If `d = 3` and `r` is a permutation of `(r₃₃, r₃₄, r₃₄)`, then `Ψ ≤ 0.165616`.
(c) If `d = 4`, `0 ≤ j ≤ 4`, and `j` of the `r_i` equal `r₃₄` and the other `4 - j`
    equal `r₄₄`, then `Ψ ≤ 0.2627 - j s`.
`typeFloors d k₃ k₄` lists `k₃` floors `r_{d3}`, then `k₄` floors `r_{d4}`; composing
with every permutation `σ` gives every arrangement. Established outside Lean (the
reduction in the proof of Lemma A.10 (`lem:switch-mixed`) and Arb box certificates). Naming it does NOT
prove it. -/
def SwitchMixedClaim : Prop :=
  (∀ σ : Equiv.Perm (Fin 3), ∀ S : Matrix (Fin 4) (Fin 4) ℝ,
      SwitchAdmissible (typeFloors 3 2 1 ∘ σ) S → psi S ≤ 1529003 / 10000000) ∧
  (∀ σ : Equiv.Perm (Fin 3), ∀ S : Matrix (Fin 4) (Fin 4) ℝ,
      SwitchAdmissible (typeFloors 3 1 2 ∘ σ) S → psi S ≤ 165616 / 1000000) ∧
  (∀ j : ℕ, j ≤ 4 → ∀ σ : Equiv.Perm (Fin 4), ∀ S : Matrix (Fin 5) (Fin 5) ℝ,
      SwitchAdmissible (typeFloors 4 j (4 - j) ∘ σ) S → psi S ≤ aM - (j : ℝ) * sM)

/-- HYPOTHESIS H7 (`prop:certificate-switched`; Arb problem
`S-switched`). For every `τ ∈ [0, 35/32]` there is a transfer `t₃₄` such that every
`{3,4}`-type `(d; k₃, k₄)` other than the pure cubic type `(3; 3, 0)` satisfies
`C_T(τ) + λ_T(t₃₄, 0, 0) ≤ a_d` with `(a₃, a₄) = (c₃, 0.2627)`. Established outside
Lean by the Arb certificate. Naming it does NOT prove it. -/
def SwitchedChargingClaim : Prop :=
  ∀ τ : ℝ, τ ∈ Set.Icc (0 : ℝ) (35 / 32) → ∃ t₃₄ : ℝ,
    ∀ d k₃ k₄ : ℕ, (d = 3 ∨ d = 4) → k₃ + k₄ = d → ¬ (d = 3 ∧ k₃ = 3) →
      starBound (typeFloors d k₃ k₄) τ + transferTerm d k₃ k₄ 0 t₃₄ 0 0 ≤
        coeff C3.c3 aM 0 d

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

/-- Theorem 8.2 (`thm:switched4`): `pw(G) ≤ c₃ n₃ + 0.2627 n₄ + o(n)` for `Δ(G) ≤ 4`, uniformly. -/
def Theorem62 : Prop := UniformDegreeCountBound C3.c3 aM

/-- The seed `M = (c₃, 0.2627)`; only `d = 3, 4` are used (base degree `k = 4`). -/
def seqM : ℕ → ℝ := fun d => if d = 3 then C3.c3 else aM

/-- PROOF TARGETS. Both depend on H6 and H7 only. -/
def TargetThm62 : Prop := SwitchMixedClaim → SwitchedChargingClaim → Theorem62

def TargetThm1M : Prop :=
  SwitchMixedClaim → SwitchedChargingClaim → PathwidthSequence 4 seqM

end Sw4
end CubicPathwidth

/-! ## 5. Elaboration checks (not proofs of the claims) -/
#check CubicPathwidth.Sw4.TargetThm62
#check CubicPathwidth.Sw4.TargetThm1M
#print CubicPathwidth.Sw4.SwitchMixedClaim
#print CubicPathwidth.Sw4.SwitchedChargingClaim
#print CubicPathwidth.Sw4.psi
#print CubicPathwidth.Sw4.SwitchAdmissible
Back to top