Tight-edge metric bridge without unique shortest paths

Proved

OPG500Counterexample.tight_edge_metric_bridge

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

combinatoricsformalizationgeodesicsgraph-theory

Let $G$ be a finite connected simple graph with a strictly positive real weight on every edge. Every pair of vertices has a globally shortest simple path all of whose edges are tight, where an edge is tight when its one-edge walk is globally shortest between its endpoints.

Moreover, for every nontight edge $e$ , there exist endpoints $x,y$ , a globally shortest simple $x$ – $y$ path $p$ , and a vertex-geodesic simple cycle $C$ satisfying

E(C)=\{e\}\cup E(p).

No uniqueness of shortest paths is assumed.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

open Set
open scoped Sym2

Formal statement

namespace OPG500Counterexample

universe u

/-- For a finite connected graph with positive real edge lengths, shortest paths
use tight edges; a nontight edge together with a shortest path between its
endpoints supports a geodesic cycle. No uniqueness of shortest paths is assumed. -/
theorem tight_edge_metric_bridge
    {V : Type u} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (hconnected : G.Connected)
    (ℓ : EdgeWeight G) (hpositive : IsPositive ℓ) :
    (∀ x y : V,
      ∃ p : G.Walk x y,
        Walk.IsShortest ℓ p ∧
          ∀ e (he : e ∈ p.edges), Edge.IsTight ℓ ⟨e, p.edges_subset_edgeSet he⟩) ∧
    (∀ e : Edge G, ¬ Edge.IsTight ℓ e →
      ∃ x y : V, ∃ h : G.Adj x y, ∃ p : G.Walk x y, ∃ C : Cycle G,
        e.1 = s(x, y) ∧ Walk.IsShortest ℓ p ∧ C.IsGeodesic ℓ ∧
          C.edgeSet = insert e.1 p.edgeSet) := by sorry

end OPG500Counterexample

Source

Candidate C10, Sections T1 and T2: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c10/tight-rank.md

Read-back

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

Let $G$ be a finite simple connected graph on a vertex type $V$ , and let $\ell$ assign a positive real number to every edge. First, for every pair of vertices $x,y$ , there exists a globally shortest simple path $p$ from $x$ to $y$ such that every edge traversed by $p$ is tight: an edge is tight when its one-edge walk between its endpoints is itself a globally shortest simple path.

Second, for every edge $e$ that is not tight, there exist vertices $x,y$ , an adjacency between them whose underlying unordered edge is $e$ , a walk $p$ from $x$ to $y$ , and a cycle $C$ such that $p$ is a globally shortest simple path, $C$ is vertex-geodesic, and

C.\mathrm{edgeSet}=\{e\}\cup p.\mathrm{edgeSet}.

No uniqueness of shortest paths is asserted.

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