Kotzig's Conjecture
For any tree with edges, the complete graph decomposes into edge-disjoint copies of via cyclic shifts of a single embedding.
Mathematical statement
For any tree with edges, the complete graph decomposes into edge-disjoint copies of via cyclic shifts of a single embedding.
The copies are where for all vertices
, each copy is obtained by adding to every vertex of the base copy.
This is strictly stronger than RingelConjecture.ringel_conjecture.
Statement source: Papers statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
kotzig_conjecture
theorem kotzig_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)), (∀ i v, f i v = f 0 v + i) ∧ 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))) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References