Skip to content

Proof architecture

The formal route is layered so each theorem exposes its hypotheses and trust boundary. The terminal result is assembled from ordinary Lean propositions; no external solver result is imported as an axiom.

finite graph G + |V| <= 2 * G.maxDegree
        │
        ├── V empty ───────────────────────────────┐
        │                                           │
        └── V nonempty                              │
              │                                     │
              ▼                                     │
    complement minimum-degree and order bounds      │
              │                                     │
              ▼                                     │
    matching in G-complement with at least k edges  │
              │                                     │
              ▼                                     │
    exact trim to k = |V| - (G.maxDegree + 1)       │
              │                                     │
              ▼                                     │
    PairSingletonWitness with                       │
    J.card = G.maxDegree + 1                        │
              │                                     │
              ▼                                     │
    ordinary auxiliary graph in A_D                 │
              │                                     │
              ▼                                     │
    finite minimal noncolorable extraction          │
              │                                     │
              ▼                                     │
    fans, maximal states, dominators, crossing      │
              │                                     │
              ▼                                     │
    HasValidRainbowColoring D H J                   │
              │                                     │
              ▼                                     │
    conflict-preserving semantic decoder            │
              │                                     │
              └──────────────┬──────────────────────┘
                             ▼
    exists Assignment G (ExtensionPalette
      (G.maxDegree + 1)) with Assignment.Valid

Here D = G.maxDegree + 1 and ExtensionPalette D = Fin (D + 2). The empty branch uses exists_valid_assignment_of_isEmpty; the nonempty branch is the full route shown on the left. No parity hypothesis occurs.

Layer map

Layer Principal modules Role
Semantics Graph, Total, Auxiliary Graph incidence, assignments, validity, and conflict-preserving decoding
Matching engine MatchingLowerBound Maximum-matching argument giving at least k edges from minimum-degree and order bounds
High-degree specialization HighDegreeComplementMatching Converts the density hypothesis into the complement matching lower bound
Exact extraction MatchingExact Trims a matching subgraph to a prescribed exact edge count
Complement adapter ComplementMatchingWitness Converts a complement matching into a pair/singleton witness and proves its counts
Supplied-witness constructor PairSingletonExtension Auxiliary graph, extension, selector coverage, matching-plus-full-star structure, and degree/count identities
Supplied-partition adapter EquitablePairSingleton Retained alternate API from an explicit equitable independent partition
Structural class AuxiliaryClass, Distinguished Definition of A_D, deletion closure, and stable distinguished-edge transport
Certificates Certificate Executable checkers connected to semantic propositions by soundness theorems
Conditional selector decoding IndependentSeed, TotalIndependentSelector, PartialEdgeSelector Reverse greedy extension from supplied seed/core peel data; fresh-color vertex/edge selector, explicit alternating-path donor wrappers, properness outside the selected matching, and exact reverse normalization; all are on current main
Adapted-spare endpoint AdaptedSpareEndpoint On current main, exactly characterizes vertex properness of a supplied spare/head/missing endpoint assignment; constructs no donor matching or coloring
Critical extraction CriticalState, MinimalExtraction, DeletionBridge Minimal hypothetical counterexample and one-hole state
Recoloring geometry RainbowSwap, Kempe, PartialKempe, TwoColorGeometry Exact swap safety and physical two-color components
Fan mechanics Fan*, Dependency*, CriticalFan* Legal shifts, reachability, missing colors, and capacity
Global pivots CriticalGlobalMaximal, CriticalFrozenMobility, CriticalRootPivot Maximal reachable state and elimination of frozen triples
Auxiliary closure CriticalDirectEntry, CriticalDominator*, CriticalCrossing*, CriticalAllDClosure External-source cases and the all-orders contradiction
Terminal composition EmptyAssignment, AuxiliaryTransfer, HighDegreeTotalColoring Empty base case, nonempty decoding, and the final package theorem

At current main commit da0595da…, tree 34824cd5…, the umbrella TotalColoring.lean imports every merged production module, including the matching, empty, high-degree terminal, independent-seed, selector/path, and partial-edge normalization layers. It also imports AdaptedSpareEndpoint, merged by PR #13 from agent/donor-global-formalization. Attribute the declaration to main, and support any verification claim with a tree-specific external receipt.

Two routes into the reusable auxiliary engine

The terminal high-degree theorem constructs its input through a matching in the complement. The supplied-partition route remains available independently:

supplied EquitableIndependentPartition G D
        │  D <= |V| < 2D
        ▼
PairSingletonWitness + J.card = D
        │  G.maxDegree + 1 <= D
        │  |V| + 2 <= 2D
        ▼
InAuxiliaryClass D H J

Likewise, a downstream development may start from a supplied PairSingletonWitness, or directly from a compatible Auxiliary.Extension and InAuxiliaryClass. These are stable interfaces, not unresolved premises of TotalColoring.exists_valid_assignment_of_highDegree.

The conditional Delta + 2 modules form a separate route. The independent-seed endpoint starts from a supplied proper old-palette edge coloring, independent seed, and peel certificate. The later TotalIndependentSelector module permits both an independent fresh-color vertex set and an avoiding matching of fresh-color edges, together with a supplied actual-list core coloring and core-relative peel certificate. Its alternating rainbow-path wrapper proves the donor exchange only after the full indexed path certificate is supplied. These modules do not feed the terminal high-degree theorem and do not discharge Vizing, selector/core, peel, or path existence.

The stacked PartialEdgeSelector module isolates the exact data actually read by the semantic decoder. The old edge assignment is proper only outside the selected matching; its values on that matching are overwritten. The module also gives a reverse normalization for a supplied valid total coloring: choose one palette color, take its vertex and edge color classes, and pull the remaining colors back through Fin.succAbove. This reverse path ends in literal equality with the supplied assignment and introduces no coloring existence theorem. The independent-seed, selector/path, and partial-edge layers were merged by PRs #10--#12; their earlier branch commits and trees remain historical proof provenance.

The AdaptedSpareEndpoint module isolates the final vertex-side logic of a different route. Given disjoint supplied sets A and B, supplied missing colors, and supplied head labels, it assigns the spare none to A, the head labels to B, and missing colors elsewhere. Properness is equivalent to independence of A, coverage of every equal-missing conflict by A ∪ B, clean head labels against unchanged neighbors, and proper head labels on adjacent vertices of B. This equivalence does not construct the sets, a physical donor matching, seed or matching data, missing/head data, a proper edge coloring, or a total coloring, so it is not a route completion or an unrestricted Delta + 2 theorem.

The matching route in detail

For a nonempty finite graph, put

k = |V| - (G.maxDegree + 1).

The complement-degree formula proves every complement degree is at least k, while |V| <= 2 * G.maxDegree proves 2 * k <= |V|. The general maximum-matching lemma supplies at least k complement edges. MatchingExact deletes excess matching edges, preserving the matching predicate, to obtain exactly k.

The exact size is what closes the numerical reduction. Paired vertices contribute the matching edges; all uncovered vertices become singletons. The checked support and edge-count identities then give exactly G.maxDegree + 1 classes. PairSingletonExtension converts those classes to the ordinary auxiliary graph and proves all fields of InAuxiliaryClass (G.maxDegree + 1) required by the all-orders theorem.

Terminal boundary

The terminal declaration is:

TotalColoring.exists_valid_assignment_of_highDegree

It closes the former complement-matching, exact-count, partition-construction, and empty-graph seams inside the Lean package. The exact proof-development tree 4624044788ab42c0dc116cfbf7f38c696065263c passed five separate high-memory full/Quickstart/leanchecker replays (jobs 5388311 through 5388315).

That receipt applies to the named proof tree. It must not be silently promoted to a later integration or publication tree. Accordingly, the later publishable tree 89a32c7a78e294a8b1484092ec79afaa3b4ace5a received a separate Wave 11 exact-tree gate and public CI before PR #8 merged it into main as 0e938606. The package theorem still does not lock a manuscript theorem, establish novelty, prove an unconditional stronger palette, or settle the Total Coloring Conjecture.