# Guide for coding agents This page gives coding assistants a small, safe context window for the project. ## Read order 1. Inspect the exact terminal declaration in `TotalColoring/HighDegreeTotalColoring.lean`. For the separate supplied-witness endpoint, inspect `TotalColoring/IndependentSeed.lean`; historical source commit `cc4dd7ae1d858ea0583549f88707952e2414bf60` remains its proof provenance. For the total-independent selector and alternating-path wrappers, inspect `TotalColoring/TotalIndependentSelector.lean`; historical source commit `d008514c7a1cf834007bf0bd8de0d10a93926711` remains their proof provenance. For the adapted-spare vertex endpoint, inspect `TotalColoring/AdaptedSpareEndpoint.lean`; historical source commit `a7ed2453ca044d37583240a9b47729c9c4d5a940` remains its proof provenance. 2. Read [`claim-boundary.json`](claim-boundary.json) and check that its pinned tree matches the code tree you are discussing. 3. For the terminal route, inspect `MatchingLowerBound.lean`, `HighDegreeComplementMatching.lean`, `MatchingExact.lean`, `ComplementMatchingWitness.lean`, `PairSingletonExtension.lean`, `AuxiliaryTransfer.lean`, and `EmptyAssignment.lean` as needed. 4. Use the [curated theorem index](theorem-index.md) to find public entrypoints. 5. Read `AGENTS.md` before proposing or making repository changes. 6. Read only the additional source modules needed for the current theorem or definition. ## Authority order 1. Lean declarations at the exact pinned tree determine what is proved. Current `main` and any unmerged proof branch are distinct authorities. 2. `AGENTS.md` determines repository and trust policy. 3. `docs/claim-boundary.json` is the machine-readable public mirror. 4. The README and Pages explain the result but cannot broaden it. If code and prose disagree, narrow the prose. If two trees differ, a receipt for one does not automatically verify the other. ## Mandatory claim guardrails - The package terminal declaration is `TotalColoring.exists_valid_assignment_of_highDegree`. - Its graph-theoretic hypothesis is exactly `Fintype.card V <= 2 * G.maxDegree`, in addition to the displayed finite and decidability instances in its type. - Its conclusion is a valid assignment in `ExtensionPalette (G.maxDegree + 1)`, definitionally `Fin (G.maxDegree + 3)`. - The theorem covers both empty and nonempty finite vertex types. It has no parity hypothesis. - The result is a propositional existence theorem, not an executable coloring extractor for external graph data. - For the nonempty branch, keep the actual route straight: complement-degree bound, general matching lower bound, exact-size trimming, `PairSingletonWitness`, auxiliary-class membership, rainbow auxiliary coloring, and semantic decoding. - The empty branch uses `exists_valid_assignment_of_isEmpty`; it is not an unproved side condition. - Never call the package terminal theorem the Total Coloring Conjecture, a `G.maxDegree + 2` result, a locked or fully proved manuscript theorem, or a novelty result. - Do not extend the theorem to graphs outside its density hypothesis. - The independent-seed declarations are on current `main` commit `da0595da1fa93c51a00be78193071bdea74aeb02`, tree `34824cd54afb9a244a3fb58608a8d4da9bd6cfa6`. Their historical proof source is `agent/independent-seed-endpoint` at commit `cc4dd7ae1d858ea0583549f88707952e2414bf60`, tree `9af6a84e1305aed9a0156dcd59c279de792dea4a`; PR #10 merged them. - The separate generic endpoint `TotalColoring.exists_valid_assignment_of_independentSeedPeel` requires exactly `0 < q`, a supplied proper `phi : EdgeAssignment G (Fin q)`, a supplied independent seed `A`, and a supplied `IndependentSeedPeelCertificate G A q`; it concludes a valid assignment in `Fin (q + 1)`. - The direct wrapper `TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel` takes the corresponding explicit witnesses at `q = G.maxDegree + 1` and concludes a valid assignment in `Fin (G.maxDegree + 2)`. - Neither independent-seed declaration proves Vizing's theorem, constructs the proper edge assignment, or proves existence of the independent seed or peel certificate. Never present either as an unrestricted Total Coloring Conjecture theorem or as a strengthening of the terminal high-degree theorem's unconditional scope. - Exact source tree `9af6a84e…` passed sealed offline Easley trust jobs `5389587` and `5389588`, including strict leaf, umbrella/full, Quickstart, axiom, `leanchecker`, metadata, and reconstruction gates. This verifies the conditional decoder; it does not verify existence of its inputs. - The selector declarations are on current `main` commit `da0595da…`, tree `34824cd5…`. Their historical proof source is `agent/total-independent-selector-decoder` at source commit `d008514c7a1cf834007bf0bd8de0d10a93926711`, exact tree `1847934c78da03fe80bb67236868700c79016129`; PR #11 merged them. - `exists_valid_assignment_of_totalIndependentSelectorPeel` requires a supplied proper `Fin q` edge coloring, independent fresh-color vertex set, matching fresh-color edge set avoiding those vertices, actual-list core coloring, and core-relative peel certificate. Its maximum-degree wrapper only substitutes `q = G.maxDegree + 1`. - `AlternatingRainbowPathSelectorCertificate` makes the proposed donor exchange explicit: indexed path/endpoints, rainbow colors, unused old spare, alternating matching families, start avoidance, core colors, and peel data. The corresponding wrapper checks the exchange but does not prove existence of the path or certificate. - Neither selector wrapper proves Vizing, constructs a canonical core or selector, or proves the peel/path existence seam. Never present its conditional `Fin (G.maxDegree + 2)` conclusion as the unrestricted Total Coloring Conjecture. - Exact source tree `1847934c…` passed sealed Easley job `5391803` with exit `0:0` through strict leaf, target/umbrella/full, Quickstart, axiom, `leanchecker`, JSON/diff, and exact-tree gates. The receipt verifies the implications only. - The partial-edge decoder and exact reverse normalization are likewise on current `main` after PR #12. Their historical source commit is `c3dbe69c…`, tree `11007a4a…`. The reverse theorem still begins with a supplied valid total assignment and is not a coloring-existence theorem. - `TotalColoring.adaptedSpareVertexColor_proper_iff`, on `main` after PR #13, assumes `Disjoint A B` and characterizes properness of the supplied endpoint assignment exactly by: independence of `A`; coverage of every adjacent equal-missing pair by `A ∪ B`; cleanliness of head labels against unchanged neighbors; and properness of head labels on adjacent vertices of `B`. - That adapted-spare declaration is vertex-side only. It does not construct `A`, `B`, a physical donor matching, seed or matching data, missing/head labels, a proper edge coloring, or a total coloring. Never present it as an unrestricted `Delta + 2` theorem or a proof of the Total Coloring Conjecture. Attribute it to `main`; any verification claim must cite a tree-specific external receipt. - Keep package proof status and publication trust separate. The exact proof-development tree `4624044788ab42c0dc116cfbf7f38c696065263c` passed five separate high-memory full/Quickstart/`leanchecker` jobs (`5388311` through `5388315`). The later publishable tree `89a32c7a78e294a8b1484092ec79afaa3b4ace5a` received its own Wave 11 exact-tree gate and PR-head plus post-merge public CI before PR #8 merged it into `main`. - Do not say release `v0.1.0` contains the terminal theorem; cite a later exact commit or release that actually contains it. ## Retained conditional interfaces Do not erase or misdescribe the more general supplied-input theorems: - `MinimalExtraction.hasValidRainbowColoring_of_inAuxiliaryClass` applies to every finite formal `InAuxiliaryClass D H J` and uses an auxiliary edge palette `Fin (D + 2)`. - `Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass` keeps its supplied extension, selector-membership proof, and auxiliary-class membership explicit. - A supplied `PairSingletonWitness` exposes its concrete graph, extension, selector coverage, structural class, and numerical lemmas. - `EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition` remains a valid route from an explicit supplied partition on a nonempty graph together with `Fintype.card V <= 2 * G.maxDegree`. - On current `main` (historical source commit `cc4dd7ae…`), `exists_valid_assignment_of_independentSeedPeel` and its maximum-degree wrapper remain conditional on the explicitly supplied proper edge coloring, independent seed, and peel certificate. - On current `main` (historical source commit `d008514…`), the total-independent selector decoder and alternating-path wrapper retain every selector, core, peel, and path witness as explicit input. The supplied equitable partition is no longer a premise of the package terminal theorem. `HighDegreeTotalColoring` constructs the needed witness from an exact complement matching. Say which API you are using instead of carrying limitations from one interface over to another. ## Repository map | Need | Start here | | --- | --- | | Package terminal theorem | `TotalColoring/HighDegreeTotalColoring.lean` | | Conditional independent-seed endpoint on `main` | `TotalColoring/IndependentSeed.lean`; historical source `cc4dd7ae…`, tree `9af6a84e…` | | Total-independent selector decoder on `main` | `TotalColoring/TotalIndependentSelector.lean`; historical source `d008514…`, tree `1847934c…` | | Partial-edge decoder and normalization on `main` | `TotalColoring/PartialEdgeSelector.lean`; historical source `c3dbe69c…`, tree `11007a4a…` | | Adapted-spare vertex endpoint on `main` | `TotalColoring/AdaptedSpareEndpoint.lean`; historical source `a7ed2453…` | | Empty-vertex base case | `TotalColoring/EmptyAssignment.lean` | | General matching lower bound | `TotalColoring/MatchingLowerBound.lean` | | High-degree complement specialization | `TotalColoring/HighDegreeComplementMatching.lean` | | Exact matching extraction | `TotalColoring/MatchingExact.lean` | | Complement matching to witness | `TotalColoring/ComplementMatchingWitness.lean` | | Supplied pair/singleton interface | `TotalColoring/PairSingletonExtension.lean` | | Supplied equitable-partition interface | `TotalColoring/EquitablePairSingleton.lean` | | All-orders auxiliary theorem | `TotalColoring/CriticalAllDClosure.lean` | | Conditional auxiliary-to-total transfer | `TotalColoring/AuxiliaryTransfer.lean` | | Auxiliary predicate | `TotalColoring/AuxiliaryClass.lean` | | Semantic coloring definitions | `TotalColoring/Total.lean` | | Conditional decoding | `TotalColoring/Auxiliary.lean` | | Executable checkers | `TotalColoring/Certificate.lean` | | Complete import surface | `TotalColoring.lean` | | Modification rules | `AGENTS.md`, then `CONTRIBUTING.md` | ## Useful prompts ### Explain the package theorem safely > Explain the exact hypotheses and conclusion of > `TotalColoring.exists_valid_assignment_of_highDegree`. Trace the nonempty > complement-matching route and the empty base case. State the exact palette, > and separate the Lean package theorem from manuscript and novelty claims. ### Write downstream Lean from graph hypotheses > Write Lean code applying > `TotalColoring.exists_valid_assignment_of_highDegree` to a finite graph. > Keep the density hypothesis explicit and do not add parity, nonempty, or > supplied-partition assumptions that are absent from the theorem's type. ### Write downstream Lean from supplied structure > Apply `Auxiliary.Extension.exists_valid_decode_of_inAuxiliaryClass` while > keeping the supplied extension, selector-membership proof, and > `InAuxiliaryClass D H J` explicit. Alternatively, use > `EquitableIndependentPartition.exists_valid_assignment_of_highDegreePartition` > only when an explicit partition and the required high-degree density > inequality have already been supplied. ### Use the conditional `Delta + 2` wrapper safely > Apply > `TotalColoring.exists_valid_assignment_of_maxDegreeIndependentSeedPeel` while > keeping the proper `EdgeAssignment G (Fin (G.maxDegree + 1))`, its validity, > the independent seed, and its peel certificate explicit. State that the > declaration does not prove Vizing or seed existence and is not an > unrestricted Total Coloring Conjecture theorem. It is available on current > `main`; cite historical source commit `cc4dd7ae…` only when discussing proof > provenance. ### Use the total-independent selector safely > Apply > `TotalColoring.exists_valid_assignment_of_maxDegreeTotalIndependentSelectorPeel` > only with an explicit proper edge coloring, independent vertex selector, > matching edge selector avoiding it, actual-list core coloring, and peel > certificate. If using > `exists_valid_assignment_of_maxDegreeAlternatingRainbowPathSelector`, list > the certificate fields and state that Lean checks the donor exchange but > does not prove path/certificate existence. It is available on current > `main`; cite historical source commit `d008514…` only for proof provenance. ### Use the partial-edge normalization safely > On current `main`, the forward partial-edge decoder requires > old edge properness only on `E(G) \ F`; values on the matching `F` are > ignored. Keep independence of `S`, matching and avoidance for `F`, and the > old vertex allowed/proper conditions explicit. The reverse constructor > `partialEdgeSelectorNormalization_of_valid` begins with a supplied valid > total assignment and proves an exact decomposition of that assignment. Do > not turn this converse into an existence claim, an unconditional > `Delta + 2` theorem, or a proof of the Total Coloring Conjecture. ### Use the adapted-spare endpoint safely > On `main`, apply > `TotalColoring.adaptedSpareVertexColor_proper_iff` only with explicit > `Disjoint A B` and supplied `missing` and `head` data. State all four > equivalent conditions and that the theorem is vertex-side only. Do not > infer construction of a donor matching, seed/matching existence, a proper > edge coloring, a total coloring, an unrestricted `Delta + 2` result, or the > Total Coloring Conjecture. ### Audit prose > Classify every mathematical sentence as kernel-checked at the exact tree, > conditional on an explicit hypothesis, external mathematics, bounded > computation, manuscript-only, or unsupported. Cite the exact Lean > declaration where one exists. ### Find a checker > Locate the Boolean checker corresponding to this semantic predicate and the > theorem proving its soundness. State what parsing or completeness claims > remain outside the checker. ## Modification workflow Before editing, inspect the branch and dirty tree. Keep changes small, use no proof placeholders, update documentation mirrors when the public theorem boundary changes, and run the complete gate from `AGENTS.md`. Heavy full-library verification may be delegated to CI or an appropriate build node, but it may not be skipped before publication.