2607.19268v1 / Repro.lean

all files

import Mathlib.Analysis.Matrix.Spectrum
import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Combinatorics.SimpleGraph.LapMatrix
import Mathlib.Combinatorics.SimpleGraph.Maps
import Mathlib.Topology.Instances.Real.Lemmas

/-!
# A faithful statement of the Boots–Royle/Cao–Vince conjecture

The paper uses finite simple graphs.  Mathlib supplies simple graphs, path graphs,
adjacency matrices, and ordered eigenvalues of Hermitian matrices, but currently
has no planarity predicate or graph-join constructor.  The definitions below fill
exactly those two gaps.

`PlaneDrawing` is the standard topological definition of a plane graph: vertices
are distinct points and edges are simple continuous arcs whose interiors contain
no vertex and are pairwise disjoint.  Since every edge is represented with its
smaller endpoint first, there is exactly one arc per undirected edge.
-/

open Set

namespace BootsRoyleCaoVince

/-- A crossing-free topological drawing of a finite simple graph in `ℝ²`. -/
structure PlaneDrawing {n : ℕ} (G : SimpleGraph (Fin n)) where
  vertex : Fin n → ℝ × ℝ
  vertex_injective : Function.Injective vertex
  edge : Fin n → Fin n → ℝ → ℝ × ℝ
  edge_continuous : ∀ u v : Fin n, G.Adj u v → u < v →
    ContinuousOn (edge u v) (Icc (0 : ℝ) 1)
  edge_start : ∀ u v : Fin n, G.Adj u v → u < v → edge u v 0 = vertex u
  edge_finish : ∀ u v : Fin n, G.Adj u v → u < v → edge u v 1 = vertex v
  edge_injective : ∀ u v : Fin n, G.Adj u v → u < v →
    InjOn (edge u v) (Icc (0 : ℝ) 1)
  edge_interior_avoids_vertices : ∀ u v : Fin n, G.Adj u v → u < v →
    ∀ t ∈ Ioo (0 : ℝ) 1, ∀ w, edge u v t ≠ vertex w
  distinct_edge_interiors_disjoint : ∀ u v a b : Fin n,
    G.Adj u v → u < v → G.Adj a b → a < b →
    (u ≠ a ∨ v ≠ b) →
    Disjoint (edge u v '' Ioo (0 : ℝ) 1) (edge a b '' Ioo (0 : ℝ) 1)

/-- A graph is planar when it admits a crossing-free topological drawing in the plane. -/
def IsPlanar {n : ℕ} (G : SimpleGraph (Fin n)) : Prop :=
  Nonempty (PlaneDrawing G)

/-- The join of two simple graphs: retain both graphs and add every cross-edge. -/
def graphJoin {V W : Type*} (G : SimpleGraph V) (H : SimpleGraph W) :
    SimpleGraph (V ⊕ W) where
  Adj
    | .inl u, .inl v => G.Adj u v
    | .inr u, .inr v => H.Adj u v
    | .inl _, .inr _ => True
    | .inr _, .inl _ => True
  symm.symm
    | .inl _, .inl _, h => G.adj_symm h
    | .inr _, .inr _, h => H.adj_symm h
    | .inl _, .inr _, _ => trivial
    | .inr _, .inl _, _ => trivial
  loopless.irrefl
    | .inl _ => G.irrefl
    | .inr _ => H.irrefl

/-- The paper's candidate `Hₙ = K₂ ∨ P_(n-2)`. -/
def H (n : ℕ) : SimpleGraph (Fin 2 ⊕ Fin (n - 2)) :=
  graphJoin (SimpleGraph.completeGraph (Fin 2)) (SimpleGraph.pathGraph (n - 2))

/-- The largest (not largest-absolute-value) eigenvalue of the real adjacency matrix.
This is the adjacency spectral radius used in the paper. -/
noncomputable def adjacencySpectralRadius {n : ℕ} (G : SimpleGraph (Fin n)) : ℝ := by
  classical
  exact if hn : 0 < n then
      (G.isHermitian_adjMatrix ℝ).eigenvalues₀
        ⟨0, by simpa using hn⟩
    else
      0

/-- `G` is a planar graph attaining the maximum adjacency spectral radius at its order. -/
def IsPlanarSpectralMaximizer {n : ℕ} (G : SimpleGraph (Fin n)) : Prop :=
  IsPlanar G ∧
    ∀ G' : SimpleGraph (Fin n), IsPlanar G' →
      adjacencySpectralRadius G' ≤ adjacencySpectralRadius G

/-- Faithful Lean statement of the original Boots–Royle/Cao–Vince conjecture,
which is the `n ≥ 9` central result proved by the paper.  The biconditional says
both that `H n` attains the maximum and that it is unique up to graph isomorphism. -/
def CentralClaim : Prop :=
  ∀ n : ℕ, 9 ≤ n → ∀ G : SimpleGraph (Fin n),
    IsPlanarSpectralMaximizer G ↔ Nonempty (G ≃g H n)

#check CentralClaim
#print axioms CentralClaim

end BootsRoyleCaoVince