The theorem
Let G be a finite simple graph on n vertices, let k ≥ 1, and suppose
G is k-connected. The paper proves that the minimum-degree condition
δ(G) ≥ (n + k(k − 1))/(k + 1)
forces the following conclusion: for every longest cycle C in G, every
path whose vertices lie outside C has fewer than k vertices. Equivalently,
every path in the residual graph G − V(C) has at most k − 1 vertices.
Because k + 1 is positive, this displayed real-division form is equivalent
to the natural-number product inequality used by the Lean statement:
n + k(k − 1) ≤ (k + 1)δ(G).
The exact Lean endpoint is Bondy.bondy_longest_cycle at audited source commit
9e13b044d8821b587935fa3019d913699eadffa2.
What is now checked
The August 16 paper is accompanied by a complete Lean 4 development against a
pinned Mathlib environment. The ProofAtlas checked-artifact record names the
headline theorem and binds the retained audit of 204 first-party modules in
its Bondy.Main dependency cone. Separately, Section 14 of the paper and the
paper audit enumerate the 20 formal declarations cited in the paper's
correspondence table. The retained transitive axiom report for the headline
theorem contains only:
propext;Classical.choice;Quot.sound.
The audit reports no sorry, admit, sorryAx, project mathematical axiom,
or theorem-valued premise in the checked result. The public formalization page
records the exact theorem type and evidence boundary:
ProofAtlas has not yet promoted this artifact to an accepted-result record. The Lean kernel check, statement correspondence, specialist mathematical review, historical priority, and ProofAtlas acceptance remain separate claims.
Proof architecture
The written proof separates into two reusable parts.
1. Reduce the longest-cycle problem to a residual cap
For a longest cycle C, the proof studies the components and paths outside
C. Connectivity supplies disjoint attachment routes back to the cycle.
Longestness then constrains how those routes can be spliced into C: a
successful longer detour would contradict the choice of C.
The attachment and depth-first-search argument turns a bound on generalized cycles in each residual component into the required path bound. The local representative system, branch accounting, and linkage estimates are all part of the checked dependency cone.
2. Prove the residual cap from the global degree hypothesis
The second part derives the necessary residual cap directly from the same global size and minimum-degree inequality. Middle residual orders follow from a cycle-extension inequality. The boundary case uses its positive-surplus specialization. The remaining high-residual range is excluded by charging the full linkage contribution inside the global vertex budget.
Combining the residual-cap theorem with the cycle-to-path core yields the headline theorem with no theorem-valued premise.
The retained boundary example
The older infographic remains useful as an exact sharpness illustration. For
k = 3, it shows
G = K₄ ∨ 5K₂.
This graph has 14 vertices, connectivity 4, and minimum degree 5, exactly the
displayed threshold. A longest cycle can pass through the K₄ core and four
of the five K₂ blocks. The untouched block is a residual two-vertex path, so
the bound k − 1 = 2 is attained.
The infographic explains this one example. It is not part of the Lean proof or a substitute for the source and audit.
Paper and formalization correspondence
The new 22-page paper identifies the exact audited formal-source revision and contains a 20-declaration correspondence table. Exact implementation names are kept in that table; the surrounding exposition uses descriptive mathematical language. The paper also includes source-native diagrams for the proof architecture, the sharpness family, and the depth-first-search representative geometry.
The paper's final visual and structural audit reports 22 pages, 17 outline entries, resolved references, no blank pages, no off-page link rectangles, and no TeX layout or reference warnings. The downloadable audit is editorial and structural evidence; it is not mathematical acceptance.
Authorship and AI disclosure
Lech Mazur is the paper author and accountable editor. The paper reports that OpenAI GPT-5.6 Pro contributed substantially to mathematical exploration, proof development, computational testing, adversarial auditing, exposition, and the Lean-assisted development process. The model is not credited as an author or as an independent reviewer.
Current boundary
- Lean checks the exact declaration
Bondy.bondy_longest_cycleat the pinned audited commit; it does not by itself establish that every sentence in the paper is correct. - Formal evidence and paper-to-formal-statement correspondence are distinct from specialist peer review and ProofAtlas accepted-result status.
- The complete release audit covers commit
9e13b044…. A later local commit adds further induction seams and is not presented as part of this audited public release. - No independent external priority anchor or literature-completeness review is recorded.
- The retained infographic explains one sharp example and is not proof or formal-verification evidence.