BondyLongestCycles.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

Bondy's conjecture on longest cycles in highly connected graphs

References:

arxiv/2606.03696 Longest cycles and Dirac-type results in highly connected graphs by Jie Ma, Bo Ning, Ziyuan Zhao, where this is Conjecture 1.
[Bo80] Bondy, J. A., Longest paths and cycles in graphs of high degree. (1980).

Take a k-connected graph with a large minimum degree. Bondy says that the graph outside any longest cycle holds no long path.

The case k = 1 is Dirac's theorem and the case k = 2 is the theorem of Nash-Williams. The case k = 3 is proved. The cases k ≥ 4 are open.

Imports (1)

FormalConjecturesUtil

def Arxiv.«2606.03696».offWalk The set of vertices that a walk does not touch line 46 source
Source documentation
The set of vertices that a walk does not touch. For a longest cycle C this set carries the graph G - V(C) of the conjecture.

no axioms what this means
Statement uses: SimpleGraph, SimpleGraph.Walk, Set
Proof uses: Set.ofPred, Not, Membership.mem, List, SimpleGraph.Walk.support
1 instances, coercions and auxiliary constants left out.
```
def offWalk {a b : V} {G : SimpleGraph V} (w : G.Walk a b) : Set V :=
…
```
theorem Arxiv.«2606.03696».bondy_conjecture Conjecture 1 (Bondy, 1980) sorry line 60 source
Source documentation
Conjecture 1 (Bondy, 1980). Let $k \geq 1$ and let $G$ be a $k$-connected graph on $n$ vertices. If $\delta(G) \geq \frac{n + k(k-1)}{k+1}$, then for every longest cycle $C$ of $G$, every path in $G - V(C)$ has at most $k-1$ vertices.
The bound on the number of vertices of a path is written as + 1 ≤ k rather than ≤ k - 1, because subtraction on ℕ is truncated. The two forms agree for k ≥ 1.
A longest cycle is a cycle whose length is the circumference of G.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsKConnected, Real, HDiv.hDiv, HAdd.hAdd, Fintype.card, HMul.hMul, HSub.hSub, SimpleGraph.minDegree, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle and 8 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bondy_conjecture :
    answer(sorry) ↔ ∀ (k : ℕ), 1 ≤ k → ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], IsKConnected G k →
      ((Fintype.card V : ℝ) + k * (k - 1)) / (k + 1) ≤ G.minDegree →
      ∀ (a : V) (C : G.Walk a a), C.IsCycle → C.length = G.circumference →
      ∀ (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v), P.IsPath →
        P.support.length + 1 ≤ k := by
…
```
Mentions: Arxiv.«2606.03696».offWalk
theorem Arxiv.«2606.03696».bondy_conjecture.variants.one The case $k = 1$ is Dirac's theorem sorry line 74 source
Source documentation
The case $k = 1$ is Dirac's theorem. The condition reads $\delta(G) \geq n/2$, and no path in $G - V(C)$ can hold a vertex, so a longest cycle covers every vertex.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsKConnected, OfNat.ofNat, Nat, LE.le, Real, HDiv.hDiv, Fintype.card, SimpleGraph.minDegree, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length, SimpleGraph.circumference, Arxiv.«2606.03696».offWalk, SimpleGraph.induce and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bondy_conjecture.variants.one {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 1) (hd : ((Fintype.card V : ℝ)) / 2 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 1 := by
…
```
Mentions: Arxiv.«2606.03696».offWalk
theorem Arxiv.«2606.03696».bondy_conjecture.variants.two The case $k = 2$ is the theorem of Nash-Williams sorry line 85 source
Source documentation
The case $k = 2$ is the theorem of Nash-Williams.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsKConnected, OfNat.ofNat, Nat, LE.le, Real, HDiv.hDiv, HAdd.hAdd, Fintype.card, SimpleGraph.minDegree, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length, SimpleGraph.circumference, Arxiv.«2606.03696».offWalk and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bondy_conjecture.variants.two {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 2) (hd : ((Fintype.card V : ℝ) + 2) / 3 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 2 := by
…
```
Mentions: Arxiv.«2606.03696».offWalk
theorem Arxiv.«2606.03696».bondy_conjecture.variants.three The case $k = 3$ is proved sorry line 96 source
Source documentation
The case $k = 3$ is proved.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsKConnected, OfNat.ofNat, Nat, LE.le, Real, HDiv.hDiv, HAdd.hAdd, Fintype.card, SimpleGraph.minDegree, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length, SimpleGraph.circumference, Arxiv.«2606.03696».offWalk and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bondy_conjecture.variants.three {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : IsKConnected G 3) (hd : ((Fintype.card V : ℝ) + 6) / 4 ≤ G.minDegree)
    {a : V} (C : G.Walk a a) (hC : C.IsCycle) (hlong : C.length = G.circumference)
    (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v) (hP : P.IsPath) :
    P.support.length + 1 ≤ 3 := by
…
```
Mentions: Arxiv.«2606.03696».offWalk
theorem Arxiv.«2606.03696».bondy_conjecture.variants.large Theorem 1.1 (Ma-Ning-Zhao, 2026) sorry line 108 source
Source documentation
Theorem 1.1 (Ma-Ning-Zhao, 2026). The conjecture holds for every graph with enough vertices. The full conjecture, for graphs of every size, stays open.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Fintype.card, SimpleGraph.IsKConnected, Real, HDiv.hDiv, HAdd.hAdd, HMul.hMul, HSub.hSub, SimpleGraph.minDegree, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq and 7 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem bondy_conjecture.variants.large :
    ∀ k : ℕ, 1 ≤ k → ∃ N : ℕ, ∀ (V : Type) [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], N ≤ Fintype.card V → IsKConnected G k →
      ((Fintype.card V : ℝ) + k * (k - 1)) / (k + 1) ≤ G.minDegree →
      ∀ (a : V) (C : G.Walk a a), C.IsCycle → C.length = G.circumference →
      ∀ (u v : offWalk C) (P : (G.induce (offWalk C)).Walk u v), P.IsPath →
        P.support.length + 1 ≤ k := by
…
```
Mentions: Arxiv.«2606.03696».offWalk