/-
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 FormalConjecturesUtilRingel's Conjecture
Ringel's conjecture (1963): the complete graph $K_{2n+1}$ decomposes into copies of any tree
with $n$ edges. It remains open; the case of all sufficiently large $n$ is proved by
Montgomery–Pokrovskiy–Sudakov, see Arxiv/2001.02665/RingelConjecture.lean.
namespace RingelConjecture
open SimpleGraph
For any tree $T$ with $n$ edges, the complete graph $K_{2n+1}$ decomposes into $2n+1$ edge-disjoint copies of $T$.
A "copy" of $T$ is the image $T.\text{map}(f_i)$ of $T$ under a vertex embedding $f_i : V \hookrightarrow \text{Fin}(2n+1)$; the copies are pairwise edge-disjoint and together cover every edge of $K_{2n+1}$.
@[category research open, AMS 5]
theorem ringel_conjecture {V : Type} [Finite V]
(T : SimpleGraph V) (hT : T.IsTree)
(n : ℕ) (hn : T.edgeSet.ncard = n) :
∃ f : Fin (2 * n + 1) → (V ↪ Fin (2 * n + 1)),
Pairwise (fun i j => Disjoint (T.map (f i)).edgeSet (T.map (f j)).edgeSet) ∧
⨆ i, T.map (f i) = (⊤ : SimpleGraph (Fin (2 * n + 1))) := V:Typeinst✝:Finite VT:SimpleGraph VhT:T.IsTreen:ℕhn:T.edgeSet.ncard = n⊢ ∃ f,
(Pairwise fun i j => Disjoint (SimpleGraph.map (f i) T).edgeSet (SimpleGraph.map (f j) T).edgeSet) ∧
⨆ i, SimpleGraph.map (f i) T = ⊤
All goals completed! 🐙
end RingelConjecture