Prüfer encoding equals the terminal peel accumulator

Proved

GYGraphTheory.pruferEncode_list_eq_terminal_acc

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

combinatoricsgraph-theoryprufer-codetrees

For every graph on $n\ge2$ labeled vertices, converting the function-valued Prüfer encoding to a list gives exactly the accumulator produced after the $n-2$ recursive peeling steps:

\operatorname{List.ofFn}(\operatorname{pruferEncode}(T)) =\operatorname{acc}(\operatorname{pruferPeel}(T,n-2)).

This is a definitional bookkeeping lemma connecting the public encoding interface with the recursive algorithm state. It makes no tree assumption because both sides are defined for arbitrary graphs.

Preamble

import Definitions.Def_GYGraphTheory
import Mathlib

open scoped Classical

Formal statement

namespace GYGraphTheory

/-- Turning the function-valued Prüfer encoding into a list recovers exactly
the accumulator after all `n - 2` peeling steps. -/
theorem pruferEncode_list_eq_terminal_acc {n : ℕ} (hn : 2 ≤ n)
    (T : SimpleGraph (Fin n)) :
    haveI : NeZero n := ⟨by omega⟩
    List.ofFn (pruferEncode T) = (pruferPeel T (n - 2)).2 := by
  sorry

end GYGraphTheory

Source

J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7, Algorithm 3.7.1, p. 157; definitional correspondence for the Prove2Me encoding

View graph