\subsection{Using maximality of the joint choice of matchings}\label{sec:joint-maximality}
The core was chosen to have maximum size among all feasible joint
blue $AD$ and blue $CC$ matchings. Its maximality gives a second
relation between missing edges and blue edges leaving the retained set.
Write its retained mass as $r$,
let $a$ be the missing-blue $AD$ density, and let $c$ be the
missing-blue $CC$ density. Assume $d\ge q$ and $r>4q/5$. Define
\[
 u_0=a/d,\qquad K=(q^2-r^2)/2,
 \qquad E_{\rm pack}=c-K+qu_0-u_0^2/2.
\]
\begin{lemma}\label{lem:joint-packing-resource}
With uniform vanishing finite errors,
\begin{equation}\label{eq:joint-packing-resource}
 E_{\rm pack}\ge0,\qquad
 c_*\le \frac{E_{\rm pack}}{5-4q/r}+o(1),\qquad
 U\le ru_0+\frac{4(q-r)}{5r-4q}E_{\rm pack}+o(1).
\end{equation}
\end{lemma}
Here $c_*$ is the missing-blue density in the retained $C$ set and
$U$ its blue contact density to all omitted $C$.

\begin{proof}
Augment the core's blue $AD$ matching to a maximum
blue $AD$ matching. Its covered $D$ set contains the initial retained
set and has mass $t\ge q-a/d-o(1)$. Let $T$ be its original $C$ mates.
The initial retained $CC$ matching is maximum in $G[T]$: a larger
blue matching in $T$ would, together with the distinct $AD$ mates
already assigned to every member of $T$, give a larger feasible core.
Let $c_T$ count missing blue pairs in $T$, and let $s$ be a
Tutte--Berge barrier mass for this graph. The usual component argument
applied inside $T$ gives
\[
 0\le s\le r/2+o(1),\quad
 c_*\ge s(r-3s/2)-o(1)\ge rs/4-o(1),
\]
and the blue density from its unmatched set to its covered set is
at most $(t-r)s+o(1)$. Consequently
\[
 c_T\ge\frac{t^2-r^2}{2}+c_*-(t-r)s-o(1)
 \ge\frac{t^2-r^2}{2}+(5-4t/r)c_*-o(1).
\]
Since $c_T\le c$, $t\le q$, and $t\ge q-u_0-o(1)$, this proves
the claimed internal resource. The omitted $C$ outside $T$ have mass
at most $u_0+o(1)$ and give at most $ru_0+o(1)$ blue contacts.
The remaining omitted contacts are at most
$4(t-r)c_*/r+o(1)$. Substitution proves the external resource.

The maximum-core choice preserves all label restrictions and count
inequalities proved for arbitrary neutral cores, as well as the lower
bounds on $r$ in Section~\ref{sec:core-size}.
All auxiliary graphs have $O(M)$ vertices, so their finite errors are
uniform in the total number of original vertices.
\end{proof}

The same argument also gives inequalities retaining the barrier size.
For this purpose retain
an actual $u=q-t\in[0,u_0]$ and barrier mass $s\in[0,r/2]$ satisfying
\[
 c_*\ge s(r-3s/2),\qquad
 c_*\le c-K+qu-u^2/2+(q-u-r)s,
\]
\[
 U\le ru+(q-u-r)s.
\]
Thus
\[
 c-K+qu-u^2/2\ge s(2r-q+u-3s/2).
\]
In particular, at equality in the packing constraint,
$E_{\rm pack}=0$, the retained graph is blue complete and
$U\le ra/d$. Thus equality in this constraint restricts the blue
edges leaving the retained set as well as the edges inside it.