Positive edge weights, geodesic cycles, and peripheral cycles

Definition

opg500_weighted_cycle_models

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

combinatoricsformalizationgeodesicsgraph-theory

This definition bundle fixes the finite weighted-graph semantics used by the OPG-500 mission.

For a finite simple graph $G$ , an edge weight is a real-valued function on the actual edge subtype $E(G)$ , and positivity means $0<\ell(e)$ for every edge. A cycle is a nontrivial simple closed walk. Its weighted length counts every traversed edge, and a shortest path is required to be simple and no longer than every other simple path with the same endpoints.

A cycle is vertex-geodesic when every pair of its vertices can be joined by a globally shortest simple path using only edges of the cycle. A cycle is peripheral when it is chordless and deleting its vertices leaves a connected induced graph or no vertices. Three-connectivity means that the graph has at least four vertices and remains connected after deleting any set of fewer than three vertices.

The bundle also defines binary edge-indicator vectors over $\mathbb Z/2\mathbb Z$ and the tight-edge predicate needed by supporting targets.

Definition code

import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
import Mathlib.Combinatorics.SimpleGraph.Walk.Chord
import Mathlib.Data.Real.Basic

open Set
open scoped Sym2

namespace OPG500Counterexample

universe u

abbrev Edge {V : Type u} (G : SimpleGraph V) := G.edgeSet

abbrev EdgeWeight {V : Type u} (G : SimpleGraph V) := Edge G → ℝ

def IsPositive {V : Type u} {G : SimpleGraph V} (ℓ : EdgeWeight G) : Prop :=
  ∀ e, 0 < ℓ e

structure Cycle {V : Type u} (G : SimpleGraph V) where
  base : V
  walk : G.Walk base base
  isCycle : walk.IsCycle

def Walk.edgeList {V : Type u} {G : SimpleGraph V} {u v : V}
    (p : G.Walk u v) : List (Edge G) :=
  p.edges.attach.map fun e => ⟨e.1, p.edges_subset_edgeSet e.2⟩

def Walk.weightedLength {V : Type u} {G : SimpleGraph V} {u v : V}
    (ℓ : EdgeWeight G) (p : G.Walk u v) : ℝ :=
  ((Walk.edgeList p).map ℓ).sum

def Walk.IsShortest {V : Type u} {G : SimpleGraph V} {u v : V}
    (ℓ : EdgeWeight G) (p : G.Walk u v) : Prop :=
  p.IsPath ∧ ∀ q : G.Walk u v, q.IsPath →
    Walk.weightedLength ℓ p ≤ Walk.weightedLength ℓ q

def Cycle.vertexSet {V : Type u} {G : SimpleGraph V} (C : Cycle G) : Set V :=
  {v | v ∈ C.walk.support}

def Cycle.edgeSet {V : Type u} {G : SimpleGraph V} (C : Cycle G) : Set (Sym2 V) :=
  C.walk.edgeSet

def Cycle.edgeVector {V : Type u} [DecidableEq V] {G : SimpleGraph V}
    (C : Cycle G) (e : Sym2 V) : ZMod 2 :=
  if e ∈ C.walk.edges then 1 else 0

def CycleList.edgeVectorSum {V : Type u} [DecidableEq V] {G : SimpleGraph V}
    (cycles : List (Cycle G)) (e : Sym2 V) : ZMod 2 :=
  (cycles.map fun C => C.edgeVector e).sum

/-- A graph edge is tight when its one-edge walk is a globally shortest path
between its endpoints. The existential endpoints make this definition independent
of an orientation chosen for the unordered edge. -/
def Edge.IsTight {V : Type u} {G : SimpleGraph V}
    (ℓ : EdgeWeight G) (e : Edge G) : Prop :=
  ∃ x y : V, ∃ h : G.Adj x y,
    e.1 = s(x, y) ∧ Walk.IsShortest ℓ h.toWalk

/-- A vertex-based weighted geodesic cycle: between any two of its vertices,
there is a globally shortest simple path using only edges of the cycle. -/
def Cycle.IsGeodesic {V : Type u} {G : SimpleGraph V}
    (ℓ : EdgeWeight G) (C : Cycle G) : Prop :=
  ∀ ⦃x y : V⦄, x ∈ C.vertexSet → y ∈ C.vertexSet →
    ∃ p : G.Walk x y, Walk.IsShortest ℓ p ∧ p.edgeSet ⊆ C.edgeSet

/-- An induced cycle whose vertex deletion leaves a connected graph or no vertices. -/
def Cycle.IsPeripheral {V : Type u} {G : SimpleGraph V} (C : Cycle G) : Prop :=
  C.walk.IsChordless ∧
    (IsEmpty {v : V // v ∉ C.vertexSet} ∨
      (G.induce {v | v ∉ C.vertexSet}).Connected)

/-- Vertex 3-connectivity for a finite simple graph: at least four vertices,
and deletion of any set of fewer than three vertices leaves a connected graph. -/
def IsThreeConnected {V : Type u} [Fintype V] (G : SimpleGraph V) : Prop :=
  4 ≤ Fintype.card V ∧
    ∀ s : Finset V, s.card < 3 → (G.induce {v | v ∉ s}).Connected

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 and Section 5, Problem 3; Open Problem Garden OPG-500, https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem

Read-back

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

For a simple graph $G$ on a vertex type $V$ , Edge G is the set of unordered vertex pairs that are edges of $G$ .

EdgeWeight G is the type of all functions assigning a real number to each edge of $G$ .

An edge-weight function $\ell$ is IsPositive exactly when $0<\ell(e)$ for every edge $e$ of $G$ .

A Cycle G consists of a vertex $b$ , a walk in $G$ from $b$ back to $b$ , and a proof that this closed walk is a cycle, namely a simple nontrivial closed walk in the graph.

For a walk $p$ in $G$ , Walk.edgeList p is the ordered list of the edges traversed by $p$ , with each edge recorded as an element of Edge G; repeated traversals remain repeated in the list.

For an edge-weight function $\ell$ and a walk $p$ , Walk.weightedLength \ell p is the sum of $\ell(e)$ over the ordered edge list of $p$ , counting every traversal.

A walk $p$ from $u$ to $v$ is Walk.IsShortest \ell p exactly when $p$ is a simple path and, for every simple path $q$ from $u$ to $v$ , the weighted length of $p$ is at most the weighted length of $q$ .

For a cycle $C$ , Cycle.vertexSet C is the set of vertices occurring in its walk.

For a cycle $C$ , Cycle.edgeSet C is the set of unordered vertex pairs occurring as edges in its walk.

Given a cycle $C$ , a finite vertex type $V$ with decidable equality, and an unordered pair $e$ of vertices, Cycle.edgeVector C e is the element of $\mathbb Z/2\mathbb Z$ equal to $1$ if $e$ occurs among the edges traversed by $C$ , and equal to $0$ otherwise.

For a finite list of cycles $(C_1,\ldots,C_n)$ and an unordered pair $e$ , CycleList.edgeVectorSum is the sum in $\mathbb Z/2\mathbb Z$ of the values `Cycle.edgeVector C_i e$ for all entries of the list, including repetitions.

An edge $e$ of $G$ is Edge.IsTight \ell exactly when there exist vertices $x,y$ and an adjacency proof that $x$ and $y$ are joined by an edge such that the unordered pair underlying $e$ is $\{x,y\}$ and the one-edge walk from $x$ to $y$ is a globally shortest simple path under $\ell$ .

A cycle $C$ is Cycle.IsGeodesic \ell exactly when, for every two vertices $x,y$ occurring in $C$ , there exists a walk $p$ from $x$ to $y$ that is a globally shortest simple path under $\ell$ and whose set of traversed edges is contained in the edge set of $C$ .

A cycle $C$ is Cycle.IsPeripheral exactly when its walk is chordless and either there are no vertices outside C.vertexSet C, or the graph induced by all vertices outside C.vertexSet C is connected.

For a finite simple graph $G$ on $V$ , IsThreeConnected G means that $V$ has at least four vertices and, for every finite set $s$ of vertices with fewer than three elements, the graph induced by the vertices not in $s$ is connected.

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