# Verification

<!-- Generated by `lean-pkg page total-coloring-lean` (site output) from coverage.yaml, claims.yaml, the claims ledger and the receipts committed under .lean-receipts/. Do not edit: change the data and render it again. -->

## Verification at a glance

**How to read this page.** Lean has checked every step of the proofs listed here. Each result is exactly its Lean statement: read the statements below to see what is proved. The titles, the words and the notes are the authors' description, which Lean does not check.

Unconditionally, every finite graph with \|V\| &lt;= 2 \* maxDegree has a total coloring with maxDegree + 3 colors, and every finite auxiliary-class member has a (D + 2)-edge coloring rainbow on J; the D + 2 transfer, the partition entry point and the (q + 1)-color endpoints are conditional on supplied inputs, and the Total Coloring Conjecture is not proved.

- Main results: 13; verified: 13 of 13 (for 8 of them a second checker also compared the statement).

## Main results

### Total coloring with maxDegree + 3 colors when \|V\| &lt;= 2 \* maxDegree

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $G$ be a finite simple graph on the vertex set $V$ with
$|V| \le 2\Delta(G)$. Then $G$ has a total coloring with the
$\Delta(G)+3$ colors $\{0,1,\dots,\Delta(G)+2\}$: adjacent vertices get
distinct colors, two distinct edges sharing an endpoint get distinct
colors, and every vertex gets a color different from each edge
incident with it.
```

**In Lean.** `TotalColoringAudit.HighDegree.exists_total_coloring_of_card_le_two_mul_maxDegree` in [Audit/HighDegree/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/HighDegree/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem exists_total_coloring_of_card_le_two_mul_maxDegree
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    ∃ (vertexColor : V → Fin (G.maxDegree + 1 + 2))
      (edgeColor : G.edgeSet → Fin (G.maxDegree + 1 + 2)),
      (∀ v w, G.Adj v w → vertexColor v ≠ vertexColor w) ∧
      (∀ e f, G.lineGraph.Adj e f → edgeColor e ≠ edgeColor f) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) → vertexColor v ≠ edgeColor e)
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Unconditional: the only hypotheses are a finite vertex type, decidable adjacency and the order bound; the empty vertex type is included and there is no parity hypothesis. ExtensionPalette (maxDegree + 1) is Fin (maxDegree + 3).

### Every finite auxiliary-class member has a (D + 2)-edge coloring rainbow on its distinguished set

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $H$ be a finite simple graph and $J$ a finite set of unordered pairs
of vertices such that $(H,J)$ is in the auxiliary class
$\mathcal{A}_D$: there are a vertex $x$ and a set $M$ of pairwise
disjoint pairs with $J = M \cup \{\text{edges of } H \text{ at } x\}$,
every pair of $J$ an edge of $H$, no pair of $M$ containing $x$ or a
neighbor of $x$, every vertex other than $x$ in exactly one pair of $J$,
$|J| = D$, $\Delta(H) \le D$ and $2 \le \deg_H(x) \le D$. Then $H$ has a
proper edge coloring with $D+2$ colors in which the edges of $J$ get
pairwise distinct colors.
```

**In Lean.** `TotalColoringAudit.AuxiliaryClass.exists_rainbow_edge_coloring_of_auxiliaryClass` in [Audit/AuxiliaryClass/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/AuxiliaryClass/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem exists_rainbow_edge_coloring_of_auxiliaryClass
    {V : Type*} [Fintype V] [DecidableEq V]
    (D : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj]
    (J : Finset (Sym2 V)) (x : V) (M : Finset (Sym2 V))
    (distinguished_edges : ∀ ⦃e⦄, e ∈ J → e ∈ H.edgeSet)
    (matching : ∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f)
    (matching_off_center : ∀ ⦃e⦄, e ∈ M → x ∉ e)
    (matching_avoids_center_neighbors : ∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H.Adj x v)
    (decomposition : J = M ∪ H.incidenceFinset x)
    (exact_coverage : ∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e)
    (card_distinguished : J.card = D)
    (maxDegree_bound : H.maxDegree ≤ D)
    (center_degree : 2 ≤ H.degree x ∧ H.degree x ≤ D) :
    ∃ color : H.edgeSet → Fin (D + 2),
      (∀ e f, H.lineGraph.Adj e f → color e ≠ color f) ∧
      (∀ e f : H.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
        color e ≠ color f)
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Unconditional for every D and every finite member; proved by contradiction from the minimal-counterexample theorem below.

### No auxiliary-class member is noncolorable and minimal in the number of edges outside J

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
There is no finite $(H,J) \in \mathcal{A}_D$ such that $H$ has no proper
$(D+2)$-edge coloring rainbow on $J$, while every $(H',J) \in
\mathcal{A}_D$ on the same vertex set, with the same $J$ and with no such
coloring, has at least as many edges outside $J$ as $H$.
```

**In Lean.** `TotalColoringAudit.CriticalAllD.false_of_critical_allD` in [Audit/CriticalAllD/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/CriticalAllD/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem false_of_critical_allD
    {V : Type*} [Fintype V] [DecidableEq V]
    (D : ℕ) (H : SimpleGraph V) [DecidableRel H.Adj] (J : Finset (Sym2 V))
    (member : ∃ (x : V) (M : Finset (Sym2 V)),
      (∀ ⦃e⦄, e ∈ J → e ∈ H.edgeSet) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
      (∀ ⦃e⦄, e ∈ M → x ∉ e) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H.Adj x v) ∧
      J = M ∪ H.incidenceFinset x ∧
      (∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e) ∧
      J.card = D ∧
      H.maxDegree ≤ D ∧
      (2 ≤ H.degree x ∧ H.degree x ≤ D))
    (noncolorable : ¬∃ color : H.edgeSet → Fin (D + 2),
      (∀ e f, H.lineGraph.Adj e f → color e ≠ color f) ∧
      (∀ e f : H.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
        color e ≠ color f))
    (minimal : ∀ (H₁ : SimpleGraph V) [DecidableRel H₁.Adj],
      (∃ (x : V) (M : Finset (Sym2 V)),
        (∀ ⦃e⦄, e ∈ J → e ∈ H₁.edgeSet) ∧
        (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
        (∀ ⦃e⦄, e ∈ M → x ∉ e) ∧
        (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬H₁.Adj x v) ∧
        J = M ∪ H₁.incidenceFinset x ∧
        (∀ v, v ≠ x → ∃! e : Sym2 V, e ∈ J ∧ v ∈ e) ∧
        J.card = D ∧
        H₁.maxDegree ≤ D ∧
        (2 ≤ H₁.degree x ∧ H₁.degree x ≤ D)) →
      (¬∃ color : H₁.edgeSet → Fin (D + 2),
        (∀ e f, H₁.lineGraph.Adj e f → color e ≠ color f) ∧
        (∀ e f : H₁.edgeSet, (e : Sym2 V) ∈ J → (f : Sym2 V) ∈ J → e ≠ f →
          color e ≠ color f)) →
      (H.edgeSet \ (J : Set (Sym2 V))).ncard ≤ (H₁.edgeSet \ (J : Set (Sym2 V))).ncard) :
    False
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** The minimal-counterexample step behind the rainbow theorem above; the minimality ranges over members on the same vertex type with the same J.

### A proper selector-rainbow auxiliary edge coloring decodes to a valid total coloring

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $G$ and $H$ be simple graphs with an extension datum: a selector
edge $s(v)$ of $H$ for each vertex $v$ of $G$ and an edge $\iota(e)$ of
$H$ for each edge $e$ of $G$, such that adjacent vertices have distinct
selectors, distinct edges of $G$ sharing an endpoint go to distinct edges
of $H$ sharing an endpoint, and $s(v)$ and $\iota(e)$ are distinct and
share an endpoint whenever $v$ is an endpoint of $e$. If $c$ is a proper
edge coloring of $H$ that gives distinct selector edges distinct colors,
then coloring each vertex $v$ by $c(s(v))$ and each edge $e$ by
$c(\iota(e))$ is a valid total coloring of $G$.
```

**In Lean.** `TotalColoringAudit.Decode.decode_valid` in [Audit/Decode/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/Decode/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem decode_valid
    {V : Type*} {W : Type*} {C : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (classEdge : V → H.edgeSet) (originalEdge : G.edgeSet → H.edgeSet)
    (classEdge_ne_of_adj : ∀ {v w : V}, G.Adj v w → classEdge v ≠ classEdge w)
    (originalEdge_adj : ∀ {e f : G.edgeSet}, G.lineGraph.Adj e f →
      H.lineGraph.Adj (originalEdge e) (originalEdge f))
    (classEdge_adj_original : ∀ {v : V} {e : G.edgeSet}, v ∈ (e : Sym2 V) →
      H.lineGraph.Adj (classEdge v) (originalEdge e))
    (color : H.edgeSet → C)
    (hvalid : ∀ e f, H.lineGraph.Adj e f → color e ≠ color f)
    (hrainbow : ∀ v w, classEdge v ≠ classEdge w →
      color (classEdge v) ≠ color (classEdge w)) :
    (∀ v w, G.Adj v w → color (classEdge v) ≠ color (classEdge w)) ∧
      (∀ e f, G.lineGraph.Adj e f → color (originalEdge e) ≠ color (originalEdge f)) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        color (classEdge v) ≠ color (originalEdge e))
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** No finiteness and any color type; the extension data are hypotheses.

### Conditional transfer: a supplied extension into an auxiliary-class member gives a total coloring with D + 2 colors

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

**In words.**

```latex
Let $G$ be a simple graph and $H$ a finite simple graph with
$(H,J) \in \mathcal{A}_D$. If there is an extension datum from $G$ to $H$
(as in the decoding theorem) every selector edge of which belongs to
$J$, then $G$ has a valid total coloring with $D+2$ colors.
```

**In Lean.** `TotalColoring.Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass` in [TotalColoring/AuxiliaryTransfer.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/TotalColoring/AuxiliaryTransfer.lean).

```lean
theorem exists_valid_decode_of_inAuxiliaryClass
    [Fintype W] [DecidableEq W]
    (D : ℕ) (X : Extension G H) [DecidableRel H.Adj]
    (J : Finset (Sym2 W))
    (hclassEdge : ∀ vertex, X.classEdge vertex ∈ distinguishedEdgeSet H J)
    (hmember : InAuxiliaryClass D H J) :
    ∃ assignment : Assignment G (ExtensionPalette D), assignment.Valid
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Conditional on the supplied extension datum, selector membership in J and the auxiliary-class membership; nothing relates D to the maximum degree of G.

### A matching with at least k edges from minimum degree k and order at least 2k

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $H$ be a finite simple graph on $V$ and $k \ge 0$. If every vertex
has degree at least $k$ in $H$ and $2k \le |V|$, then $H$ has a subgraph
in which every vertex has at most one neighbor (a matching) with at
least $k$ edges.
```

**In Lean.** `TotalColoringAudit.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_ge` in [Audit/MatchingLowerBound/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/MatchingLowerBound/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem exists_matchingGraph_edgeFinset_card_ge
    {V : Type*} [Fintype V]
    (H : SimpleGraph V) [DecidableRel H.Adj] (k : ℕ)
    (hdegree : ∀ v, k ≤ H.degree v) (horder : 2 * k ≤ Fintype.card V) :
    ∃ (M : SimpleGraph V) (_ : DecidableRel M.Adj),
      M ≤ H ∧ (∀ v, (M.neighborSet v).Subsingleton) ∧ k ≤ M.edgeFinset.card
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

### A pair/singleton partition with maxDegree + 1 classes gives auxiliary-class membership when \|V\| &lt;= 2 \* maxDegree

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $G$ be a finite simple graph on $V$ and fix a partition of $V$ into
singletons and pairs of nonadjacent vertices. On $V \cup \{\ast\}$ take
a copy of $G$ together with one selector edge per class: $\ast v$ for a
singleton $\{v\}$ and $vw$ for a pair $\{v,w\}$. Let $J$ be the set of
selector edges and $M$ the pair selectors. If $|J| = \Delta(G)+1$ and
$|V| \le 2\Delta(G)$, then this graph is a member of
$\mathcal{A}_{\Delta(G)+1}$ with center $\ast$, distinguished set $J$
and matching part $M$.
```

**In Lean.** `TotalColoringAudit.PairSingleton.isAuxiliaryClassMember_of_highDegree` in [Audit/PairSingleton/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/PairSingleton/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem isAuxiliaryClassMember_of_highDegree
    {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    (partner : V → Option V)
    (partner_ne : ∀ {v w : V}, partner v = some w → v ≠ w)
    (partner_symm : ∀ {v w : V}, partner v = some w → partner w = some v)
    (partner_nonadjacent : ∀ {v w : V}, partner v = some w → ¬G.Adj v w)
    (selector : V → Sym2 (Option V))
    (hselector : ∀ v, selector v = (partner v).elim s(none, some v) (fun w ↦ s(some v, some w)))
    (J : Finset (Sym2 (Option V))) (hJ : J = Finset.univ.image selector)
    (M : Finset (Sym2 (Option V))) (hM : M = J.filter (fun e ↦ (none : Option V) ∉ e))
    (A : SimpleGraph (Option V))
    (hA : A = G.map Function.Embedding.some ⊔ SimpleGraph.fromEdgeSet (J : Set (Sym2 (Option V))))
    [DecidableRel G.Adj] [DecidableRel A.Adj]
    (hclasses : J.card = G.maxDegree + 1)
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    (∀ ⦃e⦄, e ∈ J → e ∈ A.edgeSet) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃f⦄, f ∈ M → e ≠ f → ∀ ⦃v⦄, v ∈ e → v ∉ f) ∧
      (∀ ⦃e⦄, e ∈ M → (none : Option V) ∉ e) ∧
      (∀ ⦃e⦄, e ∈ M → ∀ ⦃v⦄, v ∈ e → ¬A.Adj none v) ∧
      J = M ∪ A.incidenceFinset none ∧
      (∀ v, v ≠ none → ∃! e : Sym2 (Option V), e ∈ J ∧ v ∈ e) ∧
      J.card = G.maxDegree + 1 ∧
      A.maxDegree ≤ G.maxDegree + 1 ∧
      (2 ≤ A.degree none ∧ A.degree none ≤ G.maxDegree + 1)
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** The pair/singleton witness is a hypothesis here; the high-degree theorem above constructs one from a matching in the complement of G.

### Conditional: a supplied equitable independent partition gives a total coloring with maxDegree + 3 colors

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

**In words.**

```latex
Let $G$ be a finite simple graph on a nonempty vertex set $V$ with
$|V| \le 2\Delta(G)$. If $V$ is partitioned into exactly $\Delta(G)+1$
nonempty independent sets whose sizes differ by at most one, then $G$
has a valid total coloring with $\Delta(G)+3$ colors.
```

**In Lean.** `TotalColoring.Auxiliary.EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition` in [TotalColoring/EquitablePairSingleton.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/TotalColoring/EquitablePairSingleton.lean).

```lean
theorem exists_valid_assignment_of_highDegreePartition
    (Q : EquitableIndependentPartition G (G.maxDegree + 1))
    (hdense : Fintype.card V ≤ 2 * G.maxDegree) :
    ∃ assignment : Assignment G (ExtensionPalette (G.maxDegree + 1)),
      assignment.Valid
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Conditional on the supplied partition and a nonempty vertex type; retained as an alternate entry point. The high-degree theorem above assumes no partition.

### Conditional independent-seed endpoint: q + 1 colors from a proper q-edge coloring, an independent seed and a peel order

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

**In words.**

```latex
Let $G$ be a finite simple graph and $q > 0$. Suppose $G$ has a proper
edge coloring with $q$ colors, $A$ is an independent set of vertices,
and the vertices outside $A$ are listed without repetition as
$v_1,\dots,v_m$ (exactly the vertices outside $A$) so that for every $i$
the number of neighbors of $v_i$ among $v_{i+1},\dots,v_m$ is less than
$q - \deg_G(v_i)$ (truncated subtraction). Then $G$ has a valid total
coloring with $q+1$ colors. For $q = \Delta(G)+1$ this is
$\Delta(G)+2$ colors.
```

**In Lean.** `TotalColoring.exists_valid_assignment_of_independentSeedPeel` in [TotalColoring/IndependentSeed.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/TotalColoring/IndependentSeed.lean).

```lean
theorem exists_valid_assignment_of_independentSeedPeel {q : ℕ}
    (hq : 0 < q) (phi : EdgeAssignment G (Fin q)) (hphi : phi.Valid)
    (A : Finset V) (hA : G.IsIndepSet (A : Set V))
    (cert : IndependentSeedPeelCertificate G A q) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Conditional: the edge coloring, the seed and the peel order are hypotheses. Vizing's theorem and the existence of the seed and order are not proved, so the maxDegree + 2 case is not the Total Coloring Conjecture.

### Conditional selector decoder: a fresh-color independent set and matching with a peeled core coloring give q + 1 colors

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

**In words.**

```latex
Let $G$ be a finite simple graph with a proper edge coloring $\varphi$
with $q$ colors. Let $S$ be an independent set, $F$ a matching none of
whose edges has an endpoint in $S$, and $K \supseteq S$ a vertex set
with $g_0 \colon V \to \{0,\dots,q-1\}$ such that for all
$v, w \in K \setminus S$: $g_0(v) \ne \varphi(e)$ for every edge
$e \notin F$ at $v$, and $g_0(v) \ne g_0(w)$ when $v$ and $w$ are
adjacent. Suppose the vertices outside $K$ are listed without repetition
as $v_1,\dots,v_m$ (exactly the vertices outside $K$) so that
$|N(v_i) \cap ((K \setminus S) \cup \{v_{i+1},\dots,v_m\})| <
q - \deg_G(v_i)$ (truncated subtraction) for every $i$. Then $G$ has a
valid total coloring with $q+1$ colors.
```

**In Lean.** `TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel` in [TotalColoring/TotalIndependentSelector.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/TotalColoring/TotalIndependentSelector.lean).

```lean
theorem exists_valid_assignment_of_totalIndependentSelectorPeel
    (phi : EdgeAssignment G (Fin q)) (hphi : phi.Valid)
    (S : Finset V) (hS : G.IsIndepSet (S : Set V))
    (F : Finset G.edgeSet) (hF : EdgeFinsetIsMatching (G := G) F)
    (havoid : EdgeFinsetAvoids (G := G) F S)
    (K : Finset V) (g₀ : V → Fin q)
    (hcore : SelectorOldColoringGoodOn G phi S F K g₀)
    (cert : SelectorCorePeelCertificate G S K q) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Conditional: the edge coloring, S, F, the core K, the core coloring g0 and the peel order are hypotheses; none of them is constructed.

### Partial-edge selector decoder: old edge colors need only be proper outside the fresh matching

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $G$ be a simple graph, $f \in \{0,\dots,q\}$ a fresh color, $S$
an independent set, $F$ a matching none of whose edges has an endpoint
in $S$, and $\varphi$ an edge coloring with $q$ colors in which two
distinct edges outside $F$ sharing an endpoint get distinct colors. Let
$g \colon V \to \{0,\dots,q-1\}$ satisfy, for $v, w \notin S$:
$g(v) \ne \varphi(e)$ for every edge $e \notin F$ at $v$, and
$g(v) \ne g(w)$ when $v$ and $w$ are adjacent. Color the vertices of $S$
and the edges of $F$ with $f$, and every other vertex $v$ and edge $e$
with the image of $g(v)$, resp. $\varphi(e)$, under the order-preserving
bijection from $q$ colors onto the $q+1$ colors other than $f$. This is
a valid total coloring with $q+1$ colors.
```

**In Lean.** `TotalColoringAudit.PartialEdgeSelector.partialEdgeSelectorAssignment_valid` in [Audit/PartialEdgeSelector/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/PartialEdgeSelector/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem partialEdgeSelectorAssignment_valid
    {V : Type*} [DecidableEq V] {G : SimpleGraph V} {q : ℕ}
    (fresh : Fin (q + 1)) (phi : G.edgeSet → Fin q)
    (S : Finset V) (F : Finset G.edgeSet) (g : V → Fin q)
    (hphi : ∀ e f : G.edgeSet, e ∉ F → f ∉ F → G.lineGraph.Adj e f → phi e ≠ phi f)
    (hS : G.IsIndepSet (S : Set V))
    (hF : ∀ ⦃e f : G.edgeSet⦄, e ∈ F → f ∈ F → ¬G.lineGraph.Adj e f)
    (havoid : ∀ ⦃v : V⦄, v ∈ S → ∀ ⦃e : G.edgeSet⦄, e ∈ F → v ∉ (e : Sym2 V))
    (hallowed : ∀ v, v ∉ S → ∀ e : G.edgeSet, v ∈ (e : Sym2 V) → e ∉ F → phi e ≠ g v)
    (hproper : ∀ v, v ∉ S → ∀ w, w ∉ S → G.Adj v w → g v ≠ g w) :
    (∀ v w, G.Adj v w →
        (if v ∈ S then fresh else fresh.succAbove (g v)) ≠
          (if w ∈ S then fresh else fresh.succAbove (g w))) ∧
      (∀ e f, G.lineGraph.Adj e f →
        (if e ∈ F then fresh else fresh.succAbove (phi e)) ≠
          (if f ∈ F then fresh else fresh.succAbove (phi f))) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        (if v ∈ S then fresh else fresh.succAbove (g v)) ≠
          (if e ∈ F then fresh else fresh.succAbove (phi e)))
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Every input is a hypothesis; no finiteness is assumed.

### Conditional alternating rainbow-path selector: a supplied path certificate gives q + 1 colors

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check that applies to this result passed (the build; its statement was not compared by a second checker).

**In words.**

```latex
Let $G$ be a finite simple graph with a proper edge coloring $\varphi_0$
with $q$ colors, and $K$ a vertex set. Suppose there are distinct
vertices $u_0,\dots,u_k$, exactly the vertices of $K$, with path edges
$e_i = u_i u_{i+1}$ ($0 \le i < k$) whose $\varphi_0$-colors are pairwise
distinct; a color $\sigma \in \{0,\dots,q-1\}$ of the same palette
that no edge receives under $\varphi_0$; edge sets $L$ and $F$ of $G$,
each a matching, such that the path edge $e_i$ lies in $L$ exactly for
even $i$ and in $F$ exactly for odd $i$ ($L$ and $F$ may also contain
edges off the path), with no edge of $F$ at $u_0$; a function
$c \colon V \to \{0,\dots,q-1\}$ with $c(u_{i+1}) = \varphi_0(e_i)$;
and a list without repetition of exactly
the vertices outside $K$ satisfying the core peel inequality of the
selector decoder for $S = \{u_0\}$ and $K$. Then $G$ has a valid total
coloring with $q+1$ colors.
```

**In Lean.** `TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector` in [TotalColoring/TotalIndependentSelector.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/TotalColoring/TotalIndependentSelector.lean).

```lean
theorem exists_valid_assignment_of_alternatingRainbowPathSelector
    (phi₀ : EdgeAssignment G (Fin q)) (hphi₀ : phi₀.Valid)
    (K : Finset V) (k : ℕ)
    (cert : AlternatingRainbowPathSelectorCertificate G phi₀ K k) :
    ∃ a : Assignment G (Fin (q + 1)), a.Valid
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Conditional: the proper edge coloring and the whole certificate (path, rainbow, spare color, matchings, core colors, peel order) are hypotheses; the existence of the path is not proved.

### Soundness of the executable extension checker

**Verified.** Lean accepts the proof, and lean-pkg's record shows every check of this result passed (the build, and the statement comparison).

**In words.**

```latex
Let $X$ be an extension datum from a finite graph $G$ to a finite graph
$H$ and $c$ an edge coloring of $H$ with a color type with decidable
equality. If the Boolean checker checkExtension accepts $(X, c)$, then
decoding $c$ through $X$ gives a valid total coloring of $G$. (The
checker accepts exactly when $c$ is proper and gives distinct selector
edges distinct colors; that equivalence is the separate lemma
checkExtension_eq_true_iff, not part of this claim.)
```

**In Lean.** `TotalColoringAudit.Certificate.checkExtension_sound` in [Audit/Certificate/Challenge.lean](https://github.com/chenle02/total-coloring-lean/blob/c025d20a182644bbacdd96165c93e1b8b2a403c6/Audit/Certificate/Challenge.lean): the statement the proof was checked against (the proof is in a separate file, and a second checker confirmed it proves exactly this).

```lean
theorem checkExtension_sound
    {V : Type*} {W : Type*} {C : Type*} {G : SimpleGraph V} {H : SimpleGraph W}
    (classEdge : V → H.edgeSet) (originalEdge : G.edgeSet → H.edgeSet)
    (classEdge_ne_of_adj : ∀ {v w : V}, G.Adj v w → classEdge v ≠ classEdge w)
    (originalEdge_adj : ∀ {e f : G.edgeSet}, G.lineGraph.Adj e f →
      H.lineGraph.Adj (originalEdge e) (originalEdge f))
    (classEdge_adj_original : ∀ {v : V} {e : G.edgeSet}, v ∈ (e : Sym2 V) →
      H.lineGraph.Adj (classEdge v) (originalEdge e))
    (color : H.edgeSet → C)
    [Fintype V] [Fintype W] [DecidableEq W] [DecidableRel H.Adj] [DecidableEq C]
    (h : (decide (∀ e f : H.edgeSet,
            (e ≠ f ∧ ∃ x : W, x ∈ (e : Sym2 W) ∧ x ∈ (f : Sym2 W)) → color e ≠ color f) &&
          decide (∀ v w : V, classEdge v ≠ classEdge w →
            color (classEdge v) ≠ color (classEdge w))) = true) :
    (∀ v w, G.Adj v w → color (classEdge v) ≠ color (classEdge w)) ∧
      (∀ e f, G.lineGraph.Adj e f → color (originalEdge e) ≠ color (originalEdge f)) ∧
      (∀ (v : V) (e : G.edgeSet), v ∈ (e : Sym2 V) →
        color (classEdge v) ≠ color (originalEdge e))
```

**Axioms.** At most `Classical.choice`, `Quot.sound`, `propext` (what the build check records for the whole package).

**Note.** Concerns well-typed Lean values only; parsing external data is outside the theorem.

Every result with each of its claims, in one table: [Coverage](coverage.md).

## What the checks establish

- **Every proof is checked by Lean.** The package builds; no `sorry` (an unfinished proof) remains; the only axioms used are `Classical.choice`, `Quot.sound`, `propext` (allowed: `propext`, `Quot.sound`, `Classical.choice`).
- **The statements shown are the ones proved.** For 8 statement(s), a second checker (comparator) confirmed that the proof proves exactly the statement shown, with only the permitted axioms, and independent Lean kernels replayed the proof.
- **Not checked by any tool:** that a title or note describes its Lean statement. A definition listed under *Definitions checked by a person* is compared by name and type only.

The full account of what each check covers and what it takes on trust is lean-pkg's [trust model](https://github.com/lean-pkg/lean-pkg/blob/main/docs/trust-model.md).

## How this was checked

- lean-pkg's claims ledger: **ready**, every required claim is closed by the recorded receipts; 8 of 8 required claim(s) verified (`sha256:23f4baa46a3fc93d…`).
- Build check (`lean-pkg gate`) at commit `c025d20a1826`: `sorry` count 0; axioms used: `Classical.choice`, `Quot.sound`, `propext`.
- Axioms of every claim: read from the built environment (Lean's `collectAxioms`) for all 13 claim(s) in `claims.yaml`, not only the theorems the build prints; none uses an axiom beyond `propext`, `Quot.sound` and `Classical.choice`.
- Toolchain advisory: the build check ran on Lean `leanprover/lean4:v4.32.0`, which has a known soundness bug fixed in `v4.32.1` ([lean-v4.32.1-kernel-opaque-fvars](https://lean-lang.org/doc/reference/latest/releases/v4.32.1/); lean-pkg's [toolchain advisories](https://github.com/lean-pkg/lean-pkg/blob/main/src/lean_pkg/data/toolchain-advisories.yaml)).
- Toolchain advisory: the build check ran on Lean `leanprover/lean4:v4.32.0`, which has a known soundness bug fixed in `v4.32.2` ([lean-v4.32.2-kernel-nested-inductive](https://lean-lang.org/doc/reference/latest/releases/v4.32.2/); lean-pkg's [toolchain advisories](https://github.com/lean-pkg/lean-pkg/blob/main/src/lean_pkg/data/toolchain-advisories.yaml)).
- Toolchain advisory: the build check ran on Lean `leanprover/lean4:v4.32.0`, which has a known soundness bug fixed in `v4.33.1` ([lean-v4.33.1-kernel-and-runtime](https://lean-lang.org/doc/reference/latest/releases/v4.33.1/); lean-pkg's [toolchain advisories](https://github.com/lean-pkg/lean-pkg/blob/main/src/lean_pkg/data/toolchain-advisories.yaml)).
- Toolchain advisory: the build check ran on Lean `leanprover/lean4:v4.32.0`, which has a known soundness bug fixed in `v4.34.1` ([lean-v4.34.1-runtime-refcounts](https://lean-lang.org/doc/reference/latest/releases/v4.34.1/); lean-pkg's [toolchain advisories](https://github.com/lean-pkg/lean-pkg/blob/main/src/lean_pkg/data/toolchain-advisories.yaml)).
- Statement comparison (comparator) at commit `c025d20a1826`: 8 configuration(s), 8 theorem(s) compared (each Challenge statement against its Solution proof); permitted axioms: `Classical.choice`, `Quot.sound`, `propext`; definitions compared by name only: none.

### Receipts

| Receipt | Check | Commit | Date | Job | SHA-256 |
|---|---|---|---|---|---|
| `.lean-receipts/3f364b51d2c7-comparator.json` | statement comparison | `3f364b51d2c7` | 2026-10-18 | — | `a248b4d7ceeb034d0fb0a3700670e7b59ca7574aa84287f0e2d1589ddd2eeb1e` |
| `.lean-receipts/3f364b51d2c7-systemd-user-total-coloring-lean-verify.service-26f87e9fdae2438cb4ab302aa085cb30-h-2db2e0fa6029.json` | build | `3f364b51d2c7` | 2026-10-18 | — | `732ee12803528338b33d21df1482fdc51fd2ed169b579a61b589e5e9e0e0ba84` |
| `.lean-receipts/533f9430cb45-comparator.json` | statement comparison | `533f9430cb45` | 2026-10-08 | — | `c3c1f5d65707f99f56a870714d12541fb7b7c1abd60f3358d4f25bd0bbf907bd` |
| `.lean-receipts/533f9430cb45-home-workstation-2026-10-08-total-coloring.json` | build | `533f9430cb45` | 2026-10-08 | — | `4ea44f7efdc1ba712e79bf2e9d5f6f2f0e41a350f4c5920197f43e91a16dc966` |
| `.lean-receipts/55edc8145228-home-workstation-2026-10-06-total-coloring.json` | build | `55edc8145228` | 2026-10-06 | — | `14d42549e43e9fc24cd17655f207a60a901ed0c4e31ec83c379fe871cbb3b66d` |
| `.lean-receipts/c025d20a1826-comparator.json` (used here) | statement comparison | `c025d20a1826` | 2026-10-18 | — | `120f4a7878339120dbb684b778daa944e2c7241d48d0fee3c99b0fde2f28f09b` |
| `.lean-receipts/c025d20a1826-systemd-user-total-coloring-lean-verify.service-eff861bf68744993b3eaff1c5e6b37fc-h-2db2e0fa6029.json` (used here) | build | `c025d20a1826` | 2026-10-18 | — | `586b45670d5cfb97a03fa573d036b1c7b2f1bb03d0dd09d5d24488fa1df1d4cd` |

*(used here)*: the receipt the lean-pkg registry holds for this package, which the lines above read. SHA-256 is of the file as committed.

### Reproduce

- Lean toolchain: `leanprover/lean4:v4.32.0`.
- Mathlib: `81a5d257c8e410db227a6665ed08f64fea08e997` (lake-manifest.json).

```bash
git clone https://github.com/chenle02/total-coloring-lean
cd total-coloring-lean
git checkout c025d20a182644bbacdd96165c93e1b8b2a403c6   # the commit the build check binds
lake exe cache get
lake build
```

Expected: `#print axioms` on any declaration above reports a subset of {`Classical.choice`, `Quot.sound`, `propext`} (the union the build check records); `sorryAx` never appears.

## Citation

Le Chen and Songling Shan. *Total Coloring Lean*. Version 0.2.0. [doi:10.5281/zenodo.23452513](https://doi.org/10.5281/zenodo.23452513).

See [CITATION.cff](https://github.com/chenle02/total-coloring-lean/blob/HEAD/CITATION.cff).

## License

Released under `Apache-2.0`; see [LICENSE](https://github.com/chenle02/total-coloring-lean/blob/HEAD/LICENSE).

## Acknowledgments

Developed and verified with [lean-pkg](https://github.com/lean-pkg/lean-pkg) ([doi:10.5281/zenodo.23272098](https://doi.org/10.5281/zenodo.23272098)).