Theorem 3.1: weighted geodesic cycles generate the finite cycle space

Proved

OPG500Counterexample.finite_geodesic_cycles_generate

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsformalizationgeodesicsgraph-theory

Let $G$ be a finite simple graph and let $\ell:E(G)\to\mathbb R$ be strictly positive on every edge. For every simple cycle $C$ of $G$ , there is a finite list of vertex-geodesic simple cycles such that each listed cycle $D$ satisfies

\operatorname{length}_{\ell}(D)\leq\operatorname{length}_{\ell}(C),

and the sum over $\mathbb F_2$ of their edge-indicator vectors is the edge-indicator vector of $C$ . The statement permits repeated entries and does not assume unique shortest paths.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

Formal statement

namespace OPG500Counterexample

universe u

/-- Georgakopoulos--Sprüssel, Theorem 3.1, in the finite vertex-geodesic form:
every cycle is a binary sum of no-longer geodesic cycles. -/
theorem finite_geodesic_cycles_generate
    {V : Type u} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (ℓ : EdgeWeight G) (hpositive : IsPositive ℓ)
    (C : Cycle G) :
    ∃ cycles : List (Cycle G),
      (∀ D, D ∈ cycles →
        D.IsGeodesic ℓ ∧
          Walk.weightedLength ℓ D.walk ≤ Walk.weightedLength ℓ C.walk) ∧
      CycleList.edgeVectorSum cycles = C.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, Theorem 3.1

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

Let $G$ be a finite simple graph on a vertex type $V$ with decidable equality, let $\ell$ assign a real number to every edge of $G$ , and assume $\ell(e)>0$ for every edge. For every cycle $C$ of $G$ , there exists a finite list of cycles of $G$ such that every listed cycle $D$ is vertex-geodesic—between any two of its vertices it has a globally shortest simple path using only its edges—and satisfies

\operatorname{length}_{\ell}(D)\le \operatorname{length}_{\ell}(C),

and such that the coordinatewise sum modulo $2$ of the edge-indicator vectors of all listed cycles equals the edge-indicator vector of $C$ . The list is not required by the statement to be nonempty or to contain distinct cycles.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph