FormalConjectures.Wikipedia.GracefulLabeling

FormalConjectures
Wikipedia
GracefulLabeling

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Graceful Tree Conjecture (Ringel–Kotzig conjecture)

Reference: Wikipedia/Graceful_labeling

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


namespace GracefulLabeling


open SimpleGraph


@[category test, AMS 5]
lemma graceful_tree_one_vertex :
    let T : SimpleGraph Unit := ⊥
    let m := T.edgeFinset.card
    ∃ f : Unit → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => byT:SimpleGraph Unit := ⊥m:ℕ := T.edgeFinset.cardf:Unit → ℕe:Sym2 Unitu:Unitv:Unit⊢ (fun u v => (↑(f u) - ↑(f v)).natAbs) u v = (fun u v => (↑(f u) - ↑(f v)).natAbs) v u
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbsT:SimpleGraph Unit := ⊥m:ℕ := T.edgeFinset.cardf:Unit → ℕe:Sym2 Unitu:Unitv:Unit⊢ (↑(f u) - ↑(f v)).natAbs = (↑(f v) - ↑(f u)).natAbs
                  rw [← Int.natAbs_neg, neg_sub]All goals completed! 🐙⟩) = Finset.Icc 1 m := by⊢ let T := ⊥;
let m := T.edgeFinset.card;
∃ f,
  Function.Injective f ∧
    (∀ (v : Unit), f v ≤ m) ∧
      Finset.image (fun e => Sym2.lift ⟨fun u v => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  intro T mT:SimpleGraph Unit := ⊥m:ℕ := T.edgeFinset.card⊢ ∃ f,
  Function.Injective f ∧
    (∀ (v : Unit), f v ≤ m) ∧
      Finset.image (fun e => Sym2.lift ⟨fun u v => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  use fun _ => 0hT:SimpleGraph Unit := ⊥m:ℕ := T.edgeFinset.card⊢ (Function.Injective fun x => 0) ∧
  (∀ (v : Unit), (fun x => 0) v ≤ m) ∧
    Finset.image (fun e => Sym2.lift ⟨fun u v => (↑((fun x => 0) u) - ↑((fun x => 0) v)).natAbs, ⋯⟩ e) T.edgeFinset =
      Finset.Icc 1 m
  refine ⟨fun _ _ _ => rfl, fun _ => Nat.zero_le _, ?_⟩hT:SimpleGraph Unit := ⊥m:ℕ := T.edgeFinset.card⊢ Finset.image (fun e => Sym2.lift ⟨fun u v => (↑((fun x => 0) u) - ↑((fun x => 0) v)).natAbs, ⋯⟩ e) T.edgeFinset =
  Finset.Icc 1 m
  simp [m, T]All goals completed! 🐙


@[category test, AMS 5]
lemma graceful_tree_two_vertex :
    let T : SimpleGraph (Fin 2) := ⊤
    let m := T.edgeFinset.card
    ∃ f : Fin 2 → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => byT:SimpleGraph (Fin 2) := ⊤m:ℕ := T.edgeFinset.cardf:Fin 2 → ℕe:Sym2 (Fin 2)u:Fin 2v:Fin 2⊢ (fun u v => (↑(f u) - ↑(f v)).natAbs) u v = (fun u v => (↑(f u) - ↑(f v)).natAbs) v u
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbsT:SimpleGraph (Fin 2) := ⊤m:ℕ := T.edgeFinset.cardf:Fin 2 → ℕe:Sym2 (Fin 2)u:Fin 2v:Fin 2⊢ (↑(f u) - ↑(f v)).natAbs = (↑(f v) - ↑(f u)).natAbs
                  rw [← Int.natAbs_neg, neg_sub]All goals completed! 🐙⟩) = Finset.Icc 1 m := by⊢ let T := ⊤;
let m := T.edgeFinset.card;
∃ f,
  Function.Injective f ∧
    (∀ (v : Fin 2), f v ≤ m) ∧
      Finset.image (fun e => Sym2.lift ⟨fun u v => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  intro T mT:SimpleGraph (Fin 2) := ⊤m:ℕ := T.edgeFinset.card⊢ ∃ f,
  Function.Injective f ∧
    (∀ (v : Fin 2), f v ≤ m) ∧
      Finset.image (fun e => Sym2.lift ⟨fun u v => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  use Fin.valhT:SimpleGraph (Fin 2) := ⊤m:ℕ := T.edgeFinset.card⊢ Function.Injective Fin.val ∧
  (∀ (v : Fin 2), ↑v ≤ m) ∧
    Finset.image (fun e => Sym2.lift ⟨fun u v => (↑↑u - ↑↑v).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  refine ⟨Fin.val_injective, byT:SimpleGraph (Fin 2) := ⊤m:ℕ := T.edgeFinset.card⊢ ∀ (v : Fin 2), ↑v ≤ m decideAll goals completed! 🐙, ?_⟩
  revert m Th⊢ let T := ⊤;
let m := T.edgeFinset.card;
Finset.image (fun e => Sym2.lift ⟨fun u v => (↑↑u - ↑↑v).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  decideAll goals completed! 🐙

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}$.

@[category research open, AMS 5]
theorem declaration uses 'sorry'graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V]
    (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) :
    let m := T.edgeFinset.card
    ∃ f : V → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => byV:Type u_1inst✝²:Fintype Vinst✝¹:DecidableEq VT:SimpleGraph Vinst✝:DecidableRel T.AdjhT:T.IsTreem:ℕ := T.edgeFinset.cardf:V → ℕe:Sym2 Vu:Vv:V⊢ (fun u v => (↑(f u) - ↑(f v)).natAbs) u v = (fun u v => (↑(f u) - ↑(f v)).natAbs) v u
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbsV:Type u_1inst✝²:Fintype Vinst✝¹:DecidableEq VT:SimpleGraph Vinst✝:DecidableRel T.AdjhT:T.IsTreem:ℕ := T.edgeFinset.cardf:V → ℕe:Sym2 Vu:Vv:V⊢ (↑(f u) - ↑(f v)).natAbs = (↑(f v) - ↑(f u)).natAbs
                  rw [← Int.natAbs_neg, neg_sub]All goals completed! 🐙⟩) = Finset.Icc 1 m := byV:Type u_1inst✝²:Fintype Vinst✝¹:DecidableEq VT:SimpleGraph Vinst✝:DecidableRel T.AdjhT:T.IsTree⊢ let m := T.edgeFinset.card;
∃ f,
  Function.Injective f ∧
    (∀ (v : V), f v ≤ m) ∧
      Finset.image (fun e => Sym2.lift ⟨fun u v => (↑(f u) - ↑(f v)).natAbs, ⋯⟩ e) T.edgeFinset = Finset.Icc 1 m
  sorryAll goals completed! 🐙


end GracefulLabeling