Terminal degree invariant for Prüfer peeling

Proved

GYGraphTheory.pruferPeel_terminal_degree_count

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgraph-theoryprufer-codetrees

Let $T$ be a labeled tree on $n\ge2$ vertices. Run the Prüfer peeling algorithm for all $n-2$ removal steps and let $A$ be its accumulated list of recorded neighbor labels. Then every vertex $k$ satisfies

\deg_T(k)=\operatorname{count}_A(k)+1.

This is the terminal form of the standard induction invariant: whenever a leaf is deleted, its neighbor's degree and that neighbor's remaining occurrence count both decrease by one; the deleted leaf contributes its final incident edge, and the two surviving vertices contribute the final unrecorded edge.

Preamble

import Definitions.Def_GYGraphTheory
import Mathlib

open scoped Classical

Formal statement

namespace GYGraphTheory

/-- The terminal invariant of Prüfer peeling: after `n - 2` leaf removals,
each original degree is its accumulated neighbor-label count plus one. -/
theorem pruferPeel_terminal_degree_count {n : ℕ} (hn : 2 ≤ n)
    (T : SimpleGraph (Fin n)) (hT : T.IsTree) (k : Fin n) :
    haveI : NeZero n := ⟨by omega⟩
    T.degree k = (pruferPeel T (n - 2)).2.count k + 1 := by
  sorry

end GYGraphTheory

Source

J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7, proof of Proposition 3.7.1, p. 159

View graph