\section{A preliminary bound and restriction of the parameter domain}
\label{sec:base-certificate}
We first combine only the original and neutral-core counts. Their
quadratic bounds give both the preliminary estimate $23/53$ and a
quantitative restriction on the parameters of any instance that could
exceed the final bound. All parameter restrictions in this section
therefore use inequalities valid before the additional matching
constructions are invoked.
Write
\[
 f=y^2+x^2/4+z^2/2+w^2,\quad B_0=1-f-b^2,
 \quad m=x/2-b,
\]
where $x+y+z+w=1$ and all coordinates are nonnegative.

\subsection{Entry into the dense region}
If $E\ge9m^2/50$, completing the square gives
\[
 \frac{x^2}{4}+b^2+\frac9{50}(x/2-b)^2
 =\frac{17x^2}{59}+\frac{59}{50}(b-9x/118)^2.
\]
Weighted Cauchy--Schwarz consequently bounds the original count by
\[
 C_0\le1-y^2-\frac{17x^2}{59}-\frac{z^2}{2}-w^2+o(1)
 \le\frac{110}{127}+o(1).
\]
Indeed the reciprocals of the four coefficients sum to $127/17$.
This handles the entire nondense region.

Otherwise the packing construction gives an actual core with
\[
 r^2\ge m^2-2E-o(1)\ge\frac{16}{25}m^2-o(1),
 \qquad E\ge\frac{m^2-r^2}{2}-o(1).
\]
The maximum core fixed in Section~\ref{sec:neutral-core} is at least
as large as the core used to establish these inequalities, so both
remain valid for its size $r$.
For a positive working count threshold $2G$, the original inequality
also gives a fixed positive lower bound for $m$ whenever $C_0>2G$.
In fact
\[
 1-f=\frac78-Q,\quad
 Q=(y-1/8)^2+(x-1/2)^2/4+(z-1/4)^2/2+(w-1/8)^2,
\]
and
\[
 \frac{(m-1/4)^2}{2}\le Q+b^2<7/8-2G+o(1).
\]
Thus
\begin{equation}\label{eq:base-m-entry}
 m\ge\frac14-\sqrt{2(7/8-2G)}-o(1).
\end{equation}
For every final threshold used below the right side exceeds $1/9$.
In particular $r\ge4m/5-o(1)$, and $m/2\le r\le m$ for all
sufficiently large $M$. A fixed positive bound such as $1/9$ suffices;
no stronger lower bound for $m$ is assumed.

The other initial absorption conditions follow just as directly.
Minimizing $f$ on the indicated halfspaces gives
\[
 y\ge4w\ \Longrightarrow\ f\ge17/127,
 \qquad
 x\ge16w\ \Longrightarrow\ f\ge65/484.
\]
For the first calculation the active boundary is $y=4w$, and the
remaining $x,z$ contribution is at least $(1-5w)^2/6$; minimizing
$17w^2+(1-5w)^2/6$ gives $17/127$.
For the second boundary $x=16w$, minimize
$65w^2+(1-17w)^2/3$, obtaining $65/484$.
Hence $y<4w$ and $x<16w$ whenever the original count exceeds a
threshold satisfying
\begin{equation}\label{eq:base-entry-thresholds}
 2G>\max\{110/127,\ 1-17/127,\ 1-65/484\}.
\end{equation}
These inequalities are checked exactly for the final value of $G$.
They also hold for $G=23/53$.

\subsection{The two comparison quadratics}
Let $S=e_{14}+e_{23}+e_{24}$. The five-edge replacement at the end of
Section~\ref{sec:core-derivation}, retaining the terms $h_1,h_3$, gives
\[
 h_1+h_3\ge
 \frac{[(2yw-e_{14})(rz-e_{23})-2zy e_{24}]_+}
      {\max(2zw,2yw-e_{14})}-o(1).
\]
Put $D_*=\max(2zw,2yw)$. Increasing the denominator and discarding
the favorable product $e_{14}e_{23}$ shows that this is at least
\[
 r\min(y,z)-\frac{rz}{D_*}e_{14}
       -\frac{2yw}{D_*}e_{23}-\frac{2zy}{D_*}e_{24}-o(1).
\]
The inequality remains valid if its untruncated right side is negative.
The entry conditions give
\[
 \frac{rz}{D_*}\le\frac{r}{2w}\le\frac{x}{4w}<4,
 \qquad\frac{2yw}{D_*}\le1,\qquad
 \frac{2zy}{D_*}\le\frac yw<4.
\]
Zero-denominator cases are either excluded by the original-count
threshold or handled by assigning penalty zero. Consequently
$h_1+h_3\ge r\min(y,z)-4S-o(1)$.

Define
\[
 A=B_0-\frac{m^2-r^2}{2},\qquad
 B_*=B_0+r(x+z-2y)-3r^2-r\min(y,z).
\]
The original and core counts obey
\[
 C_0\le A-S+o(1),\qquad C_r\le B_*+3S+o(1).
\]
Here unused nonpositive deficits have simply been discarded. Taking
weights $4/5,1/5$ leaves the nonpositive term $-S/5$.

For $V=(x,y,z,w,b,r)^T$ and $\ell=(1,1,1,1,0,0)^T$, define symmetric
matrices by their diagonal and upper-triangular nonzero off-diagonal
entries; all unspecified entries are zero:
\[
\begin{array}{c|c|l}
 &\text{diagonal}&\text{off-diagonal entries}\\ \hline
 H_0&(3/8,1,1/2,1,3/2,-1/2)&(H_0)_{xb}=-1/4\\
 H_y&(1/4,1,1/2,1,1,3)&
 (H_y)_{xr}=-1/2,\ (H_y)_{yr}=3/2,\ (H_y)_{zr}=-1/2\\
 H_z&(1/4,1,1/2,1,1,3)&
 (H_z)_{xr}=-1/2,\ (H_z)_{yr}=1
\end{array}
\]
Then $A=1-V^TH_0V$, while $B_*=1-V^TH_yV$ on $y\le z$ and
$B_*=1-V^TH_zV$ on $z\le y$.
Let
\[
 c_0=(1/2,0,0,0,-1,-1)^T,\qquad
 s_0=(-1/2,0,0,0,1,2)^T,\qquad
 N_0=(c_0s_0^T+s_0c_0^T)/2.
\]
Its quadratic form is $(m-r)(2r-m)\ge0$. The exact identities needed
for the bound are
\begin{align}
 \mathcal A&=\tfrac45H_0+\tfrac15H_y
       -\tfrac7{53}\ell\ell^T-\tfrac15N_0\succeq0,
       \label{eq:base-matrix-y}\\
 \mathcal Z&=\tfrac45H_0+\tfrac15H_z
       -\tfrac7{53}\ell\ell^T\succ0.
       \label{eq:base-matrix-z}
\end{align}
Their exact rational $LDL^T$ pivots are respectively
\[
 \left(\frac{71}{265},\frac{57}{71},\frac{29}{114},
 \frac{15}{29},\frac{17}{20},0\right),\qquad
 \left(\frac{231}{1060},\frac{26}{33},\frac3{13},
 \frac5{12},\frac{29}{35},\frac{74}{725}\right).
\]
The zero pivot has zero remaining Schur-complement column. Thus no
numerical eigenvalue test is involved. These identities prove
\[
 \min(C_0,C_r)\le46/53+o(1),\qquad \gamma(4)\le23/53.
\]
All matrix entries and decompositions are reconstructed by
\path{previous_certificate.py}.

\subsection{Coercivity and exact halfspace losses}
The matrix $\mathcal A$ has rank five and kernel spanned by
\[
 V_*=(26,4,16,7,3,10)^T/53,
 \qquad \ell^TV_*=1.
\]
The kernel claim follows either by multiplication or from the displayed
pivots and $\mathcal AV_*=0$. On the mass hyperplane we therefore have
\begin{equation}\label{eq:base-coercivity}
 \min(C_0,C_r)\le\frac{46}{53}
 -(V-V_*)^T\mathcal A(V-V_*)
 -\frac15(m-r)(2r-m)+o(1).
\end{equation}
The quadratic form is strictly positive away from $V_*$ on that
hyperplane. An explicit coordinate matrix makes every localization
check reproducible. Let $W$ have columns
$e_x-e_w,e_y-e_w,e_z-e_w,e_b,e_r$. Then
\[
 K_0=W^T\mathcal AW=
 \begin{pmatrix}
 7/5&1&1&-3/10&-1/4\\
 1&2&1&0&3/10\\
 1&1&3/2&0&-1/10\\
 -3/10&0&0&8/5&3/10\\
 -1/4&3/10&-1/10&3/10&3/5
 \end{pmatrix}\succ0.
\]
For a retained linear condition $f(V)=f(V_*)+a_f^T\eta\ge0$,
where $V-V_*=W\eta$ and $f(V_*)>0$, Cauchy--Schwarz in the $K_0$
inner product gives
\[
 f(V)\le0\quad\Longrightarrow\quad
 \eta^TK_0\eta\ge
 \frac{f(V_*)^2}{a_f^TK_0^{-1}a_f}.
\]
This is the exact count loss used for each halfspace exclusion.
The checker \path{localize.py} evaluates it with rational arithmetic.

The other branch has a convenient uniform loss: even
$\mathcal Z-(1/1000)\ell\ell^T$ is positive definite. Its exact
pivots are
\[
 \left(\frac{11497}{53000},\frac{180569}{229940},
 \frac{81827}{361138},\frac{32456}{81827},
 \frac{3201}{4057},\frac{62923}{640200}\right).
\]
Thus $z\le y$ gives count at most $46/53-1/1000+o(1)$.

Finally, when using \eqref{eq:base-coercivity} below at a target
$G<23/53$, repeat the original-count entry tests
\eqref{eq:base-m-entry}--\eqref{eq:base-entry-thresholds} with that
$G$. They justify density, $r\ge m/2$, and all absorption coefficients
without using the additional matching comparisons. The exact checker
then verifies that every excluded halfspace loss exceeds
$2(23/53-G)$, or replaces it by an explicitly stronger certificate.
This is the complete logical order of the localization.