## 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:

- [Open the Lean-checked formalization](../../formalizations/bondy-longest-cycle-proof/)
- [Browse the immutable public source release](../../sources/bondy-longest-cycle-proof/)

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

1. Lean checks the exact declaration `Bondy.bondy_longest_cycle` at the pinned
   audited commit; it does not by itself establish that every sentence in the
   paper is correct.
2. Formal evidence and paper-to-formal-statement correspondence are distinct
   from specialist peer review and ProofAtlas accepted-result status.
3. 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.
4. No independent external priority anchor or literature-completeness review
   is recorded.
5. The retained infographic explains one sharp example and is not proof or
   formal-verification evidence.