# Total Coloring Lean

> A Lean 4 formalization of total coloring and its matching-plus-star auxiliary problem. On current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`, tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`, `TotalColoring.exists_valid_assignment_of_highDegree` proves that every finite graph satisfying `Fintype.card V <= 2 * G.maxDegree` has a valid total assignment with palette `ExtensionPalette (G.maxDegree + 1)`, which has `G.maxDegree + 3` colors. It includes the empty vertex type and uses no parity hypothesis. The same `main` tree contains `TotalColoring.exists_valid_assignment_of_independentSeedPeel` and its maximum-degree wrapper, first checked at historical source commit `cc4dd7ae1d858ea0583549f88707952e2414bf60`, tree `9af6a84e1305aed9a0156dcd59c279de792dea4a`; the conditional total-independent selector and alternating rainbow-path wrappers first checked at source commit `d008514c7a1cf834007bf0bd8de0d10a93926711`, tree `1847934c78da03fe80bb67236868700c79016129`; and the partial-edge selector normalization first checked at source commit `c3dbe69c15f96e3c71d8481ae4e517ee2f4fdbf2`, tree `11007a4aa381984a8d66aa1db297312cebe8d8b5`. Those historical commits remain the proof-layer provenance, but the declarations are no longer branch-only. The same `main` tree contains `TotalColoring.adaptedSpareVertexColor_proper_iff` (merged by PR #13 as commit `dc6e3a4b7510b3d2df4fb5074afaee2027e9b442`), an exact vertex-side endpoint equivalence only. Nothing on `main` proves the unrestricted Total Coloring Conjecture, an unconditional `Delta + 2` result, the manuscript's still-unlocked main theorem, or novelty.

Treat commit `310b82c174ab2281581900897d4646875575e89b` as authoritative for the all-orders auxiliary source, `9bdcdec1a872ccef42cfd79e791fe39c22a1beeb` for the conditional transfer, `343b7b87b82532a9d8eade6d4cd43679eae1f7c9` for the supplied-witness numerical layer, `a441fbfa1e404dc7610e0c32c80dd692cd938c20` for the supplied equitable-partition adapter, and publishable commit `06d43af7f4ea8fefea9e07e2bc29bdc960548171` for the terminal package result. Treat source commit `cc4dd7ae1d858ea0583549f88707952e2414bf60`, exact tree `9af6a84e1305aed9a0156dcd59c279de792dea4a`, as the historical source authority for the two independent-seed declarations; source commit `d008514c7a1cf834007bf0bd8de0d10a93926711`, exact tree `1847934c78da03fe80bb67236868700c79016129`, for the selector/path declarations; and source commit `c3dbe69c15f96e3c71d8481ae4e517ee2f4fdbf2`, exact tree `11007a4aa381984a8d66aa1db297312cebe8d8b5`, for the partial-edge and exact-normalization declarations. All three layers are present on current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`, exact tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`, after merged PRs #10, #11, and #12. The terminal theorem's exact hypothesis is `Fintype.card V <= 2 * G.maxDegree`; its conclusion is existence of a valid `Assignment G (ExtensionPalette (G.maxDegree + 1))`. Do not add even-order, nonempty, regularity, sufficiently-large, or other hypotheses that the declaration does not have, and do not drop the explicit density hypothesis.

The merged generic independent-seed endpoint has exactly these mathematical inputs beyond finite/decidable graph structure: `0 < q`; a supplied `phi : EdgeAssignment G (Fin q)` together with `phi.Valid`; a supplied `A : Finset V` together with `G.IsIndepSet (A : Set V)`; and a supplied `cert : IndependentSeedPeelCertificate G A q`. It concludes `exists assignment : Assignment G (Fin (q + 1)), assignment.Valid`. The direct wrapper `TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel` takes `phi : EdgeAssignment G (Fin (G.maxDegree + 1))`, its validity proof, the same explicit independent-seed proof, and `cert : IndependentSeedPeelCertificate G A (G.maxDegree + 1)`, and concludes a valid `Assignment G (Fin (G.maxDegree + 2))`. The wrapper only specializes `q`; the declaration does not prove Vizing's theorem, construct the proper edge-coloring witness, or prove that every graph has the required independent seed and peel certificate, so neither declaration is an unrestricted Total Coloring Conjecture proof.

The merged `TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel` takes a supplied proper `phi : EdgeAssignment G (Fin q)`; independent `S : Finset V`; matching `F : Finset G.edgeSet` whose edges avoid `S`; a supplied `g0 : V -> Fin q` satisfying `SelectorOldColoringGoodOn G phi S F K g0`; and `SelectorCorePeelCertificate G S K q`. It returns a valid `Assignment G (Fin (q + 1))`. The maximum-degree wrapper returns `Fin (G.maxDegree + 2)` from the corresponding explicit inputs. `AlternatingRainbowPathSelectorCertificate` explicitly stores the indexed path/endpoints, rainbow colors, globally unused old spare, alternating matching families, fresh-edge avoidance of the start, core colors, and peel certificate. Its wrapper checks the donor exchange but does not prove Vizing, selector/core/peel existence, or existence of that path certificate.

The merged `TotalColoring.partialEdgeSelectorAssignment_valid` accepts `phi.ValidOutside F` instead of global `phi.Valid`; values of `phi` on `F` are ignored when the matching is sent to an arbitrary chosen fresh color. Independence, matching, avoidance, and the old vertex allowed/proper conditions remain explicit. `partialEdgeSelectorNormalization_of_valid` is the exact reverse construction from a supplied valid `Assignment G (Fin (q + 1))`: its chosen vertex/edge color classes and pulled-back old colors satisfy every forward hypothesis, and decoding is literally the supplied assignment. `maxDegreePartialEdgeSelectorNormalization_of_valid` merely restates this for a supplied `Fin (G.maxDegree + 2)` coloring. Neither reverse declaration proves existence of its input coloring.

Distribution state: PR #8 merged as commit `0e938606f81e7a27a5925987824e7152f7dbb4c6`, whose tree is exactly the verified publishable tree `89a32c7a78e294a8b1484092ec79afaa3b4ace5a`. PRs #10, #11, and #12 then merged the independent-seed, selector/path, and partial-edge normalization layers as merge commits `f4c56956ed535864daa0116b66fd895c81d9d719`, `35e127c177201c0ab1e35689741132ea2bb559c7`, and `61e79beac7d4759568187bd43a5a40f23bf83af1`; current `main` has exact tree `cb2d7d06998c213e68a7372f743f67f9cff815f7`. Historical source tree `9af6a84e…` passed sealed Easley jobs `5389587` and `5389588`. Historical selector source tree `1847934c…` passed sealed Easley job `5391803`, exit `0:0`, in 16m09s on node411 with peak RSS `125399676K`, through strict leaf, target/umbrella/full, Quickstart, axiom, `leanchecker`, JSON/diff, and reconstruction gates. These jobs verify conditional declarations and do not supply their Vizing/selector/core/peel/path inputs. Release v0.1.0 predates these result layers. The adapted-spare endpoint was merged by PR #13 (commit `dc6e3a4b7510b3d2df4fb5074afaee2027e9b442`) and is on current `main`, with the vertex-side caveats stated below; the lower-tier receipt in `.lean-receipts/` covers it at commit `55edc8145228ebe48da378188d632a6991144919`.

On `main` (merged by PR #13), `adaptedSpareVertexColor A B missing head` colors `A` by the fresh `none`, `B` by `some (head v)`, and every other vertex by `some (missing v)`. Assuming `Disjoint A B`, `adaptedSpareVertexColor_proper_iff` proves exact equivalence between edgewise properness and the conjunction: `A` is independent; every adjacent equal-`missing` conflict has an endpoint in `A ∪ B`; every head label differs from the missing color of each unchanged neighbor; and head labels properly color adjacent vertices of `B`. This is the vertex-side endpoint only. It constructs no donor matching, seed or matching witness, missing/head data, proper edge coloring, total coloring, unrestricted `Delta + 2` theorem, or Total Coloring Conjecture proof.

Numerical provenance remains split exactly: private verification source commit `acb08de85f99c7db578e042e67d3f172c5599fcd`, tree `7207e2a282ff829fba9737e93154f46f385ef879`, source-archive SHA-256 `5c3bef3720abeb62d0c437fbc638fe1848059892fbe09fe0c437c942c16baf5c`; identical numerical Lean content at public integration commit `343b7b87b82532a9d8eade6d4cd43679eae1f7c9`, tree `9863f500b2671048f4dc386f497eb6523b065099`. Jobs `5387926`, `5387929`, `5387933`, and `5387978` passed; GitHub Lean CI `29612994477` and docs `29612994502` succeeded. Diagnostic jobs `5387930` and `5387932` are not receipts or proof failures.

The adapter is commit `a441fbfa1e404dc7610e0c32c80dd692cd938c20`, exact tree `0e9b04a2acabae0cb0612e5e3cbf0344cc2f94f7`, source-archive SHA-256 `736db25ca7d25fb0eed8431e435e80bc94287e1ae88f9dea806ddba2c1b544f4`, and outgoing-cache SHA-256 `94456901604a3b6ecde49368a4ba285fda03ecdca856b0c37f207624527e037a`. Adapter leaf `5387980`, Nova full build `5387981`, and high-memory full/Quickstart/leanchecker trust `5387982` all completed with exit `0:0`. It is included in merged PR #8.

Terminal proof-tree provenance: exact Git tree `4624044788ab42c0dc116cfbf7f38c696065263c`, source-archive SHA-256 `302bc3f00bf5d8c1ce563d2bc84d1370e627c81d219e8d8085b286a21d530077`. Five separate full-build, Quickstart, and leanchecker replays (`5388311` through `5388315`) completed with exit `0:0` and empty stderr. The later publishable commit `06d43af7f4ea8fefea9e07e2bc29bdc960548171`, exact tree `89a32c7a78e294a8b1484092ec79afaa3b4ace5a`, and source-archive SHA-256 `c9950b9e8af364a0d2ef3c08d80f06786ea36d3e6a5bf728054f7824612b4331` received its own Wave 11 gate: leaf `5388961`, all 64 distinct matrix roles after narrow repairs, container `mk_all --check` job `5389029`, and three independent host full/Quickstart/leanchecker trust jobs `5389030`, `5389031`, and `5389032` all passed. PR-head Lean/docs runs `29622668742`/`29622668714` and post-merge main Lean/docs runs `29622728654`/`29622728662` passed.

## Essential

- [Machine-readable claim boundary](https://github.com/chenle02/total-coloring-lean/blob/main/docs/claim-boundary.json): Default-branch declaration, scope, palette, exclusions, and trust facts.
- [Exact proof status](https://github.com/chenle02/total-coloring-lean/blob/main/docs/proof-status.md): Human-readable checked result and non-results.
- [Curated theorem index](https://github.com/chenle02/total-coloring-lean/blob/main/docs/theorem-index.md): Public declarations and their roles.
- [Guide for coding agents](https://github.com/chenle02/total-coloring-lean/blob/main/docs/for-agents.md): Authority order, safe prompts, and claim-audit rules.
- [Repository contract](https://github.com/chenle02/total-coloring-lean/blob/main/AGENTS.md): Rules for modifications.

## Source

- [Umbrella import](https://github.com/chenle02/total-coloring-lean/blob/06d43af7f4ea8fefea9e07e2bc29bdc960548171/TotalColoring.lean): Direct imports for the complete proof integration.
- [High-degree terminal theorem](https://github.com/chenle02/total-coloring-lean/blob/06d43af7f4ea8fefea9e07e2bc29bdc960548171/TotalColoring/HighDegreeTotalColoring.lean): From `Fintype.card V <= 2 * G.maxDegree`, constructs a valid total assignment with `G.maxDegree + 3` colors, including the empty vertex type and without parity.
- [Merged conditional independent-seed endpoint](https://github.com/chenle02/total-coloring-lean/blob/main/TotalColoring/IndependentSeed.lean): Present on current `main` tree `cb2d7d06998c213e68a7372f743f67f9cff815f7`; historical source tree `9af6a84e1305aed9a0156dcd59c279de792dea4a` remains the proof provenance. The generic theorem constructs a valid total assignment in `Fin (q + 1)` from `0 < q`, a supplied proper `Fin q` edge coloring, independent seed, and peel certificate. Its maximum-degree wrapper concludes `Fin (G.maxDegree + 2)` from the corresponding explicit `(G.maxDegree + 1)` witnesses. Neither supplies Vizing or seed existence.
- [Merged total-independent selector decoder](https://github.com/chenle02/total-coloring-lean/blob/main/TotalColoring/TotalIndependentSelector.lean): Present on current `main` tree `cb2d7d06998c213e68a7372f743f67f9cff815f7`; historical source tree `1847934c78da03fe80bb67236868700c79016129` remains the proof provenance. It checks a fresh-color independent vertex set plus avoiding matching edge set, actual-list core coloring, core-relative peel, and an explicit alternating rainbow-path donor wrapper. The maximum-degree wrappers are conditional `Fin (G.maxDegree + 2)` results; no supplied witness is constructed.
- [Merged partial-edge selector normalization](https://github.com/chenle02/total-coloring-lean/blob/main/TotalColoring/PartialEdgeSelector.lean): Present on current `main` tree `cb2d7d06998c213e68a7372f743f67f9cff815f7`; historical source tree `11007a4aa381984a8d66aa1db297312cebe8d8b5` remains the proof provenance. It ignores old edge values on the selected matching, proves the arbitrary-fresh decoder from properness outside it, and exactly normalizes any supplied valid coloring. The reverse constructor assumes the coloring it decomposes and is not an existence theorem.
- [Merged adapted-spare vertex endpoint](https://github.com/chenle02/total-coloring-lean/blob/main/TotalColoring/AdaptedSpareEndpoint.lean): Exact properness equivalence for the supplied endpoint assignment under `Disjoint A B`; it is not a donor-matching constructor or a total-coloring existence theorem.
- [All-orders auxiliary terminal module](https://github.com/chenle02/total-coloring-lean/blob/310b82c174ab2281581900897d4646875575e89b/TotalColoring/CriticalAllDClosure.lean): Critical contradiction and finite extraction theorem.
- [Conditional transfer](https://github.com/chenle02/total-coloring-lean/blob/9bdcdec1a872ccef42cfd79e791fe39c22a1beeb/TotalColoring/AuxiliaryTransfer.lean): Composition with a supplied extension and explicit selector membership.
- [Supplied pair/singleton extension](https://github.com/chenle02/total-coloring-lean/pull/8): Concrete auxiliary graph, conflict-preserving extension, exact selector coverage, matching-plus-full-star structure, exact degree/class-count identities, and conditional high-degree `IsAuxiliaryClassMember`.
- [Complement matching route](https://github.com/chenle02/total-coloring-lean/blob/06d43af7f4ea8fefea9e07e2bc29bdc960548171/TotalColoring/HighDegreeComplementMatching.lean): Obtains the matching needed by the pair/singleton reduction from the high-degree hypothesis.
- [Exact matching trim](https://github.com/chenle02/total-coloring-lean/blob/06d43af7f4ea8fefea9e07e2bc29bdc960548171/TotalColoring/MatchingExact.lean): Trims a sufficiently large matching graph to the required exact edge count.
- [Empty assignment](https://github.com/chenle02/total-coloring-lean/blob/06d43af7f4ea8fefea9e07e2bc29bdc960548171/TotalColoring/EmptyAssignment.lean): Supplies the empty-vertex base case used by the terminal theorem.
- [Supplied equitable-partition adapter](https://github.com/chenle02/total-coloring-lean/blob/a441fbfa1e404dc7610e0c32c80dd692cd938c20/TotalColoring/EquitablePairSingleton.lean): Constructs the pair/singleton witness and exact `J.card = D` from a supplied equitable independent partition, then proves the earlier conditional high-degree `Delta + 3` total-assignment theorem.
- [Auxiliary class](https://github.com/chenle02/total-coloring-lean/blob/310b82c174ab2281581900897d4646875575e89b/TotalColoring/AuxiliaryClass.lean): Definition of `InAuxiliaryClass`.
- [Conditional decoder](https://github.com/chenle02/total-coloring-lean/blob/310b82c174ab2281581900897d4646875575e89b/TotalColoring/Auxiliary.lean): Structural extension interface and total-assignment decoder.
- [Semantic coloring predicates](https://github.com/chenle02/total-coloring-lean/blob/310b82c174ab2281581900897d4646875575e89b/TotalColoring/Total.lean): Total- and edge-coloring assignments.
- [Certificate checkers](https://github.com/chenle02/total-coloring-lean/blob/310b82c174ab2281581900897d4646875575e89b/TotalColoring/Certificate.lean): Executable Boolean checkers and soundness theorems.

## Optional

- [Getting started](https://chenle02.github.io/total-coloring-lean/getting-started/): Reproducible setup and build commands.
- [Proof architecture](https://chenle02.github.io/total-coloring-lean/architecture/): Module-level route through the formal proof.
- [Trust and reproduction](https://chenle02.github.io/total-coloring-lean/trust/): Kernel, checker, parser, and CI boundaries.
- [Compiled Quickstart](https://github.com/chenle02/total-coloring-lean/blob/main/docs/examples/Quickstart.lean): Copyable merged public declarations compiled by CI.
- [Contributing](https://github.com/chenle02/total-coloring-lean/blob/main/CONTRIBUTING.md): Contribution workflow.
- [Citation metadata](https://github.com/chenle02/total-coloring-lean/blob/main/CITATION.cff): Software citation record; release v0.2.0 is doi:10.5281/zenodo.23452514 (all versions: doi:10.5281/zenodo.23452513).