Graceful Tree Conjecture (Ringel–Kotzig conjecture)

Reference: Wikipedia/Graceful_labeling

Conjectured by Ringel (1963) and Kotzig; formalized by Rosa (1967).

theorem GracefulLabeling.graceful_tree_one_vertex : let T := ⊥; have m := T.edgeFinset.card; ∃ (f : Unit → ℕ), Function.Injective f ∧ (∀ (v : Unit), f v ≤ m) ∧ Finset.image (fun (e : Sym2 Unit) => Sym2.lift ⟨fun (u v : Unit) => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m

theorem GracefulLabeling.graceful_tree_two_vertex : let T := ⊤; have m := T.edgeFinset.card; ∃ (f : Fin 2 → ℕ), Function.Injective f ∧ (∀ (v : Fin 2), f v ≤ m) ∧ Finset.image (fun (e : Sym2 (Fin 2)) => Sym2.lift ⟨fun (u v : Fin 2) => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m

theorem GracefulLabeling.graceful_tree_conjecture {V : Type u_1} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) : have m := T.edgeFinset.card; ∃ (f : V → ℕ), Function.Injective f ∧ (∀ (v : V), f v ≤ m) ∧ Finset.image (fun (e : Sym2 V) => Sym2.lift ⟨fun (u v : V) => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m

Every tree admits a graceful labeling.

A graceful labeling of a tree $T$ with $m$ edges is an injective map $f : V \to \{0, \dots, m\}$ such that the multiset of absolute differences $|f(u) - f(v)|$ over edges $\{u,v\}$ of $T$ equals $\{1, \dots, m\}$.