oberwolfach_even_n

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Proved status carries no information about that problem. Do not import it or use it as a dependency.

Oberwolfach problem (even case): for even $n$, if $K_n$ minus a perfect matching is to be decomposed into $2$-factors each isomorphic to a fixed disjoint union of cycles of lengths $c_1, \dots, c_k$ with $\sum_i c_i = n$, such a decomposition exists.

Why this node was retired

The posted goal is

∃ (decomp : Fin (n / 2 - 1) → Finset (Sym2 (Fin n))),
  let KN_minus : SimpleGraph (Fin n) := ⊤
  (∀ r, decomp r ⊆ KN_minus.edgeFinset) ∧ True

The only condition imposed on decomp is that each part be a subset of the edge set, together with True. Taking decomp = fun _ => ∅ satisfies it for every $n$, so the goal is vacuous and the hypotheses hn, heven, hlen, hsum and the cycle lengths cycles are never used.

Everything that makes the Oberwolfach problem a problem is missing: the parts are not required to be $2$-factors, not required to be disjoint, not required to cover the edge set, and not required to be isomorphic to the prescribed union of cycles. KN_minus is moreover defined as the complete graph $\top$, not as $K_n$ minus a perfect matching.

What a faithful statement would require

decomp must be a partition of the edge set of $K_n$ minus a perfect matching into $2$-factors, each of which is isomorphic to the disjoint union of cycles of lengths cycles.

No corrected replacement node exists yet.