2607.19268v1 / FiniteChecks.lean

all files

import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

/-!
# Decidable checks for the finite graphs in Theorem 1.1

The labels for the exceptional graphs follow the high-resolution rendering of
Figure 2: `0` and `1` are the left top/bottom vertices, followed from left to
right by the remaining vertices (upper before lower at equal horizontal level).
-/

namespace BootsRoyleCaoVince.FiniteChecks

/-- A `Fin n`-labelled copy of `K₂ ∨ P_(n-2)`: vertices `0,1` form `K₂`,
and vertices `2,...,n-1` form the path in increasing order. -/
def labeledH (n : ℕ) : SimpleGraph (Fin n) :=
  SimpleGraph.fromRel fun u v =>
    (u.val = 0 ∧ v.val = 1) ∨
    (u.val < 2 ∧ 2 ≤ v.val) ∨
    (2 ≤ u.val ∧ u.val + 1 = v.val)

instance (n : ℕ) : DecidableRel (labeledH n).Adj := by
  intro u v
  change Decidable
    (u ≠ v ∧
      (((u.val = 0 ∧ v.val = 1) ∨ (u.val < 2 ∧ 2 ≤ v.val) ∨
        (2 ≤ u.val ∧ u.val + 1 = v.val)) ∨
       ((v.val = 0 ∧ u.val = 1) ∨ (v.val < 2 ∧ 2 ≤ u.val) ∨
        (2 ≤ v.val ∧ v.val + 1 = u.val))))
  infer_instance

private def exceptional7Edges : List (ℕ × ℕ) :=
  [(0, 1),
   (0, 2), (0, 3), (0, 4), (0, 6),
   (1, 2), (1, 3), (1, 5), (1, 6),
   (2, 3),
   (3, 4), (3, 5), (3, 6),
   (4, 6), (5, 6)]

private def exceptional8Edges : List (ℕ × ℕ) :=
  [(0, 1),
   (0, 2), (0, 3), (0, 4), (0, 6), (0, 7),
   (1, 2), (1, 3), (1, 5), (1, 6), (1, 7),
   (2, 3),
   (3, 4), (3, 5), (3, 6),
   (4, 6), (5, 6),
   (6, 7)]

/-- The exceptional order-seven graph shown in Figure 2(a). -/
def exceptional7 : SimpleGraph (Fin 7) :=
  SimpleGraph.fromRel fun u v => (u.val, v.val) ∈ exceptional7Edges

instance : DecidableRel exceptional7.Adj := by
  intro u v
  change Decidable
    (u ≠ v ∧ ((u.val, v.val) ∈ exceptional7Edges ∨
      (v.val, u.val) ∈ exceptional7Edges))
  infer_instance

/-- The exceptional order-eight graph shown in Figure 2(b). -/
def exceptional8 : SimpleGraph (Fin 8) :=
  SimpleGraph.fromRel fun u v => (u.val, v.val) ∈ exceptional8Edges

instance : DecidableRel exceptional8.Adj := by
  intro u v
  change Decidable
    (u ≠ v ∧ ((u.val, v.val) ∈ exceptional8Edges ∨
      (v.val, u.val) ∈ exceptional8Edges))
  infer_instance

example : (labeledH 7).edgeFinset.card = 15 := by native_decide
example : exceptional7.edgeFinset.card = 15 := by native_decide
example : (labeledH 8).edgeFinset.card = 18 := by native_decide
example : exceptional8.edgeFinset.card = 18 := by native_decide

example : List.ofFn (fun v : Fin 7 => exceptional7.degree v) = [5, 5, 3, 6, 3, 3, 5] := by
  native_decide

example : List.ofFn (fun v : Fin 8 => exceptional8.degree v) = [6, 6, 3, 6, 3, 3, 6, 3] := by
  native_decide

#print axioms BootsRoyleCaoVince.FiniteChecks.exceptional7
#print axioms BootsRoyleCaoVince.FiniteChecks.exceptional8

end BootsRoyleCaoVince.FiniteChecks