A non-geodesic cycle splits into two strictly shorter cycles whose binary edge vectors add to it

Proved

OPG500Counterexample.nongeodesic_cycle_splits

by Zehao Jin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricscycle-spacegraph-theory

Let $G$ be a finite simple graph with strictly positive real edge lengths $\ell$ , and let $C$ be a simple cycle of $G$ that is not vertex-geodesic: some pair of vertices of $C$ has no globally shortest path using only edges of $C$ . Then there are two simple cycles $A$ and $B$ of $G$ with

\operatorname{length}_{\ell}(A)<\operatorname{length}_{\ell}(C),\qquad \operatorname{length}_{\ell}(B)<\operatorname{length}_{\ell}(C),

whose edge-indicator vectors over $\mathbb F_2$ satisfy $\mathbf 1_{E(C)}=\mathbf 1_{E(A)}+\mathbf 1_{E(B)}$ .

This is the inductive step in the proof of Theorem 3.1 of Georgakopoulos and Sprüssel: choosing a bad pair $(u,v)$ of vertices of $C$ together with a shortest $u$ – $v$ path $P$ of minimal length among all bad pairs forces the interior of $P$ to avoid $C$ and $P$ to be strictly shorter than both arcs of $C$ between $u$ and $v$ ; gluing $P$ to each arc yields $A$ and $B$ . The statement is precisely the split hypothesis of the mission's descent principle geodesic_cycle_outside_span, so that principle can be applied directly to any positively weighted finite graph. No uniqueness of shortest paths is assumed and ties are allowed.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

Formal statement

namespace OPG500Counterexample

universe u

/-- The splitting step of Georgakopoulos--Sprüssel, Theorem 3.1: a cycle that is not
vertex-geodesic is the binary sum of two strictly shorter cycles. This is exactly the
`split` hypothesis of `geodesic_cycle_outside_span`. -/
theorem nongeodesic_cycle_splits
    {V : Type u} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (ℓ : EdgeWeight G) (hpositive : IsPositive ℓ)
    (C : Cycle G) (hC : ¬ C.IsGeodesic ℓ) :
    ∃ A B : Cycle G,
      Walk.weightedLength ℓ A.walk < Walk.weightedLength ℓ C.walk ∧
      Walk.weightedLength ℓ B.walk < Walk.weightedLength ℓ C.walk ∧
      C.edgeVector = A.edgeVector + B.edgeVector := by sorry

end OPG500Counterexample

Source

Georgakopoulos--Sprüssel, Geodetic topological cycles in locally finite graphs, EJC 16 (2009), R144, https://arxiv.org/abs/0911.3999v1, Section 3.1, proof of Theorem 3.1 (the splitting of a non-geodesic cycle along a shorter path)

View graph