Formalize the Graceful Tree (Ringel–Kotzig) conjecture in Lean 4

Prove in Lean 4 the theorem (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem 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 => |f u − f v| for the endpoints u,v of e) = Finset.Icc 1 m ``` (the edge-difference is the repo's `e.lift` of `fun u v => (f u - f v : ℤ).natAbs`; see the source file for the exact well-defined lift). Meaning: every tree $T$ with $m$ edges has a graceful labeling — an injection $f:V\to\{0,\dots,m\}$ whose induced edge labels $|f(u)-f(v)|$ range over exactly $\{1,\dots,m\}$.

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. Genuinely open (all trees). For a FIXED tree the labeling is a finite decidable search, so strong PARTIAL results are natural: formalize graceful labelings for known families (paths, stars, caterpillars) or verify all trees up to $N$ vertices. If a per-tree `decide`/`native_decide` search is used, disclose the TCB.