Curated theorem index¶
This is a small map of public entrypoints, not an exhaustive inventory of internal lemmas.
Package terminal theorem¶
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.exists_valid_assignment_of_highDegree |
HighDegreeTotalColoring |
Every finite G with Fintype.card V <= 2 * G.maxDegree has a valid assignment in ExtensionPalette (G.maxDegree + 1); empty and nonempty vertex types are included |
TotalColoring.Auxiliary.exists_valid_assignment_of_highDegree_nonempty |
HighDegreeTotalColoring |
Nonempty specialization using the complement-matching witness and auxiliary decoder |
TotalColoring.exists_valid_assignment_of_isEmpty |
EmptyAssignment |
Every graph on an empty vertex type has a valid assignment for any color type |
ExtensionPalette (G.maxDegree + 1) is definitionally
Fin (G.maxDegree + 3). No parity hypothesis appears in the terminal theorem.
The exact proof-development tree
4624044788ab42c0dc116cfbf7f38c696065263c passed five separate high-memory
full/Quickstart/leanchecker jobs, 5388311 through 5388315. The later
publishable commit 06d43af7, exact tree
89a32c7a78e294a8b1484092ec79afaa3b4ace5a, received its own Wave 11 gate:
leaf 5388961, all 64 distinct matrix roles after narrow repairs, container
mk_all --check job 5389029, and independent host trust jobs
5389030--5389032. PR #8 merged that exact tree into main as 0e938606;
PR-head and post-merge Lean/docs CI passed.
Conditional independent-seed endpoint on main¶
The following declarations are present on current main commit da0595da…,
tree 34824cd5…. Their historical proof source is branch
agent/independent-seed-endpoint at exact source commit
cc4dd7ae1d858ea0583549f88707952e2414bf60, tree
9af6a84e1305aed9a0156dcd59c279de792dea4a; PR #10 merged them.
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.exists_valid_assignment_of_independentSeedPeel |
IndependentSeed |
From 0 < q, a supplied proper phi : EdgeAssignment G (Fin q), a supplied independent seed A, and a supplied IndependentSeedPeelCertificate G A q, produces assignment : Assignment G (Fin (q + 1)) with assignment.Valid |
TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel |
IndependentSeed |
Direct specialization from a supplied proper EdgeAssignment G (Fin (G.maxDegree + 1)), independent seed, and certificate at G.maxDegree + 1 to a valid Assignment G (Fin (G.maxDegree + 2)) |
The peel certificate supplies a duplicate-free order covering exactly the
vertices outside A and the strict bound
at every deletion step. Setting q = G.maxDegree + 1 makes the conclusion a
conditional Fin (G.maxDegree + 2) palette. The declaration does not prove
Vizing's theorem or construct the proper edge assignment, and it does not
prove existence of the independent seed or peel certificate. It is therefore
not an unrestricted Total Coloring Conjecture theorem and does not change the
G.maxDegree + 3 palette of the package terminal theorem above.
The maximum-degree wrapper only performs this substitution; all witnesses
remain explicit inputs.
Exact source tree 9af6a84e… passed two sealed offline Easley trust replays:
job 5389587 on node408 completed in 11m40s with peak RSS 121378968K, and
job 5389588 on node412 completed in 11m39s with peak RSS 122474236K.
Both exited 0:0 after strict leaf, umbrella/full, Quickstart, axiom,
leanchecker, metadata, and exact-tree gates. The receipts validate the
conditional declarations, not existence of their supplied witnesses.
Total-independent selector decoder on main¶
The following declarations are present on current main commit da0595da…,
tree 34824cd5…. Their historical proof source is branch
agent/total-independent-selector-decoder at source commit
d008514c7a1cf834007bf0bd8de0d10a93926711, exact tree
1847934c78da03fe80bb67236868700c79016129; PR #11 merged them.
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.totalIndependentSelectorAssignment_valid |
TotalIndependentSelector |
Semantic decoder: a fresh-color independent vertex set and a fresh-color matching of edges avoiding that set combine with a proper allowed old coloring on all remaining vertices to give a valid total assignment in Fin (q + 1) |
TotalColoring.SelectorCorePeelCertificate |
TotalIndependentSelector |
Packages S ⊆ K, a duplicate-free order covering exactly the complement of K, and the exact core-relative peel inequalities |
TotalColoring.exists_valid_assignment_of_totalIndependentSelectorPeel |
TotalIndependentSelector |
Extends a supplied actual-list coloring on K \ S along the supplied core-relative peel order and invokes the semantic decoder |
TotalColoring.exists_valid_assignment_of_maxDegreeTotalIndependentSelectorPeel |
TotalIndependentSelector |
Specializes the conditional decoder to a proper Fin (G.maxDegree + 1) edge assignment and returns a valid Fin (G.maxDegree + 2) total assignment |
TotalColoring.AlternatingRainbowPathSelectorCertificate |
TotalIndependentSelector |
Explicit indexed path, rainbow, spare, alternating matching, start-avoidance, core-color, and peel evidence; it does not assert certificate existence |
TotalColoring.exists_valid_assignment_of_alternatingRainbowPathSelector |
TotalIndependentSelector |
Checks the donor exchange from the supplied alternating rainbow-path certificate and returns a valid assignment in Fin (q + 1) |
TotalColoring.exists_valid_assignment_of_maxDegreeAlternatingRainbowPathSelector |
TotalIndependentSelector |
Maximum-degree specialization of the explicit path-certificate wrapper |
The generic peel inequality at a step v :: tail is exactly
No declaration in this section constructs the proper old-palette edge
coloring, the selector matching, the core coloring, the peel certificate, or
the alternating rainbow path. The maximum-degree wrappers are therefore
conditional G.maxDegree + 2 implications, not an unrestricted Total
Coloring Conjecture theorem.
Exact source tree 1847934c… passed sealed Easley job 5391803 on node411:
exit 0:0, elapsed 16m09s, peak RSS 125399676K, with exact-tree, strict
leaf, target/umbrella/full, Quickstart, axiom, leanchecker, JSON/diff, and
cache-archive gates.
Partial-edge selector normalization on main¶
The following declarations are present on current main commit da0595da…,
tree 34824cd5…. Their historical proof source is stacked branch
agent/partial-edge-selector-normalization at source commit
c3dbe69c15f96e3c71d8481ae4e517ee2f4fdbf2, exact source tree
11007a4aa381984a8d66aa1db297312cebe8d8b5; PR #12 merged them.
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.EdgeAssignment.ValidOutside |
PartialEdgeSelector |
Properness is required only between adjacent edges outside the selected finset; values on selected edges are unrestricted |
TotalColoring.partialEdgeSelectorEdgeAssignment_valid |
PartialEdgeSelector |
Sending a matching to an arbitrarily chosen fresh color preserves edge-color validity when the old assignment is proper outside that matching |
TotalColoring.partialEdgeSelectorAssignment_valid |
PartialEdgeSelector |
Adds an independent fresh vertex class and an avoiding fresh edge matching; old vertex colors only avoid incident edges outside the matching |
TotalColoring.totalIndependentSelectorAssignment_valid_of_validOutside |
PartialEdgeSelector |
Strengthens the earlier last-color decoder by replacing global old-edge validity with validity outside the selected matching |
TotalColoring.PartialEdgeSelectorNormalization |
PartialEdgeSelector |
Packages the selector sets, pulled-back old colors, all forward hypotheses, and literal equality of the decoded assignment with a supplied assignment |
TotalColoring.partialEdgeSelectorNormalization_of_valid |
PartialEdgeSelector |
For a supplied valid Fin (q + 1) total assignment, any chosen fresh color and fallback old color produce the exact normalization package |
TotalColoring.maxDegreePartialEdgeSelectorNormalization_of_valid |
PartialEdgeSelector |
Rephrases the reverse construction for a supplied Fin (G.maxDegree + 2) total coloring; the coloring is still an explicit input |
The forward theorem does not construct any selector or coloring. The reverse constructor starts from a supplied valid total coloring, so it cannot be used as an existence proof for that coloring or for the Total Coloring Conjecture.
Adapted-spare vertex endpoint on main¶
The following declaration is present on current main commit da0595da…,
tree 34824cd5…. Its historical proof source is branch
agent/donor-global-formalization at commit a7ed2453…; PR #13 merged it
on 2026-07-20. Any verification claim must cite a tree-specific external
receipt.
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.adaptedSpareVertexColor_proper_iff |
AdaptedSpareEndpoint |
Assuming Disjoint A B, the supplied endpoint coloring (none on A, some (head v) on B, some (missing v) elsewhere) is proper on K exactly when A is independent, every equal-missing conflict is covered by A ∪ B, head labels are clean against unchanged neighbors, and head labels are proper on adjacent vertices of B |
This is an exact vertex-side equivalence. It does not construct A, B, a
physical donor matching, donor-label transport, seed or matching witnesses,
missing/head data, a proper edge coloring, or a total coloring. It gives no
unrestricted Delta + 2 theorem and does not prove the Total Coloring
Conjecture.
Matching construction¶
| Declaration | Module | Purpose |
|---|---|---|
TotalColoring.MatchingLowerBound.IsMatchingGraph |
MatchingLowerBound |
A spanning graph whose neighbor set at every vertex is subsingleton |
TotalColoring.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_ge |
MatchingLowerBound |
Produces a matching with at least k edges from minimum-degree and order bounds |
TotalColoring.MatchingLowerBound.IsMatchingGraph.exists_subgraph_edgeFinset_card_eq |
MatchingExact |
Trims a matching to any prescribed smaller edge count |
TotalColoring.MatchingLowerBound.exists_matchingGraph_edgeFinset_card_eq |
MatchingExact |
Exact-cardinality form of the general matching lower bound |
TotalColoring.MatchingLowerBound.card_sub_maxDegree_add_one_le_degree_compl |
HighDegreeComplementMatching |
Gives the required lower bound on every complement degree |
TotalColoring.MatchingLowerBound.twice_card_sub_maxDegree_add_one_le_card |
HighDegreeComplementMatching |
Derives the matching order bound from the high-degree hypothesis |
TotalColoring.MatchingLowerBound.exists_complement_matchingGraph_edgeFinset_card_ge |
HighDegreeComplementMatching |
Produces a sufficiently large matching in the complement |
TotalColoring.MatchingLowerBound.exists_complement_matchingGraph_edgeFinset_card_eq |
HighDegreeTotalColoring |
Produces the exact complement matching needed for the class count |
Complement-matching adapter¶
| Declaration | Module | Purpose |
|---|---|---|
TotalColoring.Auxiliary.PairSingletonWitness.ofComplementMatching |
ComplementMatchingWitness |
Converts a matching subgraph of the complement into a pair/singleton witness |
TotalColoring.Auxiliary.PairSingletonWitness.ofComplementMatching_partner_eq_some_iff |
ComplementMatchingWitness |
Identifies selected partners with matching adjacency |
TotalColoring.Auxiliary.PairSingletonWitness.ofComplementMatching_singletonVertices |
ComplementMatchingWitness |
Identifies singleton vertices with the complement of the matching support |
TotalColoring.Auxiliary.PairSingletonWitness.ofComplementMatching_distinguished_card_eq_card_sub |
ComplementMatchingWitness |
Relates the distinguished count to the complement matching edge count |
TotalColoring.Auxiliary.PairSingletonWitness.ofComplementMatching_distinguished_card |
ComplementMatchingWitness |
Produces an exact prescribed distinguished count from an exact matching count |
TotalColoring.Auxiliary.exists_pairSingletonWitness_of_highDegree |
HighDegreeTotalColoring |
Packages a high-degree witness with P.distinguished.card = G.maxDegree + 1 |
Core predicates¶
| Declaration | Module | Purpose |
|---|---|---|
TotalColoring.InAuxiliaryClass |
AuxiliaryClass |
Pair-level structural predicate for the matching-plus-star class |
TotalColoring.ExtensionPalette |
CriticalState |
The auxiliary palette Fin (D + 2) |
TotalColoring.HasValidRainbowColoring |
CriticalState |
Existence of a proper auxiliary edge coloring rainbow on J |
TotalColoring.Auxiliary.Extension |
Auxiliary |
Conflict-preserving data for decoding auxiliary edge colors to a total assignment |
Supplied pair/singleton interface¶
These declarations remain public for downstream developments that already have a pair/singleton witness.
| Declaration | Module | Purpose |
|---|---|---|
TotalColoring.Auxiliary.PairSingletonWitness |
PairSingletonExtension |
A fixed partition relation into independent singleton and pair classes |
TotalColoring.Auxiliary.PairSingletonWitness.auxiliaryGraph |
PairSingletonExtension |
The ordinary auxiliary graph on Option V |
TotalColoring.Auxiliary.PairSingletonWitness.extension |
PairSingletonExtension |
The conflict-preserving extension into the auxiliary graph |
TotalColoring.Auxiliary.PairSingletonWitness.classEdge_mem_distinguishedEdgeSet |
PairSingletonExtension |
Every decoder selector belongs to the distinguished edge set |
TotalColoring.Auxiliary.PairSingletonWitness.distinguished_exact_coverage |
PairSingletonExtension |
Every copied original vertex lies on exactly one distinguished edge |
TotalColoring.Auxiliary.PairSingletonWitness.matchingPart_isEdgeMatching |
PairSingletonExtension |
The off-center distinguished family is a matching |
TotalColoring.Auxiliary.PairSingletonWitness.matchingPart_avoids_center_neighbors |
PairSingletonExtension |
Matching endpoints are not neighbors of the new center |
TotalColoring.Auxiliary.PairSingletonWitness.distinguished_decomposition |
PairSingletonExtension |
The distinguished family is the matching part union the full center star |
TotalColoring.Auxiliary.PairSingletonWitness.degree_none_eq_singletonVertices_card |
PairSingletonExtension |
Identifies center degree with the singleton-vertex count |
TotalColoring.Auxiliary.PairSingletonWitness.degree_some_eq |
PairSingletonExtension |
Identifies copied-vertex degree with original degree plus one |
TotalColoring.Auxiliary.PairSingletonWitness.card_add_degree_none_eq_two_mul_distinguished_card |
PairSingletonExtension |
Relates graph order, center degree, and class count exactly |
TotalColoring.Auxiliary.PairSingletonWitness.isAuxiliaryClassMember_of_class_count_and_bounds |
PairSingletonExtension |
Produces structural membership from class-count, degree, and order bounds |
TotalColoring.Auxiliary.PairSingletonWitness.isAuxiliaryClassMember_of_highDegree |
PairSingletonExtension |
Produces membership at parameter G.maxDegree + 1 from exact count and density |
Supplied equitable-partition interface¶
The supplied-partition declarations are retained as an alternate entrypoint. The terminal package theorem does not assume that such a partition is given.
| Declaration | Module | Purpose |
|---|---|---|
TotalColoring.Auxiliary.EquitableIndependentPartition |
EquitablePairSingleton |
Exactly D nonempty independent classes with equitable sizes |
TotalColoring.Auxiliary.EquitableIndependentPartition.class_card_eq_one_or_two |
EquitablePairSingleton |
Derives class sizes one or two from D <= Fintype.card V < 2D |
TotalColoring.Auxiliary.EquitableIndependentPartition.toPairSingletonWitness |
EquitablePairSingleton |
Constructs the concrete pair/singleton witness |
TotalColoring.Auxiliary.EquitableIndependentPartition.distinguished_card |
EquitablePairSingleton |
Proves the induced distinguished family has cardinality D |
TotalColoring.Auxiliary.EquitableIndependentPartition.highDegreeWitness_inAuxiliaryClass |
EquitablePairSingleton |
Packages auxiliary membership for a supplied high-degree partition |
TotalColoring.Auxiliary.EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition |
EquitablePairSingleton |
Produces a valid assignment from a supplied partition and density hypothesis |
Reusable auxiliary terminal entrypoints¶
| Declaration | Module | Checked conclusion |
|---|---|---|
TotalColoring.IsOutsideEdgeMinimalNoncolorable.false_of_critical_allD |
CriticalAllDClosure |
A finite outside-edge-minimal noncolorable auxiliary member is impossible |
TotalColoring.MinimalExtraction.hasValidRainbowColoring_of_inAuxiliaryClass |
CriticalAllDClosure |
Every finite InAuxiliaryClass D H J has HasValidRainbowColoring D H J |
TotalColoring.Auxiliary.Extension.decode_valid |
Auxiliary |
A proper selector-rainbow auxiliary assignment decodes to a valid total assignment |
TotalColoring.Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass |
AuxiliaryTransfer |
A supplied compatible extension into a finite auxiliary-class member yields a valid assignment with palette Fin (D + 2) |
The supplied-extension theorem remains conditional on its explicit extension, selector-membership, and auxiliary-class inputs. The terminal high-degree theorem discharges those inputs through the complement-matching route; it does not weaken or replace the reusable conditional theorem.
Executable checker soundness¶
| Declaration | Accepted Boolean implies |
|---|---|
TotalColoring.Certificate.checkTotal_sound |
The supplied total assignment is semantically valid |
TotalColoring.Certificate.checkEdge_sound |
The supplied edge assignment is proper |
TotalColoring.Certificate.checkRainbow_sound |
Distinguished selector edges have pairwise distinct colors |
TotalColoring.Certificate.checkExtension_sound |
The accepted auxiliary certificate decodes to a valid total assignment |
The checkers operate on already well-typed Lean values. Parsing arbitrary JSON or proving an external census complete is outside these soundness theorems.
Copyable inspection¶
import TotalColoring
#check TotalColoring.exists_valid_assignment_of_highDegree
#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.Auxiliary
.exists_valid_assignment_of_highDegree_nonempty
#check TotalColoring.exists_valid_assignment_of_isEmpty
#check TotalColoring.MatchingLowerBound
.exists_matchingGraph_edgeFinset_card_ge
#check TotalColoring.MatchingLowerBound
.exists_complement_matchingGraph_edgeFinset_card_eq
#check TotalColoring.Auxiliary
.exists_pairSingletonWitness_of_highDegree
#check TotalColoring.MinimalExtraction
.hasValidRainbowColoring_of_inAuxiliaryClass
#check TotalColoring.Auxiliary.Extension
.exists_valid_decode_of_inAuxiliaryClass
#check TotalColoring.Auxiliary.EquitableIndependentPartition
.exists_valid_assignment_of_highDegreePartition
#check TotalColoring.Certificate.checkExtension_sound
The canonical version of this snippet is maintained in
examples/Quickstart.lean. Current main commit
da0595da…, tree 34824cd5…, contains the independent-seed, selector/path,
and partial-edge groups. Their earlier source commits and trees remain
historical proof provenance. The final adapted-spare endpoint #check
targets the declaration merged into main by PR #13; any verification claim
must cite a tree-specific external receipt.