Kernel-checked combinatorics

Total Coloring Lean

Lean 4 foundations for total coloring, constrained auxiliary edge coloring, and proof-producing certificate checks.

Get started Exact proof boundary Browse source Sponsor

What is proved

For every finite graph G satisfying Fintype.card V <= 2 * G.maxDegree, Lean proves the existence of a valid total assignment with palette ExtensionPalette (G.maxDegree + 1).

The terminal declaration is TotalColoring.exists_valid_assignment_of_highDegree. It includes the empty vertex type and uses no parity hypothesis.

For a nonempty graph, the checked proof obtains a sufficiently large matching in the complement, trims it to the exact required size, converts it to a PairSingletonWitness, proves membership in the auxiliary class, applies the all-orders rainbow theorem, and decodes the result. The empty graph is discharged separately by a vacuous valid assignment.

The lower-level supplied-input interfaces remain public: users may start from an Auxiliary.Extension, a PairSingletonWitness, or an EquitableIndependentPartition. The abstract theorem for every finite InAuxiliaryClass D H J also remains available.

On current main commit da0595da..., tree 34824cd5..., the separate theorem exists_valid_assignment_of_independentSeedPeel constructs a Fin (q + 1) total assignment from a supplied proper Fin q edge coloring, independent seed, and peel certificate. Its direct maximum-degree wrapper has palette Fin (G.maxDegree + 2), while retaining all of those witnesses as explicit hypotheses. Its historical proof source is branch agent/independent-seed-endpoint; two sealed Easley trust replays passed at exact source tree 9af6a84e....

The later selector layer, also merged into current main, checks a broader supplied-witness decoder: an independent fresh-color vertex set may be combined with a matching of fresh-color edges avoiding it, an actual-list-colored core, and a core-relative peel certificate. An explicit alternating rainbow-path certificate wrapper checks the donor exchange. The maximum-degree wrappers have palette Fin (G.maxDegree + 2), but all edge-coloring, selector/core, path, and peel witnesses remain hypotheses. Exact source tree 1847934c... on historical branch agent/total-independent-selector-decoder passed sealed Easley job 5391803.

The partial-edge layer, merged by PR #12, weakens the old edge premise further: colors stored on the selected matching are ignored, and properness is required only outside it. It also gives an exact reverse decomposition of any supplied valid total coloring after choosing one fresh color class. The decoded assignment is literally the supplied assignment. This converse starts from the coloring and does not establish its existence.

PR #13 merged into main the exact vertex-side equivalence adaptedSpareVertexColor_proper_iff. Under Disjoint A B, the supplied endpoint assignment is proper exactly when A is independent, equal-missing conflicts meet A ∪ B, head labels are clean against unchanged neighbors, and head labels are proper on adjacent vertices of B. It constructs no donor matching, edge coloring, or total coloring. Any verification claim requires a tree-specific external receipt.

Read the exact theorem →

What is not proved

This package does not prove the Total Coloring Conjecture or an unconditional Delta + 2 theorem, and it does not establish a paper theorem or novelty claim. The conditional endpoint does not prove Vizing's theorem or existence of its seed/certificate inputs. The newer selector layer likewise does not prove existence of its selector, canonical core, peel order, or alternating rainbow path. Those statements are not supplied by the later normalization either, because that construction assumes a valid total coloring as input. Those statements are also not supplied by the adapted-spare vertex endpoint, which assumes all endpoint data and proves only vertex properness. Those manuscript claims remain under their own author and literature-review gates. Attribute verification only to the exact trees and jobs named in the proof-status page. The adapted-spare declaration is on main since PR #13; any verification claim must cite a tree-specific external receipt.

Inspect the machine-readable boundary →

Start with the theorem

import TotalColoring

#check TotalColoring.MinimalExtraction
  .hasValidRainbowColoring_of_inAuxiliaryClass
#check TotalColoring.exists_valid_assignment_of_highDegree
#check TotalColoring.Auxiliary
  .exists_valid_assignment_of_highDegree_nonempty
#check TotalColoring.MatchingLowerBound
  .exists_complement_matchingGraph_edgeFinset_card_eq
#check TotalColoring.Auxiliary.Extension
  .exists_valid_decode_of_inAuxiliaryClass
#check TotalColoring.Auxiliary.PairSingletonWitness.extension
#check TotalColoring.Auxiliary.PairSingletonWitness
  .classEdge_mem_distinguishedEdgeSet
#check TotalColoring.Auxiliary.PairSingletonWitness
  .isAuxiliaryClassMember_of_highDegree
#check TotalColoring.Auxiliary.EquitableIndependentPartition
  .exists_valid_assignment_of_highDegreePartition
#check TotalColoring.exists_valid_assignment_of_independentSeedPeel
#check TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel
#check TotalColoring.SelectorCorePeelCertificate
#check TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel
#check TotalColoring.exists_valid_assignment_of_maxDegreeTotalIndependentSelectorPeel
#check TotalColoring.AlternatingRainbowPathSelectorCertificate
#check TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector
#check TotalColoring.exists_valid_assignment_of_maxDegreeAlternatingRainbowPathSelector
#check TotalColoring.EdgeAssignment.ValidOutside
#check TotalColoring.partialEdgeSelectorAssignment_valid
#check TotalColoring.PartialEdgeSelectorNormalization
#check TotalColoring.partialEdgeSelectorNormalization_of_valid
#check TotalColoring.maxDegreePartialEdgeSelectorNormalization_of_valid

The independent-seed, selector/path, and partial-edge/normalization declarations shown above are all on current main commit da0595da…, tree 34824cd5…; their earlier proof branches and source trees remain historical provenance. The adapted-spare endpoint, on main since PR #13, is not included in this snippet. The forward coloring declarations are propositional existence theorems, while the normalization declarations start from a supplied valid assignment. They do not compute a coloring from external data. For executable finite certificates, begin with TotalColoring.Certificate and its soundness theorems.

Choose your route

Use the library

Install the pinned Lean toolchain, fetch the mathlib cache, build, and import the umbrella module.

Installation and first checks

Audit the proof

Follow the formal route from complement matching and exact extraction to the auxiliary class, then through minimal extraction, maximal one-hole states, crossing, the final contradiction, and semantic decoding.

Proof architecture

Build with an agent

Give a coding agent the exact authority order, public entrypoints, forbidden inferences, and reproducibility gates.

Agent guide · /llms.txt

Reproducibility before spectacle

The repository separates semantic propositions, executable checks, and external data. Production proofs contain no sorry, admit, custom axiom, or native_decide. CI builds the umbrella import and replays declarations with leanchecker.

Understand the trust boundary →