\documentclass[10pt,a4paper]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage[margin=1in]{geometry}
\usepackage{microtype}
\usepackage{enumitem}
\usepackage{booktabs}
\usepackage{array}
\usepackage{longtable}
\usepackage{xcolor}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,calc,decorations.pathreplacing,positioning,shapes.geometric}
\usepackage{hyperref}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!55!black,
  citecolor=blue!55!black,
  urlcolor=blue!55!black,
  pdftitle={A Formalized Proof of Bondy's Minimum-Degree Longest-Cycle Conjecture},
  pdfauthor={Lech Mazur},
  pdfsubject={A formalized proof of Bondy's minimum-degree longest-cycle conjecture},
  pdfkeywords={Bondy's conjecture, longest cycles, minimum degree, connectivity, residual paths, depth-first search, Lean}
}

\setlist{nosep}
\allowdisplaybreaks
\setlength{\emergencystretch}{2em}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\MNZ}{Ma--Ning--Zhao}
\newcommand{\cbar}{\overline c}
\newcommand{\leanname}[1]{\nolinkurl{#1}}
\numberwithin{equation}{section}

\title[Bondy's minimum-degree longest-cycle conjecture]{A Formalized Proof of Bondy's Minimum-Degree Longest-Cycle Conjecture}
\author{Lech Mazur}
\email{2022melodies@gmail.com}
\date{Revised public version of August 16, 2026.}
\subjclass[2020]{Primary 05C38; Secondary 05C35, 05C40.}
\keywords{Bondy's conjecture, longest cycles, minimum degree, graph connectivity, residual paths, depth-first search, formal verification, Lean.}

\newcommand{\AIDisclosure}{%
  \begin{center}
  \setlength{\fboxsep}{8pt}%
  \fcolorbox{blue!65!black}{blue!3}{%
    \parbox{0.92\textwidth}{\small
      \textbf{Generative-AI disclosure.}
      Generative AI played a substantial role in the discovery and derivation
      of the mathematics in this paper, not merely in editing its presentation.
      Lech Mazur directed the AI-assisted research, designed the verification
      process, selected and reconciled the model's outputs, and takes
      responsibility for the resulting manuscript and its claims.  The AI
      system used was
      OpenAI GPT-5.6 Pro.  It contributed to mathematical exploration, proof
      development, computational testing, adversarial auditing, and exposition.
      The mathematical claims rest on the written proof and on the accompanying
      Lean~4 formalization identified below.  The formalization was developed
      with AI assistance and subjected to a separate adversarial audit.  Every
      declaration supporting the final theorem is checked by the Lean kernel
      and uses no project mathematical axiom or theorem-valued premise.
      Responsibility for any remaining error in this exposition or in the
      claimed correspondence with the formal artifact lies with the human
      author.\par\smallskip
      \textbf{Formalization status:} The theorem has been formalized in
      Lean~4 against a pinned Mathlib environment.  The exact theorem type,
      trust boundary, module correspondence, and reproducibility information
      are recorded in Section~\ref{sec:formal-certification}.
    }%
  }
  \end{center}
}

\begin{document}

\begin{abstract}
Let $G$ be a $k$-connected graph on $n$ vertices.  We prove that
\[
  \delta(G)\ge \frac{n+k(k-1)}{k+1}
\]
forces every path outside every longest cycle of $G$ to have at most $k-1$
vertices.  The proof has two independently reusable parts.  The first is an
attachment--DFS cycle-to-path argument: a cap
$\min\{k-1,\delta(G)-k\}$ on generalized residual cycles implies the desired
path bound.  The second proves that residual cap from the same global size
hypothesis.  Middle residual orders follow from a cycle-extension inequality,
the exact boundary is its positive-surplus specialization, and the remaining
strictly high residual range is excluded by paying the full linkage charge
inside the global vertex budget.  A single short external connector then gives
the sharp defect inequality that contradicts the resulting attachment-free
core inequality.  In particular, the proof neither invokes nor claims the stronger
standalone size-free Jung-type residual bound.  The complete argument has
been formalized in Lean~4.  The formal theorem has no theorem-valued premise,
and its transitive axiom audit contains only \texttt{propext},
\texttt{Classical.choice}, and \texttt{Quot.sound}.
\end{abstract}

\maketitle

\AIDisclosure

\section{Introduction and prior work}\label{sec:introduction}

Minimum-degree conditions that force long or spanning cycles form a central
theme of extremal graph theory.  Dirac's theorem states that an $n$-vertex
graph with minimum degree at least $n/2$ is Hamiltonian
\cite{Dirac1952}.  Nash-Williams proved that if $G$ is $2$-connected and
\[
  \delta(G)\ge \frac{n+2}{3},
\]
then every longest cycle of $G$ is dominating, equivalently, the vertices
outside it form an independent set \cite{NashWilliams1971}.  Bondy's 1980
conjecture \cite{Bondy1980} places these results in a common
higher-connectivity framework: for a $k$-connected graph satisfying
\[
  \delta(G)\ge \frac{n+k(k-1)}{k+1},
\]
every path outside every longest cycle should have at most $k-1$ vertices.
The cases $k=1$ and $k=2$ recover the conclusions of Dirac and
Nash-Williams, respectively.

As summarized by Ma, Ning, and Zhao \cite{MNZ2026}, before the present work
the conjecture was known for $k\le3$ but remained open in general for
$k\ge4$.  Their theorem establishes the conjecture for every fixed $k$ once
the order of the graph is sufficiently large; their proof gives the explicit
sufficient range
\[
  n\ge 5k^2+7k.
\]
Thus the strongest previous general result addressing Bondy's original
minimum-degree formulation retained a size restriction.  The present
manuscript proves the result for all $k\ge1$, with no
additional lower bound on $n$ beyond the statement of the conjecture.

A natural approach is first to cap the order of every generalized cycle
outside a longest cycle $C$.  Results of Nikoghosyan
\cite{Nikoghosyan2009,Nikoghosyan2023} motivated this viewpoint, but the
proof below does not use those results as external input.  That distinction
is important: the size-free residual statement suggested by this viewpoint
is a Jung-type theorem stronger than what is needed here, and it remains
outside the scope of this paper.  Instead we retain Bondy's global order
hypothesis throughout the residual analysis.  The hypothesis pays a linkage
charge that is invisible in a size-free formulation and closes the sole
strictly high residual range.

The proof is organized in two parts.  First, the attachment and
DFS-representative framework developed by Ma--Ning--Zhao \cite{MNZ2026} is
adapted to show that the generalized residual-cycle cap
\[
  \cbar(G-C)\le \min\{k-1,\delta(G)-k\}
\]
implies Bondy's path conclusion.  Its internal degree budget localizes every
possible excess over a path-position allowance and charges it to pairwise
disjoint off-path tails.  Second, we prove the required cap directly.  The
middle residual range is handled by a formally verified cycle-extension
inequality.  The exact residual boundary is a positive-surplus instance of the
same result.  For a strictly larger residual witness, pairwise-disjoint
minimal linkage routes pay the full linkage charge within the global vertex
budget; degree partition and linked attachment yield an attachment-free raw
core inequality; and one short external connector forces an incompatible
sharp defect.
The connectivity-two boundary is dispatched separately by Dirac's
circumference theorem.

Section~\ref{sec:statement} states the theorem and records sharpness.
Section~\ref{sec:notation} fixes notation and the generalized residual
convention.
Sections~\ref{sec:attachment}--\ref{sec:vertex-budget} develop the attachment,
DFS, positional, and disjoint-tail estimates.  The local theorem in
Section~\ref{sec:local-theorem} is retained as a useful independent
consequence; Section~\ref{sec:cycle-to-path-core} packages the exact
cycle-to-path core used
in the proof.  Sections~\ref{sec:cycle-extension}--\ref{sec:residual-cap}
establish the residual cap, and Section~\ref{sec:main-proof} finishes the
theorem.  Appendix~\ref{app:algebra} records the principal algebraic
identities.

\section*{Provenance and certification boundary}
The accompanying Lean~4 development is the certification artifact for the
complete theorem.  Computational searches, scalar scans, and informal
adversarial audits used during discovery were diagnostic only and are not
proof inputs.  No result of Nikoghosyan is imported as a mathematical
premise.  The Menger fan lemma is used in the auxiliary exposition below,
and the Erd\H{o}s--Gallai estimate is retained there for comparison with the
earlier degree-sum route; both are cited in their standard published forms.
The Dirac
circumference theorem used in the formal proof is proved inside the Lean
development, and the final theorem imports no unverified mathematical
result.  The global-to-local attachment framework in
Section~\ref{sec:attachment} follows the architecture of
\cite[Lemma~3.1 and equation~(20)]{MNZ2026}.  The DFS selection in
Section~\ref{sec:dfs-construction} is adapted from
\cite[Definitions~5.2--5.3]{MNZ2026}, and its ancestry, linkage, and
localization properties correspond to the roles of
\cite[Propositions~5.4--5.5]{MNZ2026}.  Lemma~\ref{lem:coarse-dfs}
corresponds to the coarse estimate in \cite[Lemma~5.6(i)]{MNZ2026}.
Theorem~\ref{thm:local-small-path} removes the local $q$-connectivity
hypothesis from the corresponding form of \cite[Theorem~6.1]{MNZ2026}; the
included proof shows directly that local longestness is sufficient.

There are two distinct verification chains, summarized in
Figure~\ref{fig:proof-architecture}.

\begin{figure}[tbp]
\centering
\begin{tikzpicture}[
  node distance=3.5mm and 12mm,
  chainbox/.style={
    draw=blue!55!black,
    rounded corners=2pt,
    fill=blue!3,
    align=center,
    text width=.37\textwidth,
    minimum height=7mm,
    inner sep=3pt,
    font=\small
  },
  chainarrow/.style={-{Stealth[length=2mm]},semithick,blue!55!black}
]
  \node[chainbox] (a1) {attachment and\\neighborhood localization};
  \node[chainbox,below=of a1] (a2)
    {DFS representatives and branch accounting};
  \node[chainbox,below=of a2] (a3)
    {positional and positive-excess estimates};
  \node[chainbox,below=of a3] (a4) {disjoint-tail charge};
  \node[chainbox,below=of a4] (a5) {cycle-to-path core};

  \node[chainbox,right=of a1] (b1)
    {middle range: cycle extension};
  \node[chainbox,below=of b1] (b2)
    {exact boundary:\\positive-surplus case};
  \node[chainbox,below=of b2] (b3)
    {strictly high range:\\global-size payment and attachment-free core};
  \node[chainbox,below=of b3] (b4)
    {short connector and sharp defect};
  \node[chainbox,below=of b4] (b5) {residual cap};

  \foreach \u/\v in {a1/a2,a2/a3,a3/a4,a4/a5,b3/b4,b4/b5}
    \draw[chainarrow] (\u) -- (\v);
  \draw[chainarrow] (b1.east) -- ++(4mm,0) |- (b5.east);
  \draw[chainarrow] (b2.west) -- ++(-4mm,0) |- (b5.west);

  \coordinate (assembly) at ($(a5.south)!0.5!(b5.south)+(0,-1.05)$);
  \node[chainbox,text width=.45\textwidth,fill=blue!8] (c) at (assembly)
    {Bondy's path conclusion};
  \draw[chainarrow] (a5.south) -- ++(0,-4mm) -| (c.west);
  \draw[chainarrow] (b5.south) -- ++(0,-4mm) -| (c.east);

  \node[font=\small\bfseries,above=2mm of a1]
    {Cycle-to-path chain};
  \node[font=\small\bfseries,above=2mm of b1]
    {Residual-cap cases};
\end{tikzpicture}
\caption{Proof architecture.  The right side exhausts three residual-order
regimes: the middle range, the exact boundary, and the strictly high range.
Their estimates are alternatives, not cumulative payments.  The resulting
residual cap and the independently proved cycle-to-path core yield the theorem.}
\label{fig:proof-architecture}
\end{figure}

The prose below gives the complete scalar recombination and the graph-facing
statements on which it depends.  In the dependency chain of
Theorem~\ref{thm:bondy}, the Lean source expands every path/cycle construction,
support intersection, generalized order-one/order-two boundary, and
finite-choice step.  The self-contained local theorem in
Section~\ref{sec:local-theorem} is an auxiliary written consequence and is not
used by the formal theorem.  Section~\ref{sec:formal-certification} records
the exact declaration correspondence and trust boundary.  The stronger
standalone size-free residual theorem is explicitly not claimed.

\section{Statement and sharpness}\label{sec:statement}

All graphs are finite, undirected, and simple.  Whenever a graph \(G\) is
under discussion, write \(n:=|V(G)|\).  The following minimum-degree form was
conjectured by Bondy \cite{Bondy1980}.

\begin{theorem}[Bondy's minimum-degree longest-cycle conjecture]\label{thm:bondy}
Let $k\ge1$ and let $G$ be a $k$-connected graph on $n\ge3$ vertices.  If
\[
  \delta(G)\ge \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.
\end{theorem}

\begin{remark}[Sharpness]\label{rem:sharpness}
For integers $t\ge\max\{k,2\}$, let
\[
  G=K_k\vee\bigl((k+1)K_t\bigr).
\]
Figure~\ref{fig:sharpness-construction} depicts this join schematically.
Then
\[
  n=k+(k+1)t,
  \qquad
  \delta(G)=k+t-1
  =\frac{n+k(k-1)-1}{k+1}.
\]
Thus the minimum degree is one below the least integral degree satisfying the
hypothesis.  The graph is $k$-connected: deleting fewer than the $k$ central
vertices leaves a central vertex adjacent to every remaining vertex, while
deleting all of $K_k$ disconnects the outer cliques.  If a cycle $D$ avoids
the central $K_k$, then $D$ lies in one outer clique.  Otherwise, deleting
$V(D)\cap V(K_k)$ from $D$ leaves at most
$|V(D)\cap V(K_k)|\le k$ path components, each contained in a single outer
clique.  Hence every cycle meets at most $k$ of the $k+1$ outer cliques.
In particular, every longest cycle $C$ leaves one entire $t$-clique
untouched, so $G-V(C)$ contains a path on $t\ge k$ vertices and the
threshold is sharp.  In the notation of the main proof, this one-below-threshold
example has $x=t-1$ while the untouched residual clique has
$s=t=x+1$; thus the key conclusion $s\le x$ fails by exactly one unit below
the stated degree threshold.
\end{remark}

\begin{figure}[tbp]
\centering
\begin{tikzpicture}[
  clique/.style={
    draw=blue!55!black,
    thick,
    ellipse,
    fill=blue!3,
    minimum width=22mm,
    minimum height=9mm,
    align=center
  },
  joinline/.style={line width=1.1pt,blue!45!black}
]
  \node[clique,minimum width=25mm,minimum height=16mm,fill=blue!9]
    (center) at (0,0) {$K_k$};
  \node[clique] (o1) at (4.4,2.1) {$K_t^{(1)}$};
  \node[clique] (o2) at (4.4,.8) {$K_t^{(2)}$};
  \node at (4.4,0) {$\vdots$};
  \node[clique] (ok) at (4.4,-.8) {$K_t^{(k)}$};
  \node[clique] (okp) at (4.4,-2.1) {$K_t^{(k+1)}$};

  \foreach \v in {o1,o2,ok,okp}
    \draw[joinline] (center.east) -- (\v.west);
  \node[font=\small,align=center] at (2.25,2.75)
    {complete join\\(schematic)};
  \draw[decorate,decoration={brace,amplitude=5pt}]
    (5.75,-2.55) -- (5.75,2.55)
    node[midway,right=6pt,align=left,font=\small]
      {$k+1$ pairwise\\nonadjacent cliques};
\end{tikzpicture}
\caption{The sharpness construction
$K_k\vee\bigl((k+1)K_t\bigr)$.  Every central vertex is adjacent to every
vertex of every outer clique, while distinct outer cliques have no edges
between them.  A cycle can visit at most $k$ outer cliques.}
\label{fig:sharpness-construction}
\end{figure}

\section{Notation and residual conventions}\label{sec:notation}

For a path or an ordinary cycle $Q$, $|Q|$ denotes its edge-length.  Paths
of order one and length zero are allowed.  The \emph{order} of a path is its
number of vertices; for an ordinary cycle, edge-length and order coincide.
For a positive integer $t$, write $[t]:=\{1,\ldots,t\}$.
For a connected graph $H$,
write
\[
  p(H):=\text{the order of a longest path of $H$}.
\]
The circumference $c(H)$ is the length of a longest ordinary cycle; when
$H$ is a forest we put $c(H):=2$.  For a vertex $v$ and a subgraph or vertex
set $X$, write
\[
  N_X(v):=N_G(v)\cap V(X),
  \qquad
  d_X(v):=|N_X(v)|.
\]
For disjoint vertex sets or subgraphs $A,B$, let $e(A,B)$ denote the number
of edges between them, and put
\[
  \delta_G(H):=\min\{d_G(v):v\in V(H)\}.
\]

Following the generalized-cycle convention used by Nikoghosyan
\cite{Nikoghosyan2009,Nikoghosyan2023}, every vertex and every edge is also
regarded as a generalized cycle of orders $1$ and $2$, respectively.  If $C$
is a longest ordinary cycle of $G$, let $\cbar(G-C)$ denote the maximum order
of a generalized cycle in $G-V(C)$, with value $0$ when $G-V(C)$ is empty.
We say that $C$ has \emph{residual cap $s$} when every such residual vertex,
edge, or ordinary cycle has order at most $s$.  Thus residual cap $s$ is
equivalent to $\cbar(G-C)\le s$.  Finiteness gives an attaining generalized
residual cycle whenever $G-V(C)$ is nonempty.  If its order is $c$, then
\begin{equation}
  |C|+c\le n.
  \label{eq:residual-packing}
\end{equation}
This packing inequality includes the order-one and order-two cases.

Let $G$ be a graph, let $C$ be a non-Hamiltonian cycle, and let $H$ be a
component of $G-V(C)$.  The cycle $C$ is \emph{locally longest with respect
to $H$} if every path with distinct endpoints $x,y\in V(C)$ and all internal
vertices in $H$ has length at most each of the two $x$--$y$ segments of $C$.
For an integer $q\ge2$, the component $H$ is \emph{locally $q$-connected to
$C$} if, from every $v\in V(H)$, there are $q$ paths to $q$ distinct vertices
of $C$, any two intersecting only at $v$, and each of these paths has all its
internal vertices in $H$ (equivalently, it meets $C$ only at its terminal
vertex).  A triple $(G,C,H)$ with these two properties is called a
$q$-triple system.  Whenever $H$ is a component of
$G-V(C)$, no vertex of $H$ is adjacent to a different component of
$G-V(C)$.  Consequently, for every $v\in V(H)$,
\[
  d_C(v)=d_G(v)-d_H(v).
\]

\begin{theorem}[Menger fan lemma]\label{thm:fan}
If $G$ is $k$-connected, $v\in V(G)$, and
$Y\subseteq V(G)\setminus\{v\}$ has at least $k$ vertices, then there are
$k$ paths from $v$ to $k$ distinct vertices of $Y$, any two intersecting
only at $v$.
\end{theorem}

This is the standard consequence of Menger's theorem; see
\cite{Diestel2017}.

\begin{theorem}[Erd\H{o}s--Gallai]\label{thm:eg}
If a connected graph $F$ on $m$ vertices has circumference at most $s$, with
$s=2$ for forests, then
\[
  2e(F)\le s(m-1).
\]
\end{theorem}

See \cite{EG1959}.  This contextual estimate is not used in the formal
proof below.

\section{Local attachment lemmas}\label{sec:attachment}

\begin{lemma}[Global longest cycles give local triples]\label{lem:global-triple}
Let $k\ge2$, let $G$ be $k$-connected, let $C$ be a non-Hamiltonian longest
cycle, and let $H$ be a component of $G-V(C)$.  Then $(G,C,H)$ is a
$k$-triple system.
\end{lemma}

\begin{proof}
Let $z_1\cdots z_m$ be a longest path of $G$, oriented toward the endpoint
$z_m$.  Every neighbor of $z_m$ lies on this path, and
$d_G(z_m)\ge k$.  If $z_r$ is the neighbor of $z_m$ with smallest index,
then $r\le m-k$, and the edge $z_mz_r$ together with the path segment
$z_rz_{r+1}\cdots z_m$ forms a cycle of length $m-r+1\ge k+1$.  Hence
$|C|\ge k+1$.  Fix $v\in V(H)$.  The Menger fan lemma supplies $k$
paths from $v$ to distinct vertices of $C$.  Truncate each at its first
contact with $C$.  Before that contact a path cannot leave the component $H$
of $G-V(C)$.  Their first-contact vertices remain distinct because the
original paths meet pairwise only at $v$, so the truncated paths establish
local $k$-connectivity.

If a path through $H$ with distinct endpoints $x,y\in V(C)$ were longer than
one of the two $x$--$y$ segments of $C$, replacing that segment would make a
cycle longer than $C$.  Thus $C$ is locally longest with respect to $H$.
\end{proof}

The next two elementary lemmas use the path-attachment framework of
\cite[Lemma~3.1 and equation~(20)]{MNZ2026}.  Their
proofs are included in the precise linked-set form needed below.

\begin{lemma}[Two-set path lemma]\label{lem:two-set-path}
Let $Q$ be a path and let $A,B\subseteq V(Q)$ be nonempty.  Some
$a\in A$ and $b\in B$ satisfy
\[
  |Q[a,b]|\ge\frac{|A|+|B|}{2}-1.
\]
\end{lemma}

\begin{proof}
Order $Q$ from one end to the other.  Let $a_1,a_2$ be the first and last
vertices of $A$, and let $b_1,b_2$ be the first and last vertices of $B$.
Edge by edge,
\[
  |Q[a_1,b_2]|+|Q[a_2,b_1]|
  \ge |Q[a_1,a_2]|+|Q[b_1,b_2]|.
\]
The right side is at least $|A|+|B|-2$, so one cross-distance has the claimed
size.
\end{proof}

\begin{lemma}[Linked-set attachment inequality]\label{lem:attachment}
Let $(G,C,H)$ be a triple in which $C$ is locally longest with respect to
$H$.  Let $P=v_1\cdots v_p$ be a path in $H$, let
$U=\{u_1,\ldots,u_p\}\subseteq V(H)$ consist of distinct vertices, and
suppose there are pairwise vertex-disjoint $(u_i,v_i)$-paths $R_i$ in $H$
such that
\[
  V(R_i)\cap V(P)=\{v_i\}.
\]
If $|N_C(U)|\ge2$, then
\[
  |C|\ge e(U,C)+|N_C(U)|.
\]
\end{lemma}

\begin{proof}
Write $N_C(U)=\{x_1,\ldots,x_q\}$ in cyclic order, with $x_{q+1}=x_1$.
For $i\in[q]$, define
\[
  A_i:=\{v_j:u_jx_i\in E(G)\},
  \qquad
  B_i:=\{v_j:u_jx_{i+1}\in E(G)\},
\]
and let
\[
  d_i:=\max\{|P[a,b]|:a\in A_i,\ b\in B_i\}.
\]
Lemma~\ref{lem:two-set-path} gives
\begin{equation}
  d_i\ge\frac{d_U(x_i)+d_U(x_{i+1})}{2}-1.
  \label{eq:attachment-two-set}
\end{equation}
If $d_i=0$, then $A_i=B_i=\{v_a\}$ for some $a$, and
$x_iu_ax_{i+1}$ is an $(x_i,H,x_{i+1})$-path of length $2$.  If $d_i\ge1$,
choose $v_a\in A_i$, $v_b\in B_i$ at distance $d_i$.  Then $a\ne b$ and
\[
  x_iu_aR_aP[v_a,v_b]R_b^{-1}u_bx_{i+1}
\]
is simple, because the linkage paths are pairwise disjoint and meet $P$ only
at their designated endpoints.  In either case there is an
$(x_i,H,x_{i+1})$-path of length at least
\[
  \frac{d_U(x_i)+d_U(x_{i+1})}{2}+1.
\]
Local maximality of $C$ bounds from below the $x_i$--$x_{i+1}$ segment of
$C$ whose interior contains no vertex of $N_C(U)$.  Summing these cyclic
segments gives
\[
  |C|\ge\sum_{i=1}^q d_U(x_i)+q
  =e(U,C)+|N_C(U)|.
\]
\end{proof}

\section{DFS representatives and branch accounting}\label{sec:dfs-construction}

Throughout Sections~\ref{sec:dfs-construction}--\ref{sec:vertex-budget}, let
$H$ be a connected graph of order $h$, let
$P=v_1\cdots v_p$ be a non-Hamiltonian longest path of $H$, and assume
$p\ge3$.  Choose a DFS tree $T$ rooted at $v_1$ by exploring $v_{i+1}$ first
whenever $v_i$ is explored, for $i<p$.  Thus $P$ is the initial root path.
For vertices $z,z'$ of $T$, write $z\le_Tz'$ when $z$ is an ancestor of
$z'$, including equality, and let $d_T(z)$ denote the ordinary undirected
degree of $z$ in the tree $T$.  A \emph{leaf} of the rooted tree $T$ means
a vertex with no children.

\begin{lemma}[DFS comparability]\label{lem:dfs-comparability}
The endpoints of every edge of $H$ are comparable in the ancestor order of
$T$.
\end{lemma}

\begin{proof}
Let $zz'\in E(H)$, and suppose $z$ is discovered first.  The recursive DFS
call rooted at $z$ inspects every edge incident with a vertex in its active
subtree before that call returns.  If $z'$ is discovered before the edge
$zz'$ is inspected, then it is discovered during this still-active call and
is already a descendant of $z$.  If it is still unvisited when $zz'$ is
inspected, DFS discovers it from the active subtree of $z$, so it is again a
descendant of $z$.  Thus the endpoints of $zz'$ are comparable.
\end{proof}

\begin{lemma}[Rooted-tree separation]\label{lem:tree-separation}
Let $T$ be a rooted tree.
\begin{enumerate}[label=(\roman*)]
\item Descendant subtrees rooted at incomparable vertices are disjoint.
\item If $a$ and $b$ are incomparable and $b\le_Tb'$, then $a$ and $b'$ are
incomparable.
\item If one entry of a finite multiset of integers is replaced by a strictly
larger integer, then the nondecreasing rearrangement is componentwise no
smaller and is strictly larger in at least one coordinate; in particular,
it is lexicographically larger.
\end{enumerate}
\end{lemma}

\begin{proof}
Part (i) is immediate from uniqueness of root paths.  For (ii), if $a$ were
comparable with $b'$, then either $b'\le_Ta$, which gives $b\le_Ta$, or
$a\le_Tb'$.  In the latter case $a$ and $b$ are both ancestors of $b'$ and
hence lie on the same root path, so they are comparable.  Both alternatives
contradict the hypothesis.  For (iii), for every threshold $\theta$ the
number of entries at most $\theta$ cannot increase; for a threshold between
the old and new entries it decreases by one.  Hence every order statistic
is weakly larger and the first affected one is strictly larger.
\end{proof}

Both endpoints of $P$ have tree degree one.  Indeed, neither endpoint has a
neighbor in $H-P$, since such a neighbor would extend $P$.  Thus $v_p$ has
no child.  Moreover, every component of $H-v_1$ contains a neighbor of
$v_1$, all such neighbors lie on the connected path $P-v_1$, and hence
$H-v_1$ is connected.  The first DFS child $v_2$ therefore discovers every
vertex of $H-v_1$, so it is the only child of $v_1$.  Consequently
$d_T(v_1)=d_T(v_p)=1$.

The following representative construction is adapted from
\MNZ\ Definitions~5.2--5.3 \cite{MNZ2026}.

\begin{enumerate}[label=(R\arabic*)]
\item Let
\[
  I_1:=\{i\in[p]:d_T(v_i)\ge3\}.
\]
For each $i\in I_1$, choose a child $z_i$ of $v_i$ outside $P$, and then a
leaf $u_i$ of $T$ with $z_i\le_Tu_i$.  Such a child exists: the
endpoint observation above shows that $i$ is internal, and $v_i$ already has
its parent and the path child $v_{i+1}$; a third tree incidence is therefore
an off-path child.  The subtree rooted at $z_i$ is disjoint from the child
subtree containing $v_{i+1},\ldots,v_p$, so no descendant of $z_i$ lies on
$P$; in particular, $u_i\in V(H-P)$.  Put
\[
  U_1:=\{u_i:i\in I_1\}.
\]
For distinct $i,i'\in I_1$, the chosen off-path child subtrees are disjoint,
so the leaves in $U_1$ are pairwise incomparable.  Consequently the empty
choice $I_2=\varnothing$ is feasible in the next optimization.

\item Choose $I_2\subseteq[p]\setminus I_1$ and pairwise distinct vertices
$w_i\in N_H(v_i)\setminus(V(P)\cup U_1)$, $i\in I_2$, such that:
\begin{enumerate}[label=(\roman*)]
\item any two \emph{distinct} vertices of $U_1\cup W$, where
$W:=\{w_i:i\in I_2\}$, are incomparable in $T$;
\item subject to (i), $|I_2|$ is maximum;
\item subject to (i)--(ii), the nondecreasing rearrangement of the depths
$|T[v_1,w_i]|$ is lexicographically maximum.  Its length is fixed by (ii),
so the lexicographic comparison is well defined.
\end{enumerate}
After $I_2$ and $W$ are fixed, choose for each $i\in I_2$ any leaf
$u_i$ of the descendant subtree rooted at $w_i$.  Since $w_i\notin P$ and a
descendant of an off-path vertex cannot return to the initial root path $P$,
we have $u_i\in V(H-P)$.  Unlike the additional leaf-depth optimization in
\MNZ, no secondary maximization of the paths $T[w_i,u_i]$ is imposed here;
all estimates below hold for every such descendant-leaf choice.

\item Let
\[
  I_3:=[p]\setminus(I_1\cup I_2),
\]
and set $u_i:=v_i$ for $i\in I_3$.
\end{enumerate}

Put
\[
  J:=I_1\cup I_2,
  \qquad
  U:=\{u_1,\dots,u_p\}.
\]
For $j\in J$, let $\ell_j$ be the largest index such that $v_{\ell_j}$ is an
ancestor of $u_j$, and define
\[
  Q_j:=T[v_{\ell_j},u_j],
  \qquad
  \widehat Q_j:=Q_j-\{v_{\ell_j}\}.
\]
Because $v_{\ell_j}$ is the last vertex of $P$ on the root path to $u_j$,
\begin{equation}
  V(Q_j)\cap V(P)=\{v_{\ell_j}\},
  \qquad
  \widehat Q_j\subseteq H-P.
  \label{eq:Q-meets-P}
\end{equation}
Finally, define the tail
\[
  Q'_j:=
  \begin{cases}
    \widehat Q_j, & j\in I_1,\\
    T[w_j,u_j], & j\in I_2,
  \end{cases}
  \qquad
  \nu_j:=|V(Q'_j)|.
\]

Figure~\ref{fig:dfs-representatives} records the three representative types
and the distinction between a tree branch and the extra graph edge used in
the $I_2$ construction.

\begin{figure}[tbp]
\centering
\begin{tikzpicture}[
  x=1cm,y=1cm,
  pvertex/.style={circle,draw=blue!60!black,fill=white,inner sep=1.5pt,
    minimum size=5.5mm,font=\small},
  bvertex/.style={circle,draw=orange!70!black,fill=orange!8,inner sep=1.3pt,
    minimum size=5.2mm,font=\small},
  treeedge/.style={semithick,blue!55!black},
  tail/.style={very thick,orange!75!black},
  graphedge/.style={densely dashed,thick,red!65!black},
  lab/.style={font=\scriptsize,align=center}
]
  \node[pvertex] (v1) at (0,0) {$v_1$};
  \node at (.9,0) {$\cdots$};
  \node[pvertex] (vi) at (1.8,0) {$v_i$};
  \node at (2.7,0) {$\cdots$};
  \node[pvertex] (vj) at (3.6,0) {$v_j$};
  \node at (4.8,0) {$\cdots$};
  \node[pvertex] (vl) at (6.0,0) {$v_{\ell_j}$};
  \node at (6.9,0) {$\cdots$};
  \node[pvertex] (vs) at (7.8,0) {$v_s$};
  \node at (8.7,0) {$\cdots$};
  \node[pvertex] (vp) at (9.6,0) {$v_p$};

  \draw[very thick,blue!65!black]
    (v1) -- (vi) -- (vj) -- (vl) -- (vs) -- (vp);
  \node[lab,above=4mm of vj] {$P$: initial DFS root path};

  \node[bvertex] (zi) at (1.8,-.85) {$z_i$};
  \node[bvertex] (ui) at (1.8,-1.75) {$u_i$};
  \draw[treeedge] (vi) -- (zi);
  \draw[tail] (zi) -- (ui);
  \node[lab,left=2mm of zi] {$Q_i$};
  \node[lab,below=2mm of ui] {$i\in I_1$};

  \node[bvertex] (aj) at (6.0,-.72) {};
  \node[bvertex] (wj) at (6.0,-1.42) {$w_j$};
  \node[bvertex] (uj) at (6.0,-2.30) {$u_j$};
  \draw[treeedge] (vl) -- (aj) -- (wj);
  \draw[tail] (wj) -- (uj);
  \draw[graphedge] (vj) to[bend right=20]
    node[lab,below,sloped] {$v_jw_j\in E(H)$} (wj);
  \node[lab,left=2mm of aj] {$Q_j$};
  \node[lab,right=3mm of uj] {$Q'_j=T[w_j,u_j]$};
  \node[lab,below=2mm of uj] {$j\in I_2$, $\ell_j>j$};
  \node[lab,below=3mm of vs] {$u_s=v_s$, $s\in I_3$};
\end{tikzpicture}
\caption{Schematic DFS representative geometry.  Every solid edge shown is a
DFS-tree edge: blue traces $P$ and the branch stems, while thick orange
highlights the tails counted in $H-P$.  The dashed red edge is an additional
edge of $H$.  No order relation among the sample indices $i,j,s$ is intended;
only $j<\ell_j$ is structural.}
\label{fig:dfs-representatives}
\end{figure}

\begin{remark}[Leaf-choice invariance]\label{rem:leaf-choice}
For $i\in I_2$, every later argument uses only that $w_i\le_Tu_i$, that
$u_i$ is a rooted DFS leaf, and that the path $T[w_i,u_i]$ lies in the
descendant subtree of $w_i$.  No comparison with a different descendant
leaf is made.  Thus the additional maximization of the selected leaf depths
used in \cite[Definition~5.2]{MNZ2026} is unnecessary for the estimates in
this paper.
\end{remark}

The next three propositions are proved directly from the construction.

\begin{proposition}[$I_2$ ancestry geometry]\label{prop:I2-geometry}
If $j\in I_2$, then
\begin{equation}
  v_j<_T w_j\le_Tu_j,
  \qquad
  \ell_j>j,
  \qquad
  \ell_j\notin\{1,p\},
  \qquad
  \ell_j\in I_1.
  \label{eq:I2-geometry}
\end{equation}
For $j\in I_1$, one has $\ell_j=j$.
\end{proposition}

\begin{proof}
If $j\in I_1$, the chosen child $z_j$ lies outside $P$ and below $v_j$;
therefore the last vertex of $P$ on the root path to $u_j$ is $v_j$, so
$\ell_j=j$.

Now let $j\in I_2$.  The endpoints of $v_jw_j$ are comparable by
Lemma~\ref{lem:dfs-comparability}.  Every ancestor of $v_j$ lies on the
initial root path $P$, whereas $w_j\notin V(P)$; hence $w_j$ cannot be an
ancestor of $v_j$, and $v_j<_Tw_j$.  The endpoints $v_1,v_p$ have no
neighbor in $H-P$, since such a neighbor would extend $P$, so $j$ is
internal.  Because $j\notin I_1$, the internal tree vertex $v_j$ has exactly
its parent $v_{j-1}$ and its path child $v_{j+1}$; in particular,
$v_{j+1}$ is its only child.  Thus $w_j$ lies below $v_{j+1}$ and
$\ell_j>j$.

If $\ell_j=p$, then by \eqref{eq:Q-meets-P} the tree path from $v_p$ to
$w_j$ meets $P$ only at $v_p$; appending it to $P$ would make a simple path
longer than $P$.  Hence $\ell_j<p$, while $\ell_j>j\ge2$ excludes
$\ell_j=1$.  At the internal vertex $v_{\ell_j}$, the tree path to $w_j$
leaves $P$ through an off-path child.  Together with its parent and its path
child, this gives $d_T(v_{\ell_j})\ge3$, so $\ell_j\in I_1$.
\end{proof}

\begin{proposition}[Disjoint tails, linkage, and injectivity]\label{prop:dfs-linkage}
The paths $Q'_j$, $j\in J$, are nonempty, pairwise vertex-disjoint, and
contained in $H-P$.  Consequently,
\begin{equation}
  \sum_{j\in J}\nu_j\le h-p.
  \label{eq:vertex-budget-raw}
\end{equation}
Moreover, the paths
\begin{equation}
  R_i:=
  \begin{cases}
    T[u_i,v_i], & i\in I_1,\\
    T[u_i,w_i]w_iv_i, & i\in I_2,\\
    \{v_i\}, & i\in I_3,
  \end{cases}
  \label{eq:R-paths}
\end{equation}
are pairwise vertex-disjoint and satisfy
$V(R_i)\cap V(P)=\{v_i\}$.  In particular, the representatives
$u_1,\dots,u_p$ are pairwise distinct and $|U|=p$.
\end{proposition}

\begin{proof}
For $i\in I_1$, the path $Q'_i$ lies in the subtree rooted at the chosen
off-path child $z_i$.  Such subtrees are disjoint for distinct indices in
$I_1$: at a vertex $v_i$ of the root path, the off-path child subtree is
disjoint from the child subtree containing the remainder of $P$ and hence
from every branch rooted later on $P$.

For distinct $i,j\in I_2$, the vertices $w_i,w_j$ are incomparable, so their
descendant subtrees, and therefore $Q'_i,Q'_j$, are disjoint.  Finally, an
$I_2$ tail cannot meet an $I_1$ tail.  If
$T[w_j,u_j]$ met $T[z_i,u_i]$, then the tree order would make $w_j$
comparable with the leaf $u_i\in U_1$, contrary to (R2)(i).  Thus all
$Q'_j$ are pairwise disjoint.  They are nonempty by construction and are
contained in $H-P$, proving \eqref{eq:vertex-budget-raw}.

For $i\in I_1$, the off-path vertex set of $R_i$ is $V(Q'_i)$.  For
$i\in I_2$, the path $R_i$ consists of the off-path tail $Q'_i$ followed by
the final edge $w_iv_i$; its off-path vertex set is again $V(Q'_i)$.  A
descendant of an off-path vertex cannot meet $P$, because every root path to
a vertex of $P$ is an initial segment of $P$.  The established tail
disjointness and the distinct endpoints $v_i$ therefore make the paths in
\eqref{eq:R-paths} pairwise vertex-disjoint, and each meets $P$ only at
$v_i$.  Their initial vertices $u_i$ are consequently distinct.
\end{proof}

\begin{proposition}[Neighborhood localization]\label{prop:dfs-neighborhood}
For every $i\in I_3$,
\begin{equation}
  N_H(v_i)\subseteq V(P)\cup
  \bigcup_{j\in J}V(\widehat Q_j).
  \label{eq:localization}
\end{equation}
\end{proposition}

\begin{proof}
Take $z\in N_H(v_i)\setminus V(P)$.  By DFS comparability, $v_i<_Tz$.
If $z\in U_1$, then $z=u_a\in V(\widehat Q_a)$ for some $a\in I_1$.
Assume henceforth that $z\notin U_1$.

If $z$ were incomparable with every vertex of $U_1\cup W$, then the pair
$(i,z)$ could be added to the selection in (R2), contradicting the maximality
of $|I_2|$.  Hence $z$ is comparable with some vertex of $U_1\cup W$.

If $z$ is comparable with a leaf $u_a\in U_1$, then $z=u_a$ or $z$ is an
ancestor of $u_a$; since $z\notin P$, it lies in $\widehat Q_a$.  Otherwise
$z$ is comparable with some $w_j\in W$.  If $z\le_Tw_j$, including equality,
then $z$ lies on the off-path root segment of $Q_j$ and hence in
$\widehat Q_j$.  The only remaining possibility is $w_j<_Tz$.  There is at most one such
selected $w_j$, because two selected ancestors of $z$ would lie on the same
root path and hence be comparable, contrary to (R2)(i).  Since $i\in I_3$,
we have $i\notin I_1$, and by construction
$z\in N_H(v_i)\setminus(V(P)\cup U_1)$; hence $(i,z)$ is an eligible pair
for (R2).  Replace the selected pair $(j,w_j)$ by $(i,z)$.  Every other
member of $U_1\cup W$ remains incomparable with $z$ by
Lemma~\ref{lem:tree-separation}(ii), because it was incomparable with the
ancestor $w_j$; in particular, $z$ is distinct from every remaining
selected vertex.  The cardinality is unchanged, while one selected depth is
replaced by a strictly larger depth.  By
Lemma~\ref{lem:tree-separation}(iii), the nondecreasing depth sequence is
lexicographically larger.  This contradicts (R2)(iii).  Therefore $z$ belongs to one of the
$\widehat Q_j$.
\end{proof}

For $j\in J$, define
\begin{equation}
  \beta_j:=d_H(u_j)+
  \sum_{i\in I_3}d_{\widehat Q_j}(v_i).
  \label{eq:beta}
\end{equation}
Proposition~\ref{prop:dfs-neighborhood} gives the degree decomposition
\begin{equation}
  \sum_{i=1}^p d_H(u_i)
  \le
  \sum_{i\in I_3}d_P(v_i)+\sum_{j\in J}\beta_j.
  \label{eq:dfs-decomp}
\end{equation}
Indeed, for $i\in I_3$ we have $u_i=v_i$, and every neighbor of $v_i$
outside $P$ is counted in at least one displayed incidence sum; possible
double counting only strengthens this upper bound.

The endpoints satisfy $1,p\in I_3$.  The endpoint observation preceding
(R1) gives $d_T(v_1)=d_T(v_p)=1$, so neither endpoint lies in $I_1$; and
neither has an off-path neighbor, so neither lies in $I_2$.  Consequently,
\begin{equation}
  u_1=v_1,
  \qquad
  u_p=v_p.
  \label{eq:end-representatives}
\end{equation}
In particular,
\begin{equation}
  J\subseteq\{2,\ldots,p-1\}.
  \label{eq:J-internal}
\end{equation}
Thus every branch index used below lies in the domain of the positional
allowance $\omega_j$.

\section{Path-position and branch estimates}\label{sec:branch}

Put $s:=c(H)$, with the convention $s=2$ when $H$ is a forest.  Since
an $s$-cycle contains a path on $s$ vertices, and since $p\ge3$ in the forest
case, one always has $p\ge s$.  For $2\le i\le p-1$, define
\begin{equation}
  \omega_i:=
  \min\{i-1,s-1\}+\min\{p-i,s-1\},
  \label{eq:omega}
\end{equation}
and put
\begin{equation}
  E_0:=\min\{p-1,2s-2\}.
  \label{eq:E0}
\end{equation}

\begin{lemma}[Path-position budget]\label{lem:path-budget}
We have
\begin{equation}
  d_P(v_1),d_P(v_p)\le s-1,
  \qquad
  d_P(v_1)+d_P(v_p)\le E_0,
  \label{eq:endpoint}
\end{equation}
and, for $2\le i\le p-1$,
\begin{equation}
  d_P(v_i)\le\omega_i.
  \label{eq:internal-position}
\end{equation}
Consequently, with
\begin{equation}
  B_0:=E_0+\sum_{i=2}^{p-1}\omega_i,
  \label{eq:B0def}
\end{equation}
one has
\begin{equation}
  B_0=E_0+(s-1)(2p-s-2)
  \label{eq:B0}
\end{equation}
and
\begin{equation}
  \sum_{i\in I_3}d_P(v_i)
  \le B_0-\sum_{j\in J}\omega_j.
  \label{eq:I3path}
\end{equation}
\end{lemma}

\begin{proof}
For an internal vertex $v_i$, let $N_i^-$ and $N_i^+$ be its neighbors to
the left and right on $P$.  If $|N_i^-|\le1$, then $|N_i^-|\le s-1$ because
$s\ge2$.  If $|N_i^-|\ge2$ and $v_a$ is its leftmost member, then the
$|N_i^-|$ distinct neighbor positions lie on $P[v_a,v_{i-1}]$, so
$i-a\ge |N_i^-|$.  The edge $v_av_i$ together with $P[v_a,v_i]$ therefore
forms a genuine cycle of length $i-a+1\ge |N_i^-|+1$.  If $H$ is a forest,
this is impossible and hence $|N_i^-|\le1=s-1$; if $H$ is cyclic, the cycle
has length at most $s$, again giving $|N_i^-|\le s-1$.  Trivially
$|N_i^-|\le i-1$.  The same argument on the right gives
\[
  |N_i^+|\le\min\{p-i,s-1\},
\]
which proves \eqref{eq:internal-position}.  At an endpoint, if there is at
most one path-neighbor then the bound is immediate.  If there are at least
two, the farthest neighbor and the intervening segment of $P$ form a genuine
cycle; as above, this is impossible in a forest and has length at most $s$
in the cyclic case.  Hence $d_P(v_1),d_P(v_p)\le s-1$.

It remains to prove the endpoint-rotation inequality
\begin{equation}
  d_P(v_1)+d_P(v_p)\le p-1.
  \label{eq:endpoint-rotation}
\end{equation}
Set
\[
  A:=\{i\in[p-1]:v_1v_{i+1}\in E(H)\},
  \qquad
  B:=\{i\in[p-1]:v_iv_p\in E(H)\}.
\]
If $i\in A\cap B$, then
\[
  v_1v_{i+1}P[v_{i+1},v_p]v_iP[v_i,v_1]
\]
is a cycle through every vertex of $P$.  Since $P$ is not Hamiltonian and
$H$ is connected, let $X=x_0\cdots x_r$ be a shortest path from
$H-P$ to this spanning cycle, oriented so that $x_0\in H-P$ and $x_r$ lies
on the cycle.  By minimality, $x_0,\ldots,x_{r-1}$ lie outside the cycle.
Delete either cycle edge incident with $x_r$, traverse $X$ from $x_0$ to
$x_r$, and then traverse the remaining spanning path of the cycle.  This is
a simple path containing all $p$ vertices of $P$ and at least the additional
vertex $x_0$, contradicting the maximality of $P$.
Hence $A\cap B=\varnothing$, and since both are subsets of $[p-1]$,
\eqref{eq:endpoint-rotation} follows.  Combining it with the two individual
circumference caps gives \eqref{eq:endpoint}.

Because $p\ge s$, direct summation of the two truncated ramps in
\eqref{eq:omega} gives
\[
  \sum_{i=2}^{p-1}\omega_i=(s-1)(2p-s-2),
\]
which is \eqref{eq:B0}.  Finally $1,p\in I_3$, and
$[p]=I_3\mathbin{\dot\cup}J$, so subtracting the positional allowances of the
indices in $J$ gives \eqref{eq:I3path}.
\end{proof}

For $j\in J$, set
\[
  P_j:=P[v_1,v_{\ell_j}],
  \qquad
  Y_j:=\{y\in V(P_j)\setminus\{v_{\ell_j}\}:
               N_{\widehat Q_j}(y)\ne\varnothing\}.
\]
If $j\in I_2$, then $j<\ell_j$, $w_j\in\widehat Q_j$, and
$v_jw_j\in E(H)$; hence
\begin{equation}
  v_j\in Y_j
  \qquad (j\in I_2).
  \label{eq:I2-in-Y}
\end{equation}
The incidence-cover and replacement-path estimates in the next lemma adapt
the proof of \cite[Lemma~5.6, equations~(12)--(19)]{MNZ2026}.  They are
reorganized here to isolate the root and circumference budgets used by the
new position-sensitive argument.

\begin{lemma}[Exact branch accounting]\label{lem:exact-branch}
For every $j\in J$,
\begin{equation}
  \beta_j\le \ell_j+|Q_j|-2\le p-2,
  \label{eq:root-branch}
\end{equation}
and
\begin{equation}
  \beta_j\le2s-2.
  \label{eq:circ-branch}
\end{equation}
If $Y_j\ne\varnothing$, then also
\begin{equation}
  \beta_j\le s+|Q_j|-2.
  \label{eq:core-Q-bound}
\end{equation}
If $Y_j=\varnothing$, the stronger bound $\beta_j\le s-1$ holds.
\end{lemma}

\begin{proof}
Fix $j\in J$.  List
\[
  Y_j=\{y_1,\dots,y_m\}
\]
in order from $v_1$ toward $v_{\ell_j}$, and put
\[
  a_r:=d_{\widehat Q_j}(y_r)
  \qquad(1\le r\le m).
\]

\medskip\noindent\emph{Incidence cover.}
We first justify
\begin{equation}
  \sum_{i\in I_3}d_{\widehat Q_j}(v_i)
  \le\sum_{r=1}^m a_r.
  \label{eq:incidence-cover}
\end{equation}
If $v_i$, $i\in I_3$, has a neighbor $z$ on $\widehat Q_j$, DFS
comparability makes $v_i$ and $z$ comparable.  The off-path vertex $z$ cannot
be an ancestor of $v_i$, because every ancestor of $v_i$ lies on the initial
root path $P$.  Hence $v_i$ lies on the root path to $z$, and therefore on
$P_j$.  Moreover,
$i\ne\ell_j$: for $j\in I_1$ one has $\ell_j=j\notin I_3$, while for
$j\in I_2$ Proposition~\ref{prop:I2-geometry} gives $\ell_j\in I_1$.
Thus $v_i\in Y_j$, proving \eqref{eq:incidence-cover}.

By Lemma~\ref{lem:dfs-comparability}, every graph-neighbor of $u_j$ is
comparable with $u_j$.  Because $u_j$ is a rooted DFS leaf, it has no proper
descendant, so every such neighbor is an ancestor.  If $d_H(u_j)\ge2$, take
its shallowest and deepest neighbors on the ancestor chain.  Their tree distance is at least $d_H(u_j)-1$, and together with
the two incident edges to $u_j$ they form a cycle of length at least
$d_H(u_j)+1$.  Hence, also in the trivial cases $d_H(u_j)\le1$,
\begin{equation}
  d_H(u_j)\le s-1.
  \label{eq:leafdeg}
\end{equation}
The root path $T[v_1,u_j]$ has length
$(\ell_j-1)+|Q_j|\le p-1$, because $P$ is longest.  Therefore
\begin{equation}
  \ell_j+|Q_j|-2\le p-2.
  \label{eq:root-length}
\end{equation}

Suppose first that $Y_j=\varnothing$.  The incidence sum in
\eqref{eq:beta} is zero.  Also $u_jv_1\notin E(H)$, because the simple path
$u_jv_1P[v_1,v_p]$ would have length $p$ and hence would be longer than
$P$.  Every neighbor of $u_j$ lies on its ancestor chain, and therefore
\[
  N_H(u_j)\subseteq
  V(T[v_1,u_j])\setminus\{u_j,v_1\}.
\]
The set on the right has
$(\ell_j-1)+|Q_j|-1=\ell_j+|Q_j|-2$ vertices.  Hence
\[
  \beta_j=d_H(u_j)
  \le \ell_j+|Q_j|-2.
\]
This proves the first bound in \eqref{eq:root-branch}; the bound
$\beta_j\le s-1$ follows from \eqref{eq:leafdeg}.  In particular,
$\beta_j\le2s-2$, so all asserted bounds for the case $Y_j=\varnothing$
are established.

\medskip\noindent\emph{The root-path budget when $Y_j\ne\varnothing$.}
Now assume $Y_j\ne\varnothing$, so $m\ge1$.  For each
$1\le r<m$, independently choose
\[
  z_r^-\in N_{\widehat Q_j}(y_r),
  \qquad
  z_r^+\in N_{\widehat Q_j}(y_{r+1})
\]
so that $|\widehat Q_j[z_r^-,z_r^+]|$ is maximum for this particular pair
$(y_r,y_{r+1})$.  Lemma~\ref{lem:two-set-path} gives
\[
  |\widehat Q_j[z_r^-,z_r^+]|
  \ge \frac{a_r+a_{r+1}}2-1.
\]
If $z_r^-=z_r^+$, maximality of the distance forces both neighbor sets to
be that same singleton, and the route $y_rz_r^-y_{r+1}$ has length $2$.
Otherwise use
\[
  y_rz_r^-\,\widehat Q_j[z_r^-,z_r^+]\,z_r^+y_{r+1}.
\]
In either case this is a simple $y_r$--$y_{r+1}$ path of length at least
\[
  \frac{a_r+a_{r+1}}2+1.
\]
All its internal vertices lie in $\widehat Q_j\subseteq H-P$ by
\eqref{eq:Q-meets-P}.  Consequently, adjoining the retained segments
$P[v_1,y_r]$ and $P[y_{r+1},v_p]$ produces a simple path.  Replacing
$P[y_r,y_{r+1}]$ by this route would therefore make a longer path unless
\begin{equation}
  |P[y_r,y_{r+1}]|
  \ge\frac{a_r+a_{r+1}}2+1.
  \label{eq:consecutive}
\end{equation}
For the final segment, choose
$z_m^{\mathrm{end}}\in N_{\widehat Q_j}(y_m)$ farthest from
$v_{\ell_j}$ along $Q_j$.  The $a_m$ neighbor positions are distinct, so
\[
  y_mz_m^{\mathrm{end}}\,
  Q_j[z_m^{\mathrm{end}},v_{\ell_j}]
\]
has length at least $a_m+1$.  By \eqref{eq:Q-meets-P}, its internal
vertices lie outside $P$.  Replacing $P[y_m,v_{\ell_j}]$ in $P$ gives the
simple path
\[
  P[v_1,y_m]y_mz_m^{\mathrm{end}}
  Q_j[z_m^{\mathrm{end}},v_{\ell_j}]P[v_{\ell_j},v_p].
\]
Longestness of $P$ therefore implies
\begin{equation}
  |P[y_m,v_{\ell_j}]|\ge a_m+1.
  \label{eq:last-segment}
\end{equation}
Because $u_j\in V(\widehat Q_j)$, every neighbor of $u_j$ on $P_j$ belongs to
$Y_j\cup\{v_{\ell_j}\}$, whence
\begin{equation}
  d_{P_j}(u_j)\le m+1.
  \label{eq:Pj-degree}
\end{equation}
If $m\ge2$, summing \eqref{eq:consecutive} and
\eqref{eq:last-segment} yields
\[
\begin{aligned}
  a_1+|P[y_1,v_{\ell_j}]|
  &\ge \sum_{r=1}^m a_r
       +m+\frac{a_1+a_m}{2}\\
  &\ge \sum_{r=1}^m a_r+m+1.
\end{aligned}
\]
If $m=1$, then $a_1\ge1$ because $y_1\in Y_j$, and
\eqref{eq:last-segment} gives
$a_1+|P[y_1,v_{\ell_j}]|\ge2a_1+1\ge a_1+2$.
Together with \eqref{eq:Pj-degree}, both cases give
\begin{equation}
  a_1+|P[y_1,v_{\ell_j}]|
  \ge \sum_{r=1}^m a_r+d_{P_j}(u_j).
  \label{eq:mnz18}
\end{equation}

For the root-path budget, choose
$z_1^{\mathrm{root}}\in N_{\widehat Q_j}(y_1)$ farthest from $u_j$
along $Q_j$.  Among $a_1$ distinct positions, the farthest is at tree
distance at least $a_1-1$ from $u_j$.  The segment
$Q_j[u_j,z_1^{\mathrm{root}}]$ is contained in $\widehat Q_j$ and hence is
disjoint from $P$.  Therefore
\[
  u_jQ_j[u_j,z_1^{\mathrm{root}}]z_1^{\mathrm{root}}y_1P[y_1,v_p]
\]
is a simple path whose initial off-path portion has length at least $a_1$.
Maximality of $P$ therefore gives
\begin{equation}
  |P[v_1,y_1]|\ge a_1.
  \label{eq:mnz19}
\end{equation}
Combining \eqref{eq:mnz19} with \eqref{eq:mnz18}, and using
\[
  |P_j|=|P[v_1,y_1]|+|P[y_1,v_{\ell_j}]|,
\]
yields
\begin{equation}
  |P_j|\ge \sum_{r=1}^m a_r+d_{P_j}(u_j).
  \label{eq:Pj-budget}
\end{equation}
Every neighbor of the DFS leaf $u_j$ is on its ancestor chain, which is the
union of $P_j$ and $Q_j$.  For clarity, write
\[
  d_{H-P_j}(u_j):=|N_H(u_j)\setminus V(P_j)|.
\]
After removing $P_j$, the only possible neighbors are the vertices in
$V(Q_j)\setminus\{v_{\ell_j},u_j\}$, a set of cardinality $|Q_j|-1$.
Thus
\begin{equation}
  d_{H-P_j}(u_j)\le|Q_j|-1.
  \label{eq:outside-Pj}
\end{equation}
Using \eqref{eq:incidence-cover}, \eqref{eq:Pj-budget}, and
\eqref{eq:outside-Pj},
\[
\begin{aligned}
  \beta_j
  &\le d_{H-P_j}(u_j)+d_{P_j}(u_j)+\sum_{r=1}^m a_r\\
  &\le |Q_j|-1+|P_j|\\
  &=\ell_j+|Q_j|-2.
\end{aligned}
\]
Together with \eqref{eq:root-length}, this completes
\eqref{eq:root-branch}.

\medskip\noindent\emph{The circumference budget.}
It remains to obtain the circumference-sensitive bounds.  First observe that
$H$ cannot be a forest when $Y_j\ne\varnothing$.  If
$yz\in E(H)$ with $y\in P_j\setminus\{v_{\ell_j}\}$ and
$z\in\widehat Q_j$, then $y$ precedes $v_{\ell_j}$ on $P$, whereas the last
vertex of $P$ on the root path to $z$ is $v_{\ell_j}$.  Hence $yz$ is not a
tree edge, and $yz$ together with the tree path between its endpoints forms
a genuine cycle.  Thus the ordinary circumference $s$ applies.
Choose
$z_1^\star\in N_{\widehat Q_j}(y_1)$ farthest from $v_{\ell_j}$ on
$Q_j$.  The cycle
\[
  y_1z_1^\star Q_j[z_1^\star,v_{\ell_j}]P[v_{\ell_j},y_1]
\]
is simple by \eqref{eq:Q-meets-P}; its branch segment has length at least
$a_1$.  Thus the cycle has length at least
\[
  a_1+|P[y_1,v_{\ell_j}]|+1.
\]
Hence
\begin{equation}
  a_1+|P[y_1,v_{\ell_j}]|\le s-1.
  \label{eq:cycle-upper}
\end{equation}
Combining \eqref{eq:cycle-upper} with \eqref{eq:mnz18} gives
\begin{equation}
  d_{P_j}(u_j)+\sum_{r=1}^m a_r\le s-1.
  \label{eq:branch-core}
\end{equation}
Since $d_{P_j}(u_j)\ge0$, \eqref{eq:branch-core} also gives
\begin{equation}
  \sum_{r=1}^m a_r\le s-1.
  \label{eq:incidence-circ}
\end{equation}
Equations \eqref{eq:incidence-cover}, \eqref{eq:outside-Pj}, and
\eqref{eq:branch-core} imply
\[
  \beta_j\le s+|Q_j|-2,
\]
which is \eqref{eq:core-Q-bound}.  Finally,
\eqref{eq:incidence-cover}, \eqref{eq:leafdeg}, and
\eqref{eq:incidence-circ} imply $\beta_j\le2s-2$.
\end{proof}

\begin{lemma}[Branch-position bound]\label{lem:branch-position}
For every $j\in J$,
\begin{equation}
  \beta_j\le
  \gamma_j:=
  \min\{p-2,\,2s-2,\,s+2j-5,\,p+s-j-2\}.
  \label{eq:gamma}
\end{equation}
\end{lemma}

\begin{proof}
The first two entries follow from Lemma~\ref{lem:exact-branch}.  We prove the
two positional entries.

Suppose first that $j\in I_1$.  Then $\ell_j=j$, and
\eqref{eq:root-branch} gives
\begin{equation}
  \beta_j\le j+|Q_j|-2.
  \label{eq:I1exact}
\end{equation}
The path $u_jQ_jv_jP[v_j,v_p]$ is simple and has length
$|Q_j|+p-j$.  Since $P$ is longest, $|Q_j|\le j-1$, and therefore
\begin{equation}
  \beta_j\le2j-3\le s+2j-5.
  \label{eq:I1position}
\end{equation}

Now suppose $j\in I_2$.  By Proposition~\ref{prop:I2-geometry},
$\ell_j>j$.  Put
\[
  r_j:=\ell_j,
  \qquad
  A_j:=|T[v_{r_j},w_j]|,
  \qquad
  B_j:=|T[w_j,u_j]|.
\]
The tree segment $T[w_j,v_{r_j}]$ meets $P$ only at $v_{r_j}$.  Moreover,
$v_jw_j$ is not a tree edge: since $j\notin I_1$, the internal tree vertex
$v_j$ has the unique child $v_{j+1}$, whereas $w_j\notin P$.  The tree
segment and the segment of $P$ meet only at $v_{r_j}$, and $w_j$ is off
$P$.  Hence
\[
  v_jw_j\,T[w_j,v_{r_j}]\,P[v_{r_j},v_j]
\]
is a simple cycle of length $1+A_j+(r_j-j)$.  In particular, the existence
of an $I_2$ branch already excludes the forest case; in the present case the
cycle has length at most the ordinary circumference $s$.  Therefore
\begin{equation}
  r_j+A_j\le s+j-1.
  \label{eq:rA}
\end{equation}
Likewise $T[u_j,w_j]$ lies wholly off $P$, so
\[
  u_jT[u_j,w_j]w_jv_jP[v_j,v_p]
\]
is a simple path of length $B_j+1+p-j$.  Longestness of $P$ gives
\begin{equation}
  B_j\le j-2.
  \label{eq:Bj}
\end{equation}
Since $|Q_j|=A_j+B_j$, the exact root estimate gives
\begin{equation}
  \beta_j\le r_j+A_j+B_j-2.
  \label{eq:I2exact}
\end{equation}
Combining \eqref{eq:rA} and \eqref{eq:Bj} yields
\begin{equation}
  \beta_j\le s+2j-5.
  \label{eq:I2position}
\end{equation}

For the second positional bound, if $Y_j=\varnothing$ then
$\beta_j\le s-1\le p+s-j-2$ because $j\le p-1$.  If
$Y_j\ne\varnothing$, Lemma~\ref{lem:exact-branch} gives
\[
  \beta_j\le s+|Q_j|-2.
\]
The root-path inequality
$(\ell_j-1)+|Q_j|\le p-1$ and $\ell_j\ge j$ imply
$|Q_j|\le p-j$, and hence $\beta_j\le p+s-j-2$.
\end{proof}

\section{The refined vertex budget}\label{sec:vertex-budget}

Put
\begin{equation}
  \rho:=p-s,
  \qquad
  \mu:=\min\{\rho,s\},
  \qquad
  \mathcal R:=\{j:4\le j\le\mu-1\}.
  \label{eq:R}
\end{equation}
The set $\mathcal R$ is the only index interval in which the common
branch-position bound can exceed the allowance $\omega_j$.

\begin{lemma}[Location and type of possible positive excess]\label{lem:positive-location}
For every $j\in J\setminus\mathcal R$,
\begin{equation}
  \beta_j\le\omega_j.
  \label{eq:no-excess}
\end{equation}
Moreover, the same inequality holds for every $j\in I_1$, including
$j\in\mathcal R$.  Hence positive excess is possible only for
\begin{equation}
  \mathcal S:=I_2\cap\mathcal R.
  \label{eq:S}
\end{equation}
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:branch-position}, it suffices first to compare $\gamma_j$
with $\omega_j$.  If $j\le\mu$, then $j\le s$ and $j\le p-s$, so
\[
  \omega_j=s+j-2.
\]
Subtracting this quantity from the four entries in \eqref{eq:gamma} gives
\[
  \rho-j,
  \qquad
  s-j,
  \qquad
  j-3,
  \qquad
  s+\rho-2j.
\]
The fourth is the sum of the first two nonnegative terms.  Therefore
\begin{equation}
  \gamma_j-\omega_j
  =\min\{\mu-j,j-3\}.
  \label{eq:mountain}
\end{equation}
This is positive exactly when $4\le j\le\mu-1$.

It remains to consider $j>\mu$.  If $j>\rho=p-s$, then $p-j\le s-1$.
When $j\le s+1$, direct substitution gives $\omega_j\ge p-2$, so
$\gamma_j\le\omega_j$.  When $j\ge s+2$, one has
\[
  p+s-j-2=\omega_j-1,
\]
and again $\gamma_j\le\omega_j$.  The only remaining possibility is
$j>s$ while $j\le\rho$; then both terms in \eqref{eq:omega} are saturated and
\[
  \omega_j=2s-2,
\]
one of the entries in \eqref{eq:gamma}.  This proves
\eqref{eq:no-excess}.

Finally let $j\in I_1\cap\mathcal R$.  By
\eqref{eq:I1position}, $\beta_j\le2j-3$.  Since
$j\le\mu-1\le s-1$ and $\omega_j=s+j-2$,
\[
  \beta_j-\omega_j
  \le j-s-1\le-2.
\]
Thus no $I_1$ branch has positive excess.
\end{proof}


\begin{lemma}[Refined vertex-budget lemma]\label{lem:vertex-budget}
Under the hypotheses of Sections~\ref{sec:dfs-construction}--\ref{sec:branch},
\begin{equation}
  \boxed{\displaystyle
  \sum_{i=1}^p d_H(u_i)\le (s-1)(2p-s)+h-p.}
  \label{eq:vertex-budget}
\end{equation}
\end{lemma}

\begin{proof}
Let $\mathcal S=I_2\cap\mathcal R$.  If $j\in\mathcal S$, then
$j\le\mu$, so $\omega_j=s+j-2$.  Retain the notation
$r_j,A_j,B_j$ from the proof of Lemma~\ref{lem:branch-position}.  Here
$B_j=|T[w_j,u_j]|$ is an edge-length, whereas
$\nu_j=|V(Q'_j)|$ is a vertex count.  Since
$Q'_j=T[w_j,u_j]$, we have
\begin{equation}
  \nu_j=B_j+1.
  \label{eq:nu-I2}
\end{equation}
Equations~\eqref{eq:rA} and~\eqref{eq:I2exact} give
\[
  \beta_j\le s+j+B_j-3,
\]
and hence
\begin{equation}
  \beta_j-\omega_j\le B_j-1=\nu_j-2.
  \label{eq:charge-I2}
\end{equation}
By Lemma~\ref{lem:positive-location}, every branch outside $\mathcal S$ has
nonpositive excess.  The tails $Q'_j$, $j\in\mathcal S$, are pairwise
disjoint subsets of $H-P$, so Proposition~\ref{prop:dfs-linkage} gives
\begin{equation}
  \sum_{j\in\mathcal S}\nu_j\le h-p.
  \label{eq:S-tail-budget}
\end{equation}
Therefore
\begin{equation}
\begin{aligned}
  \sum_{j\in J}(\beta_j-\omega_j)
  &\le\sum_{j\in\mathcal S}(\nu_j-2)\\
  &\le h-p-2|\mathcal S|.
\end{aligned}
  \label{eq:total-charge}
\end{equation}
Neither the individual quantities $\nu_j-2$ nor the resulting upper bound
need be nonnegative; no nonnegativity is used.
Combining \eqref{eq:dfs-decomp}, \eqref{eq:I3path}, and
\eqref{eq:total-charge},
\[
\begin{aligned}
  \sum_{i=1}^p d_H(u_i)
  &\le B_0-\sum_{j\in J}\omega_j+\sum_{j\in J}\beta_j\\
  &\le B_0+h-p-2|\mathcal S|.
\end{aligned}
\]
Finally \(E_0\le2s-2\), so
\[
  B_0=E_0+(s-1)(2p-s-2)\le(s-1)(2p-s),
\]
which proves~\eqref{eq:vertex-budget}.
\end{proof}

\begin{remark}[Disjoint-tail charge and unused reserve]
The paths $Q_j$ may share root prefixes.  No such prefix is charged in
Lemma~\ref{lem:vertex-budget}; only the pairwise disjoint tails $Q'_j$ enter
\eqref{eq:total-charge}.  The argument does not require an example with
positive excess, or even that $\mathcal S$ be nonempty.  Membership in
$\mathcal S$ identifies only where the common upper bound could exceed the
positional allowance; it does not assert that the actual excess is positive.
In fact, before the last uniformization the proof establishes the stronger
auxiliary estimate
\[
  \sum_{i=1}^p d_H(u_i)\le B_0+h-p-2|\mathcal S|.
\]
The theorem-facing form agrees with the uniform allowance sum used by the
formal cycle-to-path core.  Its decisive feature is the coefficient-one term \(+h\),
which cancels against the term \(h\) in \(n\ge h+|C|\).
\end{remark}

\section{A self-contained local small-path theorem}\label{sec:local-theorem}

The following coarse consequence of the DFS construction is useful
independently of the final residual-cap core.  It corresponds to
the coarse representative estimate in \cite[Lemma~5.6(i)]{MNZ2026}, but is
proved here from the present construction.

\begin{lemma}[Coarse DFS degree sum]\label{lem:coarse-dfs}
Let $H$ be connected and let $P=v_1\cdots v_p$ be a non-Hamiltonian longest
path, where $p\ge3$.  For the representatives constructed in
(R1)--(R3),
\begin{equation}
  \sum_{i=1}^p d_H(u_i)\le p(p-2).
  \label{eq:coarse-dfs}
\end{equation}
\end{lemma}

\begin{proof}
Lemma~\ref{lem:exact-branch} gives $\beta_j\le p-2$ for every $j\in J$.
Put $m:=|I_3|$.  The endpoints lie in $I_3$, so $m\ge2$.  Also
$J\ne\varnothing$: if $I_1\ne\varnothing$ this is immediate; if $I_1$ is empty,
connectedness and $H-P\ne\varnothing$ provide an edge from an internal
$v_i$ to $H-P$, and the corresponding singleton is a feasible choice in
(R2).  Thus $m\le p-1$.

By the endpoint-rotation part of Lemma~\ref{lem:path-budget},
$d_P(v_1)+d_P(v_p)\le p-1$, while every other path vertex has path-degree at
most $p-1$.  Hence
\[
\begin{aligned}
  \sum_{i\in I_3}d_P(v_i)
  &\le (m-1)(p-1)\\
  &\le m(p-2),
\end{aligned}
\]
where the last inequality is equivalent to $m\le p-1$.  Now
\eqref{eq:dfs-decomp} gives
\[
\begin{aligned}
  \sum_{i=1}^p d_H(u_i)
  &\le m(p-2)+|J|(p-2)\\
  &=p(p-2).
\end{aligned}
\]
\end{proof}

The next theorem is an independent local form of
\cite[Theorem~6.1]{MNZ2026} with the local $q$-connectivity hypothesis
deleted.  The included proof uses only the coarse estimate just established
and local longestness of $C$ with respect to $H$.

\begin{theorem}[Local small-path bound]\label{thm:local-small-path}
Let $q\ge3$, let $C$ be a cycle of a graph $G$, and let $H$ be a component
of $G-V(C)$ such that $C$ is locally longest with respect to $H$.  Put
$\delta_H:=\delta_G(H)$ and $p:=p(H)$.  If
\[
  q-1\le p\le\delta_H-q+1,
\]
then
\begin{equation}
  |C|\ge q(\delta_H-q+2).
  \label{eq:local-small-path}
\end{equation}
\end{theorem}

\begin{proof}
Let $P=v_1\cdots v_p$ be a longest path of $H$, and set
\[
  f(z):=z(\delta_H+2-z).
\]
The hypothesis gives
\[
  q\le p+1\le\delta_H-q+2.
\]
The concave quadratic $f$ has equal values
\[
  f(q)=f(\delta_H-q+2)=q(\delta_H-q+2),
\]
so
\begin{equation}
  f(p+1)\ge q(\delta_H-q+2).
  \label{eq:f-concave}
\end{equation}

Suppose first that $P$ is Hamiltonian in $H$.  Enumerate
$U=V(H)$ as $u_i:=v_i$ along $P$, and take $R_i:=\{v_i\}$ for every $i$
in Lemma~\ref{lem:attachment}.  Each vertex of $H$ has at
most $p-1$ neighbors in $H$, so
\[
  e(U,C)\ge p(\delta_H-p+1).
\]
For any $u\in U$,
$d_C(u)\ge\delta_H-p+1\ge q$, and hence
$|N_C(U)|\ge\delta_H-p+1\ge2$.  Therefore
\[
  |C|\ge(p+1)(\delta_H-p+1)=f(p+1).
\]

Now suppose that $P$ is non-Hamiltonian.  Then $p\ge3$: otherwise $p=2$,
but a connected graph with at least three vertices contains a path on three
vertices, while a connected graph of order two is traced by $P$.  Hence
Lemma~\ref{lem:coarse-dfs} and representative injectivity give
\[
  e(U,C)
  =\sum_{i=1}^p\bigl(d_G(u_i)-d_H(u_i)\bigr)
  \ge p(\delta_H-p+2).
\]
A vertex of $C$ is adjacent to at most the $p$ distinct representatives, so
\[
  |N_C(U)|\ge\frac{e(U,C)}p\ge\delta_H-p+2\ge q+1.
\]
The linkage from Proposition~\ref{prop:dfs-linkage} permits application of
Lemma~\ref{lem:attachment}, and hence
\[
  |C|\ge(p+1)(\delta_H-p+2)>f(p+1).
\]
In both cases, \eqref{eq:f-concave} proves \eqref{eq:local-small-path}.
\end{proof}


\section{The cycle-to-path core}\label{sec:cycle-to-path-core}

We first isolate the cycle-to-path implication.  This is the point at which
the detailed DFS work above enters the final proof.

\begin{lemma}[Uniform representative budget]\label{lem:uniform-representative}
Let \(H\) be a connected graph of order \(h\), let
\(P=v_1\cdots v_p\) be a longest path of \(H\), and suppose \(2\le s\le p\)
and every ordinary cycle contained in \(H\) has order at most \(s\).  There
are distinct representatives \(u_1,\ldots,u_p\), with \(u_1=v_1\), and
pairwise disjoint \((u_i,v_i)\)-paths meeting \(P\) only at \(v_i\), such
that
\begin{equation}
  p+\sum_{i=1}^{p}d_H(u_i)
  \le (s-1)(2p-s)+h.
  \label{eq:uniform-representative}
\end{equation}
The same statement is valid for a forest with the convention \(s=2\).
\end{lemma}

\begin{proof}
If \(P\) is Hamiltonian, take \(u_i=v_i\) and the trivial linkage paths.
For each position, the neighbors to its left and right are bounded by the
two truncated distances
\(\min\{i-1,s-1\}\) and \(\min\{p-i,s-1\}\): otherwise the farthest
neighbor and the intervening part of \(P\) form a cycle longer than \(s\)
(and in the forest case even one such chord is impossible).  Summing these
pointwise bounds gives
\[
  \sum_{i=1}^{p}d_H(v_i)\le (s-1)(2p-s),
\]
and \(h=p\).

If \(P\) is non-Hamiltonian, then \(p\ge3\): otherwise connectedness and a
vertex outside \(P\) would extend a longest path of order at most two.  Use
the representatives and linkage paths from
Proposition~\ref{prop:dfs-linkage}.  Lemma~\ref{lem:vertex-budget} gives
\[
  \sum_{i=1}^{p}d_H(u_i)\le(s-1)(2p-s)+h-p.
\]
Adding \(p\) proves~\eqref{eq:uniform-representative}.
\end{proof}

\begin{theorem}[Cycle-to-path core]\label{thm:cycle-to-path-core}
Let \(q,x\in\mathbb Z_{\ge0}\), and suppose
\begin{equation}
  d_G(v)\ge q+1+x\quad(v\in V(G)),
  \qquad
  n+2\le(q+2)(x+2).
  \label{eq:core-hypotheses}
\end{equation}
If a longest cycle \(C\) has residual cap \(\min\{q,x\}\), then every path
in \(G-V(C)\) has order at most \(q\).
\end{theorem}

\begin{proof}
Suppose that a residual path \(P_0\) has order at least \(q+1\), let \(H\)
be its component in \(G-V(C)\), and choose a longest path
\(P=v_1\cdots v_p\) of \(H\).  Put
\[
  s:=\min\{q,x\}.
\]
The generalized residual cap and the edges or vertices of \(P_0\) force
\(s\ge2\).  Write
\[
  s=\sigma+1,\qquad q=s+b,\qquad x=s+a,\qquad
  p=q+1+t=s+\rho,
\]
where \(a,b,t\ge0\) and \(\rho=b+t+1\).  Every ordinary cycle in \(H\) has
order at most \(s\), so Lemma~\ref{lem:uniform-representative} supplies a
linked representative family \(U=\{u_1,\ldots,u_p\}\) with
\begin{equation}
  p+\sum_i d_H(u_i)\le B+h,
  \qquad
  B:=\sigma(p+\rho).
  \label{eq:core-budget}
\end{equation}

The endpoint \(v_1=u_1\) has no neighbor in \(H-P\), and its path-position
degree is at most \(\sigma=s-1\).  Hence, with
\[
  \delta_0:=q+1+x,\qquad d:=q+a+2,
\]
we have \(d_C(u_1)\ge d\).  In particular,
\(|N_C(U)|\ge d\ge2\).  Global longestness of \(C\) makes it locally
longest with respect to \(H\), so Lemma~\ref{lem:attachment} gives
\begin{equation}
  e(U,C)+d\le |C|.
  \label{eq:core-attachment}
\end{equation}
Summing the degree floor over the distinct representatives gives
\begin{equation}
  p\delta_0\le\sum_i d_H(u_i)+e(U,C).
  \label{eq:core-degree}
\end{equation}
Since \(H\) and \(C\) are vertex-disjoint, \(h+|C|\le n\).  Combining
\eqref{eq:core-budget}--\eqref{eq:core-degree} yields
\begin{equation}
  p+p\delta_0+d\le B+n.
  \label{eq:core-upper}
\end{equation}

Let \(M:=(q+2)(x+2)\).  Direct expansion using the displayed parameter
equalities gives the exact identity
\begin{equation}
  p+p\delta_0+d
  =
  M+B+2+b(b+t+4)+t(a+4).
  \label{eq:core-identity}
\end{equation}
Thus \(M+B+2\le B+n\), whereas~\eqref{eq:core-hypotheses} says
\(n+2\le M\), an impossibility.  This proves the theorem.
\end{proof}

\section{Cycle extension in the middle residual range}
\label{sec:cycle-extension}

The residual-cap proof needs the following exact cycle-extension inequality.

\begin{theorem}[Cycle extension with positive surplus]\label{thm:cycle-extension}
Let \(C\) be a longest cycle and let \(R\) be a maximum generalized residual
cycle of order \(c\ge2\).  If \(d\ge1\) and
\[
  d_G(v)\ge c+d\qquad(v\in V(G)),
\]
then
\begin{equation}
  (c+1)(d+1)\le |C|.
  \label{eq:cycle-extension}
\end{equation}
\end{theorem}

\begin{proof}
Choose a degree-maximal linkage to a generalized residual cycle of maximum
order.
For residual order two, the two linkage routes and the residual edge
give the required replacement cycles.  For residual order at least three,
pass to its cyclic carrier and let \(Z\) be the set of confined positions
whose representative degree is above the ordinary carrier allowance.  There
are three exhaustive cases: \(Z=\varnothing\), \(|Z|=1\), and
\(|Z|\ge2\).  In each case the relevant linkage routes and carrier arcs are
spliced into external bridges, longestness bounds those bridges by the
corresponding arcs of \(C\), and the resulting incidence inequalities sum to
\eqref{eq:cycle-extension}.  The constructions include all
endpoint-coincidence and generalized-order-two boundaries.

The formalization checks these four exhaustive cases separately and combines
them in a single dispatcher.  Section~\ref{sec:formal-certification} records
their exact declaration correspondence.  Every case constructs its paths and
cycles and proves their support and order inequalities in Lean; none is an
assumed theorem-valued input.
\end{proof}

The instance \(d\ge2\) is the middle cycle-extension theorem used below.
The positive form is needed at the exact residual boundary.  We also use the
following connectivity-two consequence of Dirac's circumference bound.

\begin{lemma}[Connectivity-two residual bound]\label{lem:connectivity-two-high}
Let \(C\) be a longest cycle of a \(2\)-connected graph \(G\).  Suppose
\(d_G(v)\ge y+2\) for every vertex, and a maximum generalized residual cycle
has order \(c\ge y+1\).  Then
\[
  2(y+2)\le |C|.
\]
\end{lemma}

\begin{proof}
Dirac's circumference theorem gives
\[
  \min\{n,2(y+2)\}\le |C|.
\]
If the first term realizes the minimum, then
\(n\le |C|\), contradicting the packing
\(|C|+c\le n\) because \(c\ge1\).  Hence the second term is at most
\(|C|\).
\end{proof}

\begin{corollary}[Exact residual boundary]\label{cor:exact-boundary}
Let \(C\) be a longest cycle of \(G\), and let \(1\le r\le y\).  Suppose
\(G\) is \((r+1)\)-connected,
\(d_G(v)\ge(r+1)+y\) for every vertex, and the maximum residual order is
\(c=y+1\).  Then
\begin{equation}
  (r+1)(y+2)\le |C|.
  \label{eq:exact-boundary}
\end{equation}
\end{corollary}

\begin{proof}
Choose a generalized residual cycle of maximum order and apply
Theorem~\ref{thm:cycle-extension} with residual order \(c=y+1\) and surplus
\(d=r\).
\end{proof}

\section{The strictly high residual range}
\label{sec:strict-high}

The remaining residual range is not closed by quoting a standalone
size-free theorem.  Instead we keep the global order hypothesis and use the
following formally verified linkage package.  We state precisely the
numerical interface used in the proof; the underlying paths, supports, and
normalizations are all constructed in the companion formalization.

\begin{lemma}[High-residual linkage package]
\label{lem:high-residual-linkage}
Let \(m\ge3\), let \(C\) be a longest cycle, and let a maximum residual
generalized cycle have order
\[
  h=y+1+e=m+q,
  \qquad e\ge1,\qquad e\le q.
\]
Suppose \(G\) is \(m\)-connected and
\(d_G(v)\ge m+y\) for every vertex.  There are nonnegative integers
\(S,\Pi,X,A,\Delta\) and a linkage-support set
\(\mathcal L\subseteq V(G-C)\) such that
\begin{align}
  S+h&\le|\mathcal L|,                                      \label{eq:linkage-support}\\
  h(m+y)&\le S+\Pi+X,                                      \label{eq:linkage-degree}\\
  \Pi+\Delta&=h(h-1),                                      \label{eq:linkage-defect}\\
  X+A&\le|C|.                                              \label{eq:linkage-attachment}
\end{align}
Moreover, whenever
\begin{equation}
  |C|+S+e+1\le m(y+2),
  \label{eq:linkage-paid-premise}
\end{equation}
there is an external connector of length \(\ell\) satisfying
\begin{align}
  \ell&\le y-1,                                            \label{eq:connector-short}\\
  (e+1)(h-2)&\le\Delta.                                    \label{eq:connector-sharp}
\end{align}
\end{lemma}

\begin{proof}[Construction and proof outline]
The parameter assumptions give \(h=m+q\ge4\), which is the exact carrier
order needed by the four-exception cyclic summation below.
Choose a minimum path linkage from every position of a cyclic carrier for
the maximum residual witness.  The special positions are the confined
moving representatives.  Their integer charges \(\phi\) sum to \(S\);
the complementary charges \(\gamma\) sum to \(\Pi\).
\(X\) is the total number of incidences between these linkage
representatives and \(C\), while \(A\) is the cardinality of the union of
their attachment positions on \(C\).
Pairwise disjoint route supports contain one carrier-root vertex at every
carrier position, and confinement identifies \(\phi\) with degree along the
corresponding route.  This gives~\eqref{eq:linkage-support}.  Summing the
representative degree partition and the exact identity separating special
and complementary charge gives~\eqref{eq:linkage-degree}.  The pointwise
bound \(\gamma+1\le h\) defines the nonnegative complement \(\Delta\) in
\eqref{eq:linkage-defect}.  Applying the linked-set attachment inequality to
the same representatives gives~\eqref{eq:linkage-attachment}; in particular,
\(X\) and \(A\) refer to the same physical linkage.

Connectivity supplies a complete generic external family with \(m\)
canonical gaps.  If \(\ell_i\) denotes its chosen external-connector length,
the one-cycle gap ledger is
\[
  2m+\sum_{i=1}^{m}\ell_i\le |C|.
\]
Together with~\eqref{eq:linkage-paid-premise}, positivity of \(S+e+1\) shows
that some \(\ell_i\le y-1\), proving~\eqref{eq:connector-short}.

For that connector, let \(x,z\) be its two distinct carrier roots, put
\(H_0=h-1\), and define the cyclic edge weights
\[
  \beta_i=\gamma_i+\gamma_{i+1}.
\]
On an edge incident with \(x\) or \(z\), the complete cyclic-neighbor
projection bounds one endpoint by \(\ell\) and the other by \(H_0\).
Away from both roots, the nonincident projection gives
\(\beta_i\le2\ell\le H_0+\ell\).  The overlap-safe four-exception sum is
therefore
\begin{equation}
  2\Pi\le4H_0+2(h-2)\ell.
  \label{eq:connector-beta-sum}
\end{equation}
Since~\eqref{eq:connector-short} and \(h=y+1+e\) give
\(\ell+e+1\le H_0\), equation~\eqref{eq:connector-beta-sum} implies
\[
\begin{aligned}
  2\bigl(\Pi+(e+1)(h-2)\bigr)
  &\le 4H_0+2(h-2)\ell+2(h-2)(H_0-\ell)\\
  &=2hH_0,
\end{aligned}
\]
and hence \(\Pi+(e+1)(h-2)\le hH_0\).
Using~\eqref{eq:linkage-defect} yields~\eqref{eq:connector-sharp}.
Every path concatenation and every endpoint-coincidence boundary in this
argument is included in the checked declaration cited in
Section~\ref{sec:formal-certification}.
\end{proof}

\begin{proposition}[Strict high-range exclusion]\label{prop:strict-high}
Let \(C\) be a longest cycle of \(G\).  Let \(1\le r\le y\), put \(m=r+1\),
and suppose
\begin{align}
  &G\text{ is }m\text{-connected},                         \label{eq:strict-high-conn}\\
  &d_G(v)\ge m+y\quad(v\in V(G)),                           \label{eq:strict-high-deg}\\
  &n+2\le(m+1)(y+2).                                      \label{eq:strict-high-size}
\end{align}
Then
\[
  \cbar(G-C)\le y+1.
\]
\end{proposition}

\begin{proof}
Suppose instead that a generalized residual cycle of maximum order has
order \(c\ge y+2\).  Packing gives \(|C|+c\le n\).  If \(m=2\),
Lemma~\ref{lem:connectivity-two-high} gives
\(2(y+2)\le|C|\), while packing and~\eqref{eq:strict-high-size} give
\(|C|+2\le2(y+2)\), a contradiction.  Hence \(m\ge3\).

Write
\[
  c=y+1+e=m+q,
\]
where \(e\ge1\).  Since \(m\le y+1\), we also have \(e\le q\).  Apply
Lemma~\ref{lem:high-residual-linkage} with \(h=c\).  The linkage support is disjoint
from \(C\), so~\eqref{eq:linkage-support} and
\(|C|+|\mathcal L|\le n\), followed by~\eqref{eq:strict-high-size}, give
\begin{equation}
  |C|+S+e+1\le m(y+2).
  \label{eq:paid}
\end{equation}
The package therefore supplies its short connector and sharp defect.

Combining~\eqref{eq:linkage-degree}--\eqref{eq:linkage-attachment} with
\eqref{eq:paid} uses the exact identity
\begin{equation}
  h(h-1)+m(y+2)=h(m+y)+(m+e\,q),
  \label{eq:strict-high-core-identity}
\end{equation}
and yields the attachment-free core inequality
\begin{equation}
  \Delta+A+e+1\le m+e\,q.
  \label{eq:attachment-free-core}
\end{equation}
Indeed, add \(\Delta+A+e+1\) to the degree inequality, regroup as
\((\Pi+\Delta)+(X+A)+(S+e+1)\), and then use
\eqref{eq:linkage-defect}, \eqref{eq:linkage-attachment},
\eqref{eq:paid}, and~\eqref{eq:strict-high-core-identity}.

Finally insert~\eqref{eq:connector-sharp} into~\eqref{eq:attachment-free-core}:
\[
  (e+1)(h-2)+A+e+1\le m+e\,q.
\]
Since \(h=m+q\), cancellation gives
\begin{equation}
  em+q+A\le e+1.
  \label{eq:terminal-impossible}
\end{equation}
But \(m\ge3\), \(q\ge e\ge1\), and \(A\ge0\), so the left side is at
least \(4e>e+1\), a contradiction.
\end{proof}

\begin{remark}
The global size hypothesis is used in~\eqref{eq:paid}.  Removing it also
removes the full payment of \(S+e+1\).  Proposition~\ref{prop:strict-high}
therefore does not prove the stronger standalone Jung-type high-residual
bound.
\end{remark}

\section{Residual-cap assembly}\label{sec:residual-cap}

We now prove the cap required by Theorem~\ref{thm:cycle-to-path-core}.

\begin{theorem}[Residual cap under the product bound]
\label{thm:residual-cap}
Let \(q,x\in\mathbb Z_{\ge0}\), put
\[
  r:=\min\{q,x\},\qquad y:=\max\{q,x\},
\]
and suppose
\begin{align}
  &G\text{ is }(q+1)\text{-connected},                    \label{eq:cap-connectivity}\\
  &d_G(v)\ge q+1+x\quad(v\in V(G)),                        \label{eq:cap-degree}\\
  &n+2\le(q+2)(x+2).                                      \label{eq:cap-size}
\end{align}
Then every longest cycle \(C\) has residual cap \(r\).
\end{theorem}

\begin{proof}
The min--max identities are
\begin{equation}
  (r+1)+y=q+1+x,
  \qquad
  (r+2)(y+2)=(q+2)(x+2).
  \label{eq:minmax}
\end{equation}
Thus \(G\) is \((r+1)\)-connected, the degree floor is
\((r+1)+y\), and \(n+2\le(r+2)(y+2)\).

If \(G-V(C)\) is empty there is nothing to prove.  If \(r=0\), the
min--max identities give
\[
  \delta(G)\ge y+1,\qquad n+2\le2(y+2),
\]
and hence \(2\delta(G)\ge n\).  Since the ordinary cycle \(C\) exists,
\(n\ge3\), so Dirac's theorem makes \(G\) Hamiltonian,
so the longest cycle \(C\) spans \(G\).  This is the generalized
residual-cap-zero case.
Assume henceforth that \(r\ge1\), let \(c\) be the maximum generalized
residual order, and suppose \(c\ge r+1\).

If \(c\le y\), write
\[
  c=r+1+u,\qquad y=c+t,\qquad d=r+t+1
\]
with \(u,t\ge0\).  Then \(c+d=(r+1)+y\), and
Theorem~\ref{thm:cycle-extension} gives
\[
  (c+1)(d+1)\le|C|.
\]
The exact identity
\begin{equation}
  (r+2)(y+2)+u(t+1)=(c+1)(d+1)+c+1
  \label{eq:middle-identity}
\end{equation}
contradicts both \(n+2\le(r+2)(y+2)\) and
\(|C|+c\le n\).

If \(c=y+1\), Corollary~\ref{cor:exact-boundary} gives
\[
  (r+1)(y+2)\le|C|.
\]
Together with \(c=y+1\), residual packing, and
\[
  (r+2)(y+2)=(r+1)(y+2)+(y+2),
\]
this contradicts \(n+2\le(r+2)(y+2)\).

Finally, if \(c\ge y+2\), Proposition~\ref{prop:strict-high} applies and
gives a contradiction.  Hence \(c\le r\), which is exactly residual cap
\(r\).
\end{proof}

\section{Proof of Theorem~\ref{thm:bondy}}\label{sec:main-proof}

\begin{proof}[Proof of Theorem~\ref{thm:bondy}]
Connectivity gives \(k\le\delta(G)\).  Write
\[
  k=q+1,\qquad \delta(G)=q+1+x
\]
with \(q,x\ge0\).  The degree hypothesis in Theorem~\ref{thm:bondy} is the
integer inequality
\[
  n+(q+1)q\le(q+2)(q+1+x).
\]
Rearranging gives
\begin{equation}
  n+2\le(q+2)(x+2).
  \label{eq:product-bridge}
\end{equation}
Theorem~\ref{thm:residual-cap} supplies residual cap
\(\min\{q,x\}\) for the arbitrary longest cycle \(C\).  The cycle-to-path
core, Theorem~\ref{thm:cycle-to-path-core}, now shows that every path
disjoint from \(C\)
has order at most \(q=k-1\), equivalently fewer than \(k\) vertices.
\end{proof}

\section{Formal certification and correspondence}
\label{sec:formal-certification}

The accompanying Lean~4 development, implemented in Lean~4
\cite{Lean4} with Mathlib \cite{Mathlib2020}, uses the exact
finite-simple-graph
formulation
\[
\begin{split}
 &1\le k,\quad G\text{ is \(k\)-connected},\\
 &|V(G)|+k(k-1)\le(k+1)\delta(G)
\end{split}
\quad\Longrightarrow\quad
 \operatorname{ord}(P)<k
\]
for every path \(P\) whose support is disjoint from the support of an
arbitrary longest cycle \(C\).  Minimum degree is defined totally, so no
extra nonempty-type premise is hidden.  Generalized residual witnesses of
orders one and two are part of the formal definitions, not informal
boundary conventions added afterward.
Here \texttt{VertexConnectedAtLeast G k} means \(k<|V(G)|\) and that
deleting every set of fewer than \(k\) vertices leaves a connected induced
subgraph.  A \leanname{VPath} has injective vertex positions and consecutive
adjacencies, its order is its number of positions, and a \leanname{VCycle}
is such a path of order at least three with a closing edge.
\texttt{IsLongestCycle G C} universally compares \(C\)'s order with every
such ordinary cycle.  Thus the formal notions agree with the graph-theoretic
ones in Theorem~\ref{thm:bondy}; in particular, the strict conclusion
\(P.\mathrm{order}<k\) is exactly ``at most \(k-1\) vertices.''
The cycle argument itself supplies \(|V(G)|\ge3\), so the explicit
\(n\ge3\) convention in the paper statement is not a missing formal premise.
The formalization environment pins Lean
\leanname{v4.30.0-rc2} and Mathlib revision
\leanname{5450b53e5ddc75d46418fabb605edbf36bd0beb6}.

\begingroup
\small
\setlength{\LTpre}{\smallskipamount}
\setlength{\LTpost}{\smallskipamount}
\begin{longtable}{@{}>{\raggedright\arraybackslash}p{0.34\textwidth}
  >{\raggedright\arraybackslash}p{0.58\textwidth}@{}}
\toprule
Paper item & Lean declaration \\
\midrule
\endfirsthead
\toprule
Paper item & Lean declaration \\
\midrule
\endhead
\midrule
\multicolumn{2}{r@{}}{\scriptsize Continued on next page} \\
\endfoot
\bottomrule
\endlastfoot
Uniform representative budget (non-Hamiltonian branch) &
\leanname{Bondy.linkedRepresentatives_degreeBudget} \\
Linked attachment &
\leanname{Bondy.linked_attachment_statement},
\leanname{Bondy.linked_attachment_total} \\
Cycle-to-path core &
\leanname{Bondy.bondy_core_cap} \\
Residual-cap-zero Dirac boundary &
\leanname{Bondy.diracResidualCapZero} \\
Cycle extension: residual order two &
\leanname{Bondy.cycleExtensionN_of_witness_order_two} \\
Cycle extension: no exceptional position &
\leanname{Bondy.cycleExtensionN_of_highConfinedPos_empty} \\
Cycle extension: one exceptional position &
\leanname{Bondy.cycleExtensionN_of_highConfinedPos_card_eq_one} \\
Cycle extension: at least two exceptional positions &
\leanname{Bondy.cycleExtensionN_of_two_highConfined} \\
Positive-surplus cycle extension &
\leanname{Bondy.cycleExtensionNPositive} \\
Middle cycle extension &
\leanname{Bondy.cycleExtensionNMiddle} \\
Connectivity-two residual bound &
\leanname{Bondy.residualHighCycleBound_of_connectivity_two} \\
Exact residual boundary &
\leanname{Bondy.residualHighCycleBound_of_order_eq_y_add_one} \\
Special support payment &
\leanname{Bondy.PathLinkage.specialPhi_add_carrierOrder_le_linkageSupport_card} \\
Attachment-free core inequality &
\leanname{Bondy.positiveHigh_rawCore} \\
Short connector &
\leanname{Bondy.PathLinkage.exists_short_generic_chosenPlainConnector} \\
Sharp connector defect &
\leanname{Bondy.PathLinkage.repairedThetaGammaDefect_ge_mul_carrier_sub_two_of_shortConnector} \\
Strict high-range exclusion &
\leanname{Bondy.no_positiveHigh_residualCircumferenceData_of_globalSize} \\
Residual-cap assembly &
\leanname{Bondy.bondyResidualCap} \\
Final theorem &
\leanname{Bondy.bondy_longest_cycle} \\
\end{longtable}
\endgroup

Public information about the proof and its formal verification is available
at:
\begin{center}
\begin{minipage}{0.94\textwidth}
\small\raggedright
Proof information:\quad
\url{https://www.proofatlas.ai/research/bondy-longest-cycle-proof/}\\
Formal source revision:\quad
\leanname{9e13b044d8821b587935fa3019d913699eadffa2}
\end{minipage}
\end{center}
A clean-start build and audit were completed at the displayed revision.  The
audit verified the source and compiled artifacts for all 204 project modules
in the final dependency cone, reran the exact intermediate and final type
checks, performed a scoped source scan, and checked the transitive axioms of
all twenty distinct formal declarations named in this paper.  The exact
commands and audit outputs are recorded in the accompanying formal-verification
artifact.  This claim concerns the final dependency cone, not exploratory
modules outside it.
There is no \texttt{sorry}, \texttt{admit}, project mathematical axiom,
theorem-valued premise, or unverified mathematical import in that dependency
cone.  The transitive axiom report for the final theorem contains
only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}.

The formal theorem proved here is the global-size Bondy statement.  Neither
the paper nor the formalization claims the stronger standalone size-free
high-residual bound.

\appendix
\section{Algebraic expansions}\label{app:algebra}

For the cycle-to-path core, put
\[
  s=\sigma+1,\quad q=s+b,\quad x=s+a,\quad
  p=q+1+t=s+\rho,\quad \rho=b+t+1,
\]
and set
\[
  \delta_0=q+1+x,\quad d=q+a+2,\quad
  B=\sigma(p+\rho),\quad M=(q+2)(x+2).
\]
Then direct expansion gives
\[
  p+p\delta_0+d
  =M+B+2+b(b+t+4)+t(a+4).
\]

For the residual split, with
\[
  r=\min\{q,x\},\qquad y=\max\{q,x\},
\]
one has
\[
  (r+1)+y=q+1+x,\qquad
  (r+2)(y+2)=(q+2)(x+2).
\]
If \(c=r+1+u\), \(y=c+t\), and \(d=r+t+1\), then
\[
  (r+2)(y+2)+u(t+1)=(c+1)(d+1)+c+1.
\]

Finally, in the strictly high branch
\[
  h=m+q=y+1+e
\]
implies
\[
  h(h-1)+m(y+2)=h(m+y)+(m+e\,q).
\]
Substituting the sharp defect into the attachment-free core inequality gives
\[
\begin{aligned}
 &(e+1)(h-2)+A+e+1\le m+e\,q\\
 &\hspace{35mm}\Longleftrightarrow\quad em+q+A\le e+1.
\end{aligned}
\]
The source-to-product bridge used in the final line is
\[
  n+(q+1)q\le(q+2)(q+1+x)
  \quad\Longrightarrow\quad
  n+2\le(q+2)(x+2).
\]

\begin{thebibliography}{99}

\bibitem{Bondy1980}
J.~A. Bondy,
\newblock \emph{Longest paths and cycles in graphs of high degree},
\newblock Research Report CORR 80-16, Department of Combinatorics and
Optimization, University of Waterloo, 1980.

\bibitem{Dirac1952}
G.~A. Dirac,
\newblock Some theorems on abstract graphs,
\newblock \emph{Proceedings of the London Mathematical Society} (3)
\textbf{2} (1952), 69--81,
\newblock doi:10.1112/plms/s3-2.1.69.

\bibitem{Diestel2017}
R.~Diestel,
\newblock \emph{Graph Theory}, 5th ed.,
\newblock Graduate Texts in Mathematics 173, Springer, 2017,
\newblock doi:10.1007/978-3-662-53622-3.

\bibitem{EG1959}
P.~Erd\H{o}s and T.~Gallai,
\newblock On maximal paths and circuits of graphs,
\newblock \emph{Acta Math. Acad. Sci. Hungar.} \textbf{10} (1959), 337--356,
\newblock doi:10.1007/BF02024498.

\bibitem{Lean4}
L.~de Moura and S.~Ullrich,
\newblock The Lean 4 theorem prover and programming language,
\newblock in \emph{Automated Deduction---CADE 28},
Lecture Notes in Computer Science 12699, Springer, 2021, pp.~625--635,
\newblock doi:10.1007/978-3-030-79876-5\_37.

\bibitem{MNZ2026}
J.~Ma, B.~Ning, and Z.~Zhao,
\newblock Longest cycles and Dirac-type results in highly connected graphs,
\newblock arXiv:2606.03696v1 [math.CO], June 2026,
\newblock \url{https://arxiv.org/abs/2606.03696}.

\bibitem{Mathlib2020}
The Mathlib Community,
\newblock The Lean mathematical library,
\newblock in \emph{Proceedings of the 9th ACM SIGPLAN International
Conference on Certified Programs and Proofs}, ACM, 2020, pp.~367--381,
\newblock doi:10.1145/3372885.3373824.

\bibitem{NashWilliams1971}
C.~St.~J.~A. Nash-Williams,
\newblock Edge-disjoint Hamiltonian circuits in graphs with vertices of large
valency,
\newblock in \emph{Studies in Pure Mathematics} (L.~Mirsky, ed.),
\newblock Academic Press, London, 1971, pp.~157--183.

\bibitem{Nikoghosyan2009}
Zh.~G. Nikoghosyan,
\newblock Dirac-type generalizations concerning large cycles in graphs,
\newblock \emph{Discrete Mathematics} \textbf{309} (2009), 1925--1930,
\newblock doi:10.1016/j.disc.2008.03.011.

\bibitem{Nikoghosyan2023}
Z.~Nikoghosyan,
\newblock A note on large cycles in graphs around conjectures of Bondy and Jung,
\newblock \emph{Mathematical Problems of Computer Science} \textbf{59} (2023),
7--15; arXiv:2211.16446,
\newblock doi:10.51408/1963-0097.

\end{thebibliography}

\end{document}