Total Coloring Lean v0.2.0

Lean 4 formalization and certificate checking for total coloring and auxiliary rainbow edge-coloring reductions.

• Every reusable theorem claim (8) is now judged by a comparator configuration: six new Mathlib-only Challenges, each with a machine-checked proof that it is not weaker than the library theorem, mapped with judged_as in claims.yaml.
• Release v0.1.0 predates the all-orders auxiliary theorem and conditional transfer.
• Verified at comparator tier with lean-pkg 0.14.0: both receipt tiers bind commit c025d20a1826 (sorry 0, standard axioms). Check it yourself: lean-pkg receipt check --repo . --commit c025d20a1826 --at v0.2.0 --docs-descendants.

Total Coloring Lean v0.1.0

Initial formal-assurance foundation for the total-coloring project.\n\n- Pins Lean and mathlib v4.32.0.\n- Defines semantic total- and edge-coloring assignments.\n- Proves exactness and soundness of executable finite checkers.\n- Proves conditional decoding from a proper rainbow auxiliary edge coloring.\n- Includes kernel-reduced K1/K2 acceptance and rejection examples.\n\nThis release does not prove the Total Coloring Conjecture, existence of the required auxiliary coloring, all finite orders, or completeness of an external graph census.