\section{The supply of label-4 vertices and the imbalance of the two families}
\label{sec:top-capacity}
The reservoir construction matches retained $C$ vertices to the
original label-4 vertex set, whose mass is $2w$. When that set is
smaller than the retained set, a comparison that simply replaces
the matched mass by $r$ is not applicable. We first give a bound
that treats both possible relative sizes. It will also exclude
small values of $|d-q|$ before any lower bound on that imbalance
is assumed.

Write $H=h_3$ and $B_0=B-b^2$. The following comparison applies in
either orientation and uses only $r\le q$, which every neutral core
satisfies. It assumes neither $q\le2w$ nor a lower bound on the
mass of good $P$ vertices.
Put
\[
 h_0=\min(r,2w),\qquad D_0=\max(r,2w),
\]
and define the quadratic polynomial, separately on its two capacity
regions,
\[
 g(h_0)=h_0(3q/2-r-z+2y)-7h_0^2/8+q^2/2.
\]
A maximum label-3 matching between retained $C$ and the original
label-4 vertices covers target mass
\[
 t\ge h_0-e_{24}/D_0-o(1).
\]
This is the rectangular vertex-cover bound and applies regardless of
which side is larger. The exact outward caps of retained $C,D$ were
proved independently of top capacity.

The direct reservoir count, with the matched mass $t$ left
unspecified, gives
\[
\begin{split}
 C_T-C_0\le{}&t(3q/2-r-z+2y+3H/r)-7t^2/8+q^2/2\\
 &+2c+j+(2+t/r)a+e_{12}+e_{23}+e_{24}+e_{34}+o(1).
\end{split}
\]
For $0\le t\le r\le q$, the derivative of its part independent of
$H$ is at least $-5r/4-z$. Also $3tH/r\le3H$ and $t/r\le1$.
Adding the initial count and using this bound on the number of
unmatched target vertices proves
\begin{equation}\label{eq:top-limited-raw-reservoir}
\begin{split}
 C_T\le{}&B_0+g(h_0)+3H+2a+c-E_{AA}-e_{13}-e_{14}\\
 &+\frac{5r/4+z}{D_0}e_{24}+o(1).
\end{split}
\end{equation}
No $Z\ge3r/2$ hypothesis enters this comparison.

On the domain $r,w\ge1/10$ established from the initial quadratic
certificate, the coefficient of $e_{24}$ is at most $33/8$, and in particular at most $5$.
Indeed $x\ge2r$ and $x+y+z+w=1$ imply
$5r/4+z\le1-3r/4-w$. If $r\le2w$, the ratio is at most
$33/8$ by $r,w\ge1/10$; if $r\ge2w$, it is at most $15/4$.
The core estimate \eqref{eq:rawcore} is also valid here. On $y\le3z/8$ and $y\le w$
it is enough to retain its $-5H/8$ and to bound its possibly positive
$e_{14}$ coefficient by
\[
 (r/(2w)-1)_+\le3/2,
\]
using $r\le\min(d,q)\le1/2$ and $w\ge1/10$.

Let $p,b_R,b_T$ be nonnegative weights, summing to one, for the
initial count, the core count, and
\eqref{eq:top-limited-raw-reservoir}, respectively. It suffices to impose
\[
 \frac58b_R\ge3b_T,\qquad p\ge5b_T,\qquad
 p\ge2b_T,\qquad p+b_T\ge\frac32b_R.
\]
These absorb respectively $H,e_{24}$, the positive $a,c$ terms, and
$e_{14}$; all remaining cross-defect terms are nonpositive.
Writing $m=\min(d,q)$ and $K=(m^2-r^2)/2$, the packing estimate $E\ge K-o(1)$
then yields
\[
 C\le B_0+b_Rf_R+b_Tg(h_0)-(p-2b_T)K+o(1).
\]
This is a rational quadratic expression on each of the regions
$r\le2w$ and $r\ge2w$.

\paragraph{Small imbalance.}
Apply the same comparison to $0\le h\le3m/10$, where $h=|d-q|$.
Keep the actual $CD$ mass $q$ in $g(h_0)$, but use
$m=\min(d,q)$ in the packing term $K$. There are four cases: the
two orientations, each with $r\le2w$ or $r\ge2w$. In the former
case use $h_0=r$; in the latter use $h_0=2w$. Retain the same
conservative $3e_{14}/2$ core coefficient and the same defect budgets.
Four rational positive-definite matrices certify
\[
 \gamma(4)\le433403/1000000=0.433403
 \qquad(0\le h\le3m/10).
\]
The checker explicitly requires all four orientation/capacity cases.
It assumes neither $m\le2w$ nor $h\ge3m/10$. We therefore first
dispose of the small-imbalance region. The
comparison for $q\ge d\ge2w$ below can then use $h\ge3m/10$.
This order is essential because that comparison depends on a
positive lower bound for $h/m$.

In the case $d\ge q$, the two matrices in
\path{ab-boundary-certificate.json} prove
\[
 \gamma(4)\le433/1000
 \quad\text{when }d\ge q\ge2w
\]
on the shared localized domain. Its checker verifies the defect budgets,
positive definiteness by rational $LDL^T$, and the presence of both
capacity regions. This includes both relative sizes of $r$ and
$2w$ whenever
$q\ge2w$.

\paragraph{The larger-$CD$ orientation.}
The full surplus-target construction uses no top vertices. Its
assumption $d\le2w$ is needed only when discarding the rebuilt-core
term $(s/(2w)-1)e_{14}$ and the analogous initial-core term.
Since $s,r\le d\le1/2$ and $w\ge1/10$, retain at most
$3e_{14}/2$ in each core or full-target comparison. Bound this term
before the packing replacement $s\to d$; then every derivative and
resource-allocation argument for that replacement is unchanged.
All eligibility, matching-intersection, unsafe-vertex, and rich-row
arguments are independent of top capacity. Consequently the
full-target comparison is valid on $d\ge2w$
provided that its convex-combination weights obey the additional
inequality $p\ge3(b_R+b_D)/2$, where $p,b_R,b_D$ are the weights
of the initial, core, and full-target counts. The rational
eight-variable certificate in \path{cd-boundary-certificate.json}
gives
$\gamma(4)\le0.43301$ on this region. Together with the larger-$AB$
bound $0.433$, this excludes $m\ge2w$ in both orientations;
since $r\le m$, it also excludes $r\ge2w$.