Graph minors, complete minors, the statement $\mathrm{HC}(t)$ , and degeneracy

Definition

HadwigerConj_Defs

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-coloringgraph-minorsgraph-theory

All graphs are simple (no loops or parallel edges).

Minor. A graph $H$ with vertex set $W$ is a minor of a graph $G$ with vertex set $V$ if there are branch sets $B_w\subseteq V$ , one for each $w\in W$ , such that each $B_w$ induces a connected (hence nonempty) subgraph of $G$ , distinct branch sets are disjoint, and for every edge $w_1w_2$ of $H$ some vertex of $B_{w_1}$ is adjacent in $G$ to some vertex of $B_{w_2}$ . This is equivalent to the usual definition: $H$ is isomorphic to a graph obtained from a subgraph of $G$ by contracting edges.
Complete minor. $G$ has a $K_t$ minor if the complete graph $K_t$ is a minor of $G$ .
$\mathrm{HC}(t)$ . For an integer $t\ge 0$ , $\mathrm{HC}(t)$ is the statement “every finite graph with no $K_{t+1}$ minor is $t$ -colourable”.
Degeneracy. $G$ is $k$ -degenerate if every nonempty set $S$ of vertices contains a vertex having at most $k$ neighbours in $S$ .

These are the basic notions of Seymour's survey (Section 1 and Section 3) and are shared by every statement of this mission.

Formalization Note Minors are encoded by branch sets (a minor model). $\mathrm{HC}(t)$ quantifies over all finite vertex types in Type. Degeneracy is phrased with induced subgraphs (vertex subsets); this is equivalent to the survey's “every non-null subgraph has a vertex of degree at most $k$ ”, since passing from a subgraph to the induced subgraph on the same vertex set can only raise degrees.

Definition code

import Mathlib

namespace HadwigerConj

/-- `IsMinor H G`: the graph `H` is a minor of the graph `G`, expressed through branch sets.
There is a family `B w` (one for each vertex `w` of `H`) of vertex sets of `G` such that
each `B w` induces a connected (in particular nonempty) subgraph of `G`, distinct branch sets
are disjoint, and whenever `w₁ w₂` is an edge of `H` some vertex of `B w₁` is adjacent in `G`
to some vertex of `B w₂`. -/
def IsMinor {W V : Type*} (H : SimpleGraph W) (G : SimpleGraph V) : Prop :=
  ∃ B : W → Set V,
    (∀ w, (G.induce (B w)).Connected) ∧
    (∀ w₁ w₂, w₁ ≠ w₂ → Disjoint (B w₁) (B w₂)) ∧
    (∀ w₁ w₂, H.Adj w₁ w₂ → ∃ u ∈ B w₁, ∃ v ∈ B w₂, G.Adj u v)

/-- `HasCompleteMinor G t`: the complete graph `K_t` is a minor of `G`. -/
def HasCompleteMinor {V : Type*} (G : SimpleGraph V) (t : ℕ) : Prop :=
  IsMinor (⊤ : SimpleGraph (Fin t)) G

/-- `HC t`: every finite graph with no `K_{t+1}` minor is `t`-colourable. -/
def HC (t : ℕ) : Prop :=
  ∀ (V : Type) [Finite V] (G : SimpleGraph V), ¬ HasCompleteMinor G (t + 1) → G.Colorable t

/-- `IsDegenerate G k`: every nonempty set `S` of vertices contains a vertex with at most `k`
neighbours inside `S` (i.e. every non-null induced subgraph has a vertex of degree `≤ k`). -/
def IsDegenerate {V : Type*} (G : SimpleGraph V) (k : ℕ) : Prop :=
  ∀ S : Set V, S.Nonempty → ∃ v ∈ S, (G.neighborSet v ∩ S).ncard ≤ k

end HadwigerConj

Source

P. Seymour, "Hadwiger's conjecture" (survey), in: Open Problems in Mathematics, Springer, 2016 (uploaded PDF `paper.pdf`), Section 1 (definition of minor, statement 1.1 and HC(t)) and Section 3 (definition of k-degenerate, p. 4); Wikipedia, "Hadwiger conjecture (graph theory)", https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Note — non-blind read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the intended meaning. It is not independent or blind testimony, and no reviewer should treat it as such; an independent audit is still needed.

This file declares four notions.

$\mathrm{IsMinor}(H,G)$ , for a graph $H$ $H$ on a vertex type $W$ $W$ and a graph $G$ $G$ on a vertex type $V$ $V$ (arbitrary types, possibly infinite): there exists a family of vertex sets $B_w\subseteq V$ $B_{w} \subseteq V$ , indexed by $w\in W$ $w \in W$ , such that
- for every $w$ , the subgraph of $G$ induced on $B_w$ is connected (connected includes nonempty);
- for all $w_1\neq w_2$ , $B_{w_1}$ and $B_{w_2}$ are disjoint;
- for all $w_1,w_2$ adjacent in $H$ , there exist $u\in B_{w_1}$ and $v\in B_{w_2}$ adjacent in $G$ .
$\mathrm{HasCompleteMinor}(G,t)$ , for $t\in\mathbb N$ : $\mathrm{IsMinor}(K_t,G)$ where $K_t$ is the complete graph on $\{0,\dots,t-1\}$ . For $t=0$ it is true for every $G$ (empty family).
$\mathrm{HC}(t)$ , for $t\in\mathbb N$ : for every finite type $V$ (in the lowest universe) and every simple graph $G$ on $V$ , if $G$ does not have a $K_{t+1}$ minor then $G$ admits a proper colouring with $t$ colours (adjacent vertices get different colours; with $t=0$ this requires $V$ empty).
$\mathrm{IsDegenerate}(G,k)$ : for every nonempty set $S\subseteq V$ there is $v\in S$ such that the number of neighbours of $v$ lying in $S$ is at most $k$ . The count is the cardinality of a set, with the convention that an infinite set counts as $0$ ; so for infinite $V$ this count is junk, while for finite $V$ it is the usual count.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Nov 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Graph minors, complete minors, the statement HC(t)\mathrm{HC}(t)HC(t), and degeneracy

Graph minors, complete minors, the statement $\mathrm{HC}(t)$ , and degeneracy