A geodesic cycle outside a closed binary family

Proved

OPG500Counterexample.geodesic_cycle_outside_span

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

combinatoricsformalizationgeodesicsgraph-theory

Let $G$ be a finite simple graph with strictly positive real edge weights, and let inside be a predicate on binary edge vectors that is closed under addition. Assume a finite list contains every simple cycle of $G$ and at least one cycle has its edge vector outside inside.

If every nongeodesic cycle splits into two strictly shorter simple cycles whose binary edge vectors sum to the original vector, then

\exists C,\quad C\text{ is vertex-geodesic and its edge vector is outside `inside`}.

The statement includes tied cycle lengths and requires strict decrease only for the two cycles supplied by a split.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

Formal statement

namespace OPG500Counterexample

universe u

/-- A graph-level finite descent principle. If every nongeodesic cycle splits
into two strictly shorter cycles whose binary edge vectors add to the original,
then any closed family missing some cycle also misses a geodesic cycle. -/
theorem geodesic_cycle_outside_span
    {V : Type u} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (ℓ : EdgeWeight G) (hpositive : IsPositive ℓ)
    (inside : (Sym2 V → ZMod 2) → Prop)
    (inside_add : ∀ a b, inside a → inside b → inside (a + b))
    (table : List (Cycle G))
    (complete : ∀ C : Cycle G, C ∈ table)
    (outside : ∃ C : Cycle G, ¬ inside C.edgeVector)
    (split : ∀ C : Cycle G, ¬ 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) :
    ∃ C : Cycle G, C.IsGeodesic ℓ ∧ ¬ inside C.edgeVector := by sorry

end OPG500Counterexample

Source

Candidate C10, Sections T3 and T6, and candidate C12: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c10/tight-rank.md; https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c12/FiniteDescent.lean

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 every edge have a positive real weight, and let inside be a predicate on functions $(\mathrm{Sym}^2 V)\to\mathbb Z/2\mathbb Z$ . Assume inside is closed under pointwise addition: whenever two edge-vectors are inside, their sum is inside. Let table be a list containing every cycle of $G$ . If some cycle $C$ has an edge-vector that is not inside, and every cycle $C$ that is not vertex-geodesic can be written using cycles $A,B$ with

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

and with the modulo- $2$ edge-vector identity

\mathbf v(C)=\mathbf v(A)+\mathbf v(B),

then there exists a vertex-geodesic cycle $C$ whose edge-vector is not inside.

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