König’s Edge-Coloring Theorem

The checked proof obtains an injective adjacent selector on maximum-degree vertices, turns its finite path components into a matching that covers every such vertex, deletes that matching to lower the maximum degree, and colors recursively before assigning one fresh color.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

1. 

   01

   Hall counting gives an injective neighbor selector

   |S| ≤ |N(S)| ⇒ injective selector

   For every finite set of maximum-degree vertices, degree counting gives at least as many available neighbors. The resulting Hall inequalities produce one injective adjacent selector on the full maximum-degree set.

   Lean lemmas for this step

   • card_le_card_biUnion_neighborFinset_of_forall_degree_eq_maxDegree
   • exists_injective_neighbor_of_maxDegree_vertices

2. 

   02

   Follow a selector path to its first exit

   unhit source → finite selector path → first exit

   When the selector range is not contained in the maximum-degree set, start at a source that is not selected by any other source and iterate the selector. No vertex repeats before the first exit, and alternating path edges begin the covering matching.

   Lean lemmas for this step

   • exists_unselected_source_of_not_range_subset
   • selector_path_ne_of_lt
   • exists_first_iterate_exit_of_unselected
   • exists_isMatching_cover_of_selector_path

3. 

   03

   Resolve selector components into a matching

   selector components ⇒ covering matching

   Following selector arrows in the finite bipartite graph produces paths and cycles. Choosing alternating edges component by component removes selector collisions and yields one matching covering all maximum-degree vertices.

   Lean lemmas for this step

   • selector_path_ne_of_lt
   • exists_isMatching_cover_of_selector_path
   • exists_isMatching_cover_subset_of_injective_neighbor
   • exists_isMatching_cover_maxDegree_vertices_of_bipartite

4. 

   04

   Delete the covering matching

   Δ(G ∖ M) ≤ Δ(G)−1

   Every former maximum-degree vertex loses an incident edge, while all other vertices had degree below Δ already. The remainder is bipartite and has maximum degree at most Δ−1.

   Lean lemmas for this step

   • edgeColorable_of_isMatching_sdiff
   • degree_sdiff_of_le
   • maxDegree_sdiff_spanningCoe_le_pred_of_isMatching_cover
   • isBipartiteWith_sdiff

5. 

   05

   Restore one fresh matching color

   (Δ−1) colors + 1 matching color = Δ colors

   The upper-left state colors six remainder edges as two perfect matchings: cobalt solid edges pair corresponding rows, while emerald long-dash edges cycle to the next right-bank row. The lower-left state contains the deleted matching alone as three antique-gold dot-dash edges cycling to the remaining row. The right state combines all nine edges on the same three-by-three bipartite vertex set. Each color-and-rhythm class is a matching, and every final vertex meets exactly one cobalt, one emerald, and one gold edge, so incident colors are pairwise distinct. The finite graph is an explanatory example; the exact general theorem remains in HTML.

   Lean lemmas for this step

   • konigEdgeColoringTheorem_of_matching_cover
   • edgeColorable_of_isMatching_sdiff
   • ProperEdgeColoring
   • konigEdgeColoringTheorem