\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[margin=27mm]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,array}
\usepackage{xcolor}
\usepackage{microtype}
\usepackage[colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref}
\hypersetup{
 pdftitle={A computer-assisted proof of the four-uniform Erd\H{o}s matching conjecture},
 pdfauthor={Oleksiy Babanskyy},
 pdfsubject={Extremal combinatorics: the four-uniform matching conjecture},
 pdfkeywords={Erd\H{o}s matching conjecture, hypergraphs, exact certificates, shifting}
}
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{\small The four-uniform matching conjecture}
\fancyhead[R]{\small O. Babanskyy}
\fancyfoot[C]{\thepage}
\setlength{\headheight}{14pt}
\setlength{\emergencystretch}{2em}
\numberwithin{equation}{section}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\F}{\mathcal F}
\newcommand{\A}{\mathcal A}
\newcommand{\HH}{\mathcal H}
\newcommand{\BB}{\mathcal B}
\newcommand{\E}{\mathbb E}
\newcommand{\Var}{\operatorname{Var}}
\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
\newcommand{\ceil}[1]{\left\lceil#1\right\rceil}
\DeclareMathOperator{\HT}{HT}
\title{\vspace{-12mm}\textbf{A computer-assisted proof of the\\four-uniform Erd\H{o}s matching conjecture}}
\author{Oleksiy Babanskyy}
\date{}
\begin{document}
\maketitle
\begin{abstract}
We prove the Erd\H{o}s matching conjecture for four-uniform hypergraphs
for every matching parameter and every admissible number of vertices.
The proof combines the finite-board method of Hou, Hu and Liu with
ordered local configurations, exact integer counts and certified
inequalities. Small matching parameters are treated on full labelled
configurations. Two fixed counting inequalities and two endpoint anchors
propagate polynomially across the remaining range; 51 endpoint records
and the two fixed inequalities suffice for the intermediate cardinality
inputs. Dense triple supports admit direct slab and majority proofs. A classical shadow bound and a deletion argument complete
the passage from these local bounds to the global theorem.
The strict margins also yield clique stability with explicit constants
for shifted families whose matching number is preserved on deleting
the first vertex, and classifications of extremizers in specified ranges.
The finite parts are supported by exact certificates and exhaustive
computations with stated mathematical specifications.
\end{abstract}
\noindent\textbf{Keywords:} Erd\H{o}s matching conjecture; four-uniform
hypergraphs; exact certificates; shifting; extremal stability.


\section{The complete four-uniform bound}\label{sec:problem}
All vertex and matching parameters are integers.
A matching is a collection of pairwise disjoint sets. Write
\(\nu(\F)\) for the largest size of a matching in
\(\F\subseteq\binom{[n]}4\), and define
\[
 B_r(n,t)=\binom nr-\binom{n-t}r,\qquad A_4(s)=\binom{4s+3}4.
\]
For a \(t\)-set \(T\subseteq[n]\), the complete cover
\[
 \mathcal C_T(n)=\{E\in\binom{[n]}4:E\cap T\ne\varnothing\}
\]
has \(B_4(n,t)\) members and matching number at most \(t\).
Write \(\mathcal C_t=\mathcal C_{[t]}(n)\) when the ground set is clear.
The other candidate is the complete four-graph on \(4s+3\) vertices,
with all remaining vertices isolated.

\begin{theorem}[Four-uniform matching bound]\label{thm:global}
Let \(s\ge1\). For every \(n\ge4s+4\) and
\(\F\subseteq\binom{[n]}4\) with \(\nu(\F)\le s\),
\[
 |\F|\le M(n,s):=\max\{A_4(s),B_4(n,s)\}.
\]
For \(s\le4\), the classical shadow input in Section \ref{sec:imports}
and the small full-carrier certificates suffice.
\end{theorem}
The clique on \(4s+3\) vertices and the complete \(s\)-cover attain
the two terms. For \(n<4s+4\) the complete family has no forbidden
matching and gives the trivial extremal value \(\binom n4\).
The theorem concerns cardinality. Section \ref{sec:structural} identifies
the exact extremizers in explicit cover and clique domains and gives
quantitative clique stability for shifted ONE families. It does not
classify every crossing case or prove arbitrary-family stability.


\paragraph{Contribution and antecedents.}
Erd\H{o}s formulated the matching problem in \cite[equation (9)]{Erdos65}.
Frankl \cite{Frankl17} settled uniformity three; the short proof of
Frankl--R\"odl--Ruci\'nski \cite{FRR} covers matching number at least 33.
Hou--Hu--Liu \cite[Theorem 1.1]{HHL} prove the four-uniform bound for
\(s\ge6961\), using a finite-board reduction.
Theorem \ref{thm:global} extends that range to every positive \(s\).
Its ingredients retain local order in the trace constraints, couple
the resulting inequalities, and use integer orbit counts where a
continuous relaxation loses necessary information.
The board method, selected-residual construction and consumed HHL
programs remain attributed to that work.
The reduction to Property ONE and the deletion inequality have
antecedents in \cite[Proposition 5.1 and Corollary 5.1]{Frankl17}.

\paragraph{Notation and proof route.}
A family is \emph{shifted} if every four-set coordinatewise below one
of its members also belongs to it. It has \emph{Property ONE} if a
maximum matching avoids its first vertex. Put
\[
 a_s=n_4(s)=\min\{n\ge4s+4:B_4(n,s)\ge A_4(s)\}.
\]
For \(s\ge2\), the direct inputs are the two crossings \(a_s-1,a_s\).
Section \ref{sec:imports} proves that these inputs suffice, before
the finite configurations are analysed. Section \ref{app:global}
gives the trace reduction, an ordered board and the certificates for
the small and intermediate parameters.
Section \ref{app:range92} proves the necessary layer inequalities and
covers the infinite tail. The division of the critical inputs is
\[
\begin{array}{c|l}
s=1&\text{partition and classical link bound}\\
s=2,3,4&\text{partition and four full-carrier certificates}\\
s\ge5&\text{51 endpoint records, two fixed inequalities and propagation}\\
s\ge73&\text{stronger ONE-clique bound directly from the layers}.
\end{array}
\]
Theorem \ref{thm:global} is a cardinality statement. Table
\ref{tab:domains} distinguishes it from the structural consequences.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.21\linewidth}>{\raggedright\arraybackslash}p{.34\linewidth}>{\raggedright\arraybackslash}p{.39\linewidth}@{}}
\toprule
Conclusion & Families & Parameter domain\\
\midrule
Exact cardinality &
All four-uniform families, \(\nu\le s\) &
\(s\ge1,\ n\ge4s+4\)\\[2pt]
Clique stability \(71/143\) &
Shifted ONE, \(\nu=s\) &
\(s\ge122,\ 4s+4\le n\le a_s\)\\[2pt]
Clique extremizers &
Arbitrary, \(\nu\le s\), maximum size &
\(s\ge25,\ 4s+4\le n<a_s\)\\[2pt]
Cover extremizers &
Arbitrary, \(\nu\le s\), maximum size &
\(s=5,\ n\ge33;\ s=6,\ n\ge34;\)
\(7\le s\le121,\ n\ge a_s;\)
\(s\ge122,\ n\ge a_s+1\)\\
\bottomrule
\end{tabular}
\caption{Domains of the global and structural results.
The constants \(71\) and \(143\) control respectively the number of
edges outside the canonical clique and the symmetric difference.
The precise statements are in Section \ref{sec:structural}.}
\label{tab:domains}
\end{table}

\paragraph{Dependence on mathematical and computational inputs.}
The global cardinality proof imports Frankl's shadow inequality
\cite[Theorem 1.2]{Frankl13}; it does not import the complete
three-uniform matching theorem. The necessary finite HHL statements
are reconstructed with explicit searches and certificate checks.
The cover-uniqueness consequence also uses
\cite[Theorem 1.1]{Frankl13} at \(s=4,n\ge32\).
The complementary shifted cover-stability and graph results in
Appendix \ref{app:local} have their additional imports listed there.
Exact equality can be transferred through shifts by the two inverse
lemmas in Section \ref{sec:structural}; quantitative stability for
arbitrary families is not established.
Section \ref{sec:literature} compares the precise statements with
earlier work, including the clique-side results of Guo--Lu.
Section \ref{sec:reproduce} separates the global computations from
the additional checks required by the appendices.

\section{From the critical bounds to the global theorem}\label{sec:imports}
Write \(\partial\HH\) for the immediate shadow and
\(K_j(\A)\) for the number of \(j\)-sets all of whose appropriate uniform
subsets belong to \(\A\). Integer binomial coefficients are zero when
the upper argument is nonnegative and smaller than the lower one.
For polynomial identities we use the product extension of binomials.

We use shifting, which preserves cardinality and does not increase the
matching number, and the following classical quantitative input.

\paragraph{Shadow.}
Frankl \cite[Theorem 1.2]{Frankl13} gives
\(|\HH|\le u|\partial\HH|\) when \(\nu(\HH)=u\).
Consequently \(\nu(\HH)\le c\) implies
\(|\HH|\le c|\partial\HH|\), with the empty case immediate.

\begin{lemma}[Shifted completion]\label{lem:completion}
Let \(n\ge4t\) and let \(\F\subseteq\binom{[n]}4\) be shifted with
\(\nu(\F)\le t\). There is a shifted \(\mathcal G\supseteq\F\)
with \(\nu(\mathcal G)=t\).
Consequently, for \(K\ge0\), a bound
\[
 |\mathcal G\setminus\mathcal C_t|
 \le K\bigl(B_4(n,t)-|\mathcal G|\bigr)
\]
for every shifted \(\mathcal G\) of exact matching number \(t\)
implies the same bound for every shifted \(\F\) of matching number at most \(t\).
\end{lemma}
\begin{proof}
While the matching number is below \(t\), add a coordinatewise minimal
missing four-set. Every strict predecessor is present, so the enlarged
family is still shifted. Adding one edge increases the matching number
by at most one. The process is finite and reaches \(t\), because the
complete family has matching number \(\floor{n/4}\ge t\).
Inclusion then gives
\[
 |\F\setminus\mathcal C_t|
 \le|\mathcal G\setminus\mathcal C_t|
 \le K(B_4(n,t)-|\mathcal G|)
 \le K(B_4(n,t)-|\F|).
\]
\end{proof}

\subsection{A section bound already sufficient for the links}
\begin{lemma}[A consequence of Frankl's section method]\label{lem:P2}
For \(r\ge2\), \(t\ge1\), put
\[
 D_r(t)=(2r-1)t+r-(r-1)\floor{\frac{t+1}{r}}.
\]
Every \(r\)-uniform family with matching number at most \(t\) on
\(n\ge D_r(t)\) vertices has size at most \(B_r(n,t)\).
In particular \(D_4(3)=22\), and \(D_3(t)\le n_4(t)\) for all \(t\ge1\).
\end{lemma}
\begin{proof}
Shift and complete to matching number exactly \(t\), by the argument
of Lemma \ref{lem:completion} in uniformity \(r\).
An edge of a maximum matching avoids \([t-1]\), so shiftedness forces
the complete \(r\)-graph on \([t+r-1]\).
Put \(X=[t+1]\), \(Y=[n]\setminus X\),
\(q_0=\floor{(t+1)/r}\), and \(c=t-q_0\).
The section \(\HH\) disjoint from \(X\) has matching number at most \(c\),
using \(q_0\) disjoint edges inside \(X\).
For the nested singleton sections \(\A_1,\ldots,\A_{t+1}\) on \(Y\),
the shadow input gives \(|\HH|\le c|\A_{t+1}|\).
They are cross-dependent.

For a matching of \(v=2t-q_0+1=t+c+1\) sets of size \(r-1\) in \(Y\),
write \(d_i\) for its section counts.
The nested-neighbourhood argument gives an \(x\in[0,t]\) such that
the first \(t-x\) counts are at most \(v\) and the last \(x+1\)
are at most \(x\). Hence
\[
 \sum_{i=1}^t d_i+(c+1)d_{t+1}
 \le(t-x)v+x^2+(c+1)x
 =tv+x(x+c+1-v)\le tv.
\]
Such a matching exists because \(n\ge D_r(t)\) is precisely
\(|Y|\ge(r-1)v\). Averaging gives
\[
 |\HH|+\sum_{i=1}^{t+1}|\A_i|
 \le t\binom{|Y|}{r-1}.
\]
Every section using at least two vertices of \(X\) already meets \([t]\);
bounding it by the complete section proves the cover inequality.
The argument uses the shadow theorem and the weighted nested-section
method of \cite[Sections 3--5]{Frankl13}.

For the last assertion, write \(t=3a+b\), \(b=0,1,2\).
Then \(D_3(t)=13a+3,13a+8,13a+11\), respectively.
Exact binomial subtraction gives the following coefficients in ascending
powers of \(a\):
\[
\begin{array}{c|rrrrr|c}
 b&[a^0]&[a^1]&[a^2]&[a^3]&[a^4]&\text{domain}\\ \hline
 0&0&78&1653&7974&2175&a\ge1\\
 1&360&2782&7425&7682&2175&a\ge0\\
 2&4560&19862&29877&16966&2175&a\ge0
\end{array}
\]
The polynomial is \(24[A_4(t)-B_4(D_3(t)-1,t)]\), and is strictly
positive in each displayed domain.
Since \(B_4(n,t)\) increases with \(n\), it follows that
\(D_3(t)\le n_4(t)\).
\end{proof}
This consequence supplies every triple link in the global proof.
The complete three-uniform EMC is not an additional premise.


\subsection{The critical statement that remains to be checked}
For every \(s\ge2\), the local input is
\begin{equation}\label{eq:critical-input}
 |\F|\le M(n,s)\quad
 \text{at }n\in\{a_s-1,a_s\},\qquad
 \F\text{ shifted and ONE},\quad\nu(\F)=s.
\end{equation}
It is enough to check saturated families: enlargement under
\(\nu\le s\) preserves an existing matching avoiding 1, as explained
in Section \ref{sec:fulltrace}. The partition argument below and
Proposition \ref{prop:small} treat \(s=2,3,4\).
Section \ref{app:global} supplies the retained finite records;
Corollary \ref{an:cor:critical} supplies the propagated critical inputs.
Proposition \ref{thm:range92} also gives the stronger ONE-clique bound
for all \(s\ge73\).
We now prove the global theorem from exactly these inputs.
Their verification in the later sections uses the trace and shadow
lemmas, not the global theorem.

\subsection{Crossings, deletion and propagation}\label{sec:globalinduction}
First note that for \(s\ge2\),
\begin{equation}\label{eq:admissible-small}
 24[A_4(s)-B_4(4s+4,s)]
 =s(s-1)(81s^2+95s+26)>0.
\end{equation}
Thus \(a_s-1\ge4s+4\). Also \(a_t\le5t+4\), since
\begin{equation}\label{eq:coarse-crossing}
 24[B_4(5t+4,t)-A_4(t)]
 =113t^4+226t^3+139t^2+26t>0\qquad(t\ge1).
\end{equation}

The following inequality is the four-uniform specialization of
\cite[Proposition 5.1, equation (5.1)]{Frankl17}.
We retain the elementary proof because its strict clique branch
is used in the equality argument.
\begin{lemma}[Direct deletion]\label{lem:direct-deletion}
For \(s\ge2\), \(n\ge4s+4\),
\[
 M(n-1,s-1)+\binom{n-1}3\le M(n,s).
\]
\end{lemma}
\begin{proof}
If the preceding maximum is the cover, Pascal's identity gives
\(B_4(n-1,s-1)+\binom{n-1}3=B_4(n,s)\).
Otherwise \(B_4(n-1,s-1)<A_4(s-1)\), so
\(n-1<a_{s-1}\le5s-1\) and hence \(n-1\le5s-2\).
For \(u=s-2\ge0\), exact subtraction gives
\[
 24\left[A_4(s)-A_4(s-1)-\binom{5s-2}3\right]
 =5736+8056u+3660u^2+524u^3>0.
\]
Monotonicity of the binomial coefficient proves the remaining case.
A tie in the preceding maximum belongs to the cover case.
\end{proof}

\begin{lemma}[Propagation using the classical link range]\label{lem:link33}
If the cover bound holds for all families at \((n,t)=(a,t)\),
where \(a\ge n_4(t)\), then it holds at every \(n\ge a\).
\end{lemma}
\begin{proof}
For the step from \(n\) to \(n+1\), shift the family.
The link of its last vertex has matching number at most \(t\):
otherwise \(t+1\) disjoint triples leave at least \(t+1\) unused vertices
among the first \(n\ge a\ge4t+4\) vertices. Replace the last vertex
by those smaller distinct vertices to obtain a forbidden matching.
Lemma \ref{lem:P2}, since \(n\ge n_4(t)\ge D_3(t)\), bounds the
link by \(B_3(n,t)\). Restriction to the first \(n\) vertices and Pascal give
\(B_4(n,t)+B_3(n,t)=B_4(n+1,t)\).
\end{proof}

\begin{proof}[Proof of Theorem \ref{thm:global}]
Induct on \(s\). At \(n=4(s+1)\), a uniformly random partition into
\(s+1\) four-sets contains at most \(s\) members of any admissible family.
Taking expectations gives
\[
 |\F|\le\frac{s}{s+1}\binom{4s+4}4=\binom{4s+3}4.
\]
For \(s=1\), \(a_1=8\) and this is the cover bound; Lemma
\ref{lem:link33} propagates it to every \(n\ge8\).

Let \(s\ge2\) and assume the theorem for \(s-1\) at all admissible
ground sets. It suffices first to treat \(n=a_s-1,a_s\).
Shift and enlarge to matching exactly \(s\).
If ONE fails, deleting vertex 1 reduces the matching number exactly
by one: every maximum matching uses 1, and loses just one edge.
The remaining \(n-1\ge4(s-1)+4\) vertices are in the inductive domain.
There are at most \(\binom{n-1}3\) deleted edges, so induction and
Lemma \ref{lem:direct-deletion} prove the target.

If ONE holds, use the following exhaustive list of critical inputs.
For \(s=2,3\), the lower points are \((2,12),(3,16)\) and follow
from the partition bound; the upper points follow from
Proposition \ref{prop:small}. For \(s=4\), that proposition gives both.
For \(s\ge5\), use the 51 endpoint records of Section \ref{app:global}
selected in Corollary \ref{an:cor:critical}, the two fixed inequalities
of Lemma \ref{an:lem:anchors}, and the propagation proved there.
This covers every critical input. Proposition \ref{thm:range92}
also gives the stronger ONE-clique bound for \(s\ge73\).
At a lower point the target is the clique term, and at an upper
point it is the cover term.

Adding isolated vertices to \(a_s-1\) gives the clique bound at
every smaller admissible \(n\); Lemma \ref{lem:link33} propagates
the upper cover bound to every larger \(n\). This completes the induction.
For \(s\le4\), only the partition, small certificates and the
classical-shadow proof of Lemma \ref{lem:P2} have been used.
\end{proof}

\section{Trace reduction and critical certificates}\label{app:global}
We verify the critical input \eqref{eq:critical-input} for the finite
range. Exact traces turn a global family into finite configurations;
the ordered board retains comparisons that would be lost by a larger
symmetry quotient. The necessary layer inequalities are proved in
Section \ref{app:range92}. The four small points are checked directly
on the full carrier without those layer inequalities.

\subsection{Full-carrier traces and elementary completion}\label{sec:fulltrace}
Shifting preserves size and does not increase matching number.
A shifted family can be enlarged to a shifted family maximal under
\(\nu\le s\): add an admissible missing edge and shift again.
The old shifted core is preserved by every such shift, so size
increases; finiteness terminates the process. At \(n\ge4s+4\),
a maximal family has matching exactly \(s\), since otherwise any
missing edge could be added. If ONE held before enlargement,
its matching avoiding 1 persists.

\begin{lemma}[Exact traces on the full carrier]\label{lem:fulltrace}
Let \(\F\) be shifted, saturated under \(\nu\le s\), and ONE, with
\(\nu(\F)=s\), \(n\ge4s+4\). Put \(K=[4s+3]\), \(q=n-4s-3\).
There is an \(s\)-matching inside \(K\) avoiding 1. Choose such a
matching so that its residual
\(D=\{1,\delta_1,\delta_2\}\), \(\delta_1<\delta_2\), is
lexicographically minimal outside 1.
For \(\mathcal G=\{E\cap K:E\in\F\}\):
\begin{enumerate}
\item every trace has size 2, 3 or 4; no small trace lies inside \(D\);
\item \(\nu(\mathcal G)=s\);
\item every four-set containing a trace of \(\mathcal G\) belongs to \(\F\);
\item \(\displaystyle |\F|=\sum_{H\in\mathcal G}\binom q{4-|H|}\).
\end{enumerate}
\end{lemma}
\begin{proof}
A matching avoiding a set \(R\) can be moved into an initial segment
of \([n]\setminus R\) with at least as many available positions.
Whenever a used vertex lies beyond that segment, replace it by a
free smaller vertex in the segment; shiftedness preserves its edge
and the matching. Apply this with \(R=\{1\}\) to get the selection.

An empty trace, or a small trace in \(D\), would give an edge
disjoint from the selected matching. A singleton in a column can
be shifted to 1, with the same contradiction. This proves the first claim.

If \(s+1\) traces were disjoint, choose, among all collections of
\(s+1\) edges having disjoint traces, one maximizing the size of
their union. Their traces are allowed to change in this maximization.
The edges share some vertex \(u\notin K\), since \(\nu(\F)=s\).
Some \(v\in K\) is unused: covering all \(4s+3\) vertices of \(K\)
would leave only one of the \(4(s+1)\) edge positions outside \(K\),
which cannot support a shared vertex. Replace \(u\) by \(v\) in
one edge. Since \(v<u\), that edge remains present; its trace expands
into unused positions and remains disjoint from the others.
The union increases because another edge still uses \(u\), a contradiction.
The selected columns supply an \(s\)-matching in \(\mathcal G\).

If a four-set \(Q\) containing a trace \(H\) were absent, saturation
would supply \(s\) disjoint edges avoiding \(Q\). Their exact traces,
together with \(H\), would be \(s+1\) disjoint traces.
Thus all such completions are present. In particular every choice
of \(4-|H|\) external vertices completes \(H\), and counting edges
by their unique exact trace proves the last claim.
\end{proof}
Internal enlargements of a trace to size \(j'\le4\) are exact traces
whenever \(q\ge4-j'\). The proof rewrites the classical shifting and
mixed-trace mechanisms of \cite[Section 2]{HHL}; those mechanisms
remain attributed even though their proofs are included here.
No four-column denominator is used on the full carrier.

\subsection{The complete weighted board}
For a saturated shifted ONE family, the selected matching consists of
\(s\) four-vertex columns in \([4s+3]\), avoiding vertex 1, and a residual
three-set \(D\). For four chosen columns \(\tau\), the board has 19 vertices.
For a trace \(H\) of size \(j\in\{2,3,4\}\) meeting \(z\) columns, set
\[
 w_{s,n}(H)=\frac{\binom q{4-j}}{\binom{s-z}{4-z}},\qquad q=n-4s-3.
\]
There are exactly \(\binom{s-z}{4-z}\) boards containing that trace.
Lemma \ref{lem:fulltrace} and this multiplicity therefore give
\begin{equation}\label{eq:coupled-identity}
 |\F|-A_4(s)=\sum_\tau\Phi_{s,n}(\tau),\qquad
 \Phi_{s,n}=\sum_{\substack{|H|=2,3\\H\ {\rm present}}}w_{s,n}(H)
              -\sum_{\substack{|H|=4\\H\ {\rm missing}}}w_{s,n}(H).
\end{equation}
All quadruple layers are retained, including spread one.

\begin{figure}[ht]
\centering
\setlength{\tabcolsep}{10pt}
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{c|cccc}
Residual \(D\)&\(F_a\)&\(F_b\)&\(F_c\)&\(F_d\)\\ \hline
\(1\)&\colorbox{blue!12}{\(x_{a0}\)}&\(x_{b0}\)&\(x_{c0}\)&\(x_{d0}\)\\
\(\delta_1\)&\(x_{a1}\)&\colorbox{blue!12}{\(x_{b1}\)}&\(x_{c1}\)&\(x_{d1}\)\\
\(\delta_2\)&\(x_{a2}\)&\(x_{b2}\)&\(x_{c2}\)&\(x_{d2}\)\\
&\(x_{a3}\)&\(x_{b3}\)&\(x_{c3}\)&\(x_{d3}\)
\end{tabular}
\caption{A 19-vertex board: four matching edges and the three residual
vertices. Each column is ordered from level 0 to level 3;
\(1<\delta_1<\delta_2\). Row alignment imposes no comparison between
different columns or between a column and the residual.
The highlighted pair illustrates a trace of spread two, if present.
The \(q\) external vertices lie outside the full carrier \([4s+3]\),
not merely outside this board.}
\label{fig:board}
\end{figure}

For example, a present pair \(H=\{x_{a0},x_{b1}\}\), with \(q\ge2\),
has \(\binom q2\) completions outside the full carrier.
It lies in \(\binom{s-2}{2}\) four-column boards, each assigning it
weight \(\binom q2/\binom{s-2}{2}\). Summing those contributions
recovers its exact number of completions. Figure \ref{fig:board}
displays the local order without imposing global symmetry.


The 5016 labelled subsets of sizes 2, 3 and 4 form 291 orbits under
column permutations and residual permutations. Average the presence
indicator over this group. Its orbit coordinates \(x_i\) lie in \([0,1]\);
this does not assume that the original board is invariant.
Full columns and low seeds have value one, and small traces inside \(D\)
have value zero. Column levels retain their order.
The coordinate key records size, residual cardinality and the sorted
four column bitmasks.

The inequalities used by the certificate are all necessary:
\begin{enumerate}
\item lowering inside a column preserves presence;
\item a present trace forces a containing trace of the next size;
  for sizes \(2\) to \(3\), use \(q\ge1\) and a completion outside the board;
\item five pairwise disjoint present traces are impossible, giving
  \(\sum_{\ell=1}^5x_{H_\ell}\le4\), averaged over the group;
\item with \(T_z,P_z,M_z\) counting present triples, present pairs and
  missing quadruples of spread \(z\), Section \ref{app:range92} proves
\[
 \frac{18}{35}T_3+\frac{18}{71}P_2\le M_4,\qquad
 \frac98T_2+\frac{27}{32}P_1\le M_3,\qquad
 2T_1+2P_0\le M_2;
\]
\item the full finite support profiles give additional linear inequalities,
  as specified next.
\end{enumerate}
A triple support is a down-set of \(\{0,1,2,3\}^3\).
Three disjoint triples leaving a low level free in a column are forbidden:
that low seed and the remaining full column would complete five
disjoint traces. Enumeration gives 2016 forbidden matchings,
51 minimal down-closures, 232848 down-sets and 26893 legal down-sets.
Their 20 level-multiset counts have 1632 distinct profiles.
The pair enumeration gives 70 down-sets, 10 legal ones and 7 profiles
on 10 level classes. For every integer vector \(h\) appearing in a row,
the checker reconstructs all legal profiles \(p\) and calculates
\(\beta(h)=\max_p h\cdot p\) exactly. The inequality
\(h\cdot p\le\beta(h)\), averaged over the four triple supports or
six pair supports, is valid even when some entries of \(h\) are negative.
The distributed checker reconstructs the labelled universes and all transports.
These are classifications of the stated finite supports, not of global
four-uniform families.

For three further points, keep \(D=\{1,\delta_1,\delta_2\}\),
\(\delta_1<\delta_2\), individually fixed and average only over columns.
The 469 coordinates now record the residual bitmask.
Shifting permits replacement of any occupied vertex by the absent
minimum 1, or of \(\delta_2\) by the absent \(\delta_1\).
No comparison between \(\delta_1\) and a column vertex is assumed.
The old matching witnesses remain disjoint under every residual
permutation, now yielding distinct rows. This refinement uses 58 selected
rows of the new order type. No five-column extension constraint is consumed.

\subsection{Local order and traces forced by the minimal residual}\label{sec:prefix5}
We refine the ordered-residual model while keeping the same authentic
board. Write \(D=\{1,\delta_1,\delta_2\}\), with \(\delta_1<\delta_2\),
and select the matching to minimize \((\delta_1,\delta_2)\)
lexicographically. In the records, the four levels of column \(c\) have
labels \(4c,\ldots,4c+3\), and \(16,17,18\) denote
\(1,\delta_1,\delta_2\). These labels are positions, not global vertex values.

\begin{lemma}[Exhaustive order prefixes]\label{lem:prefix5}
Restrict the global order to a carrier with \(b\) four-vertex
columns and a residual three-set. Name columns \(0,1,\ldots\) in
order of first appearance. After a prefix \(p\), if \(k\) columns
have appeared, the next vertex is one of: the first unused residual
vertex; the first unused level of a seen column; or the first level
of the next new column, named \(k\), if \(k<b\).
Keeping all available choices partitions the orders extending \(p\).
\end{lemma}
\begin{proof}
Each residual or column is an increasing chain. The next vertex of
any interleaving must be the unused head of one of these chains.
Unseen columns differ only by names; naming the chosen one \(k\)
is canonical. The stated choices are distinct and exhaustive, and
the same argument applies after each extension.
\end{proof}

For a four-column board the root is \(p=(16)\); its children are \((16,17)\) and \((16,0)\).
The second local vertex need not be the global vertex 2.
A prefix guarantees its internal order, that every prefix vertex precedes
every unused vertex, and the internal column and residual orders.
No other comparisons are imposed. If \(a<b\) is guaranteed, shiftedness
of the original family gives
\[
 {\bf1}_H\le {\bf1}_{(H\setminus\{b\})\cup\{a\}}
 \quad(b\in H,\ a\notin H).
\]
Indeed replacing \(b\) by \(a\) in an edge realizing the exact trace
\(H\) leaves its vertices outside \([4s+3]\) unchanged.

Only the group \(S_{4-k}\) permuting unseen columns fixes this information.
Averaging over that group is therefore valid; averaging a seen column
with an unseen one is not. The key consists of the trace size, residual
bitmask, the ordered bitmasks of seen columns and the multiset of unseen
column bitmasks. For \(k=0,1,2,3,4\), respectively, the numbers of orbit
means are
\[
 469,\quad1289,\quad2920,\quad5016,\quad5016.
\]
They always represent the same 5016 labelled subsets.
Every transported row is a necessary inequality before it is averaged;
the original family is not assumed symmetric.

\begin{lemma}[Lexicographically forced traces]\label{lem:forcing5}
Let \(K=[4s+3]\), \(q=n-4s-3\), and let the shifted saturated ONE
family and its selected residual be as above.
For distinct \(x,y\in K\setminus\{1\}\), if the increasing pair associated
to \(\{x,y\}\) is lexicographically smaller than
\((\delta_1,\delta_2)\) and \(q\ge1\), then \(\{1,x,y\}\) is an exact trace.
If \(x\in K\setminus\{1\}\), \(x<\delta_1\), and \(q\ge2\), then
\(\{1,x\}\) is an exact trace.
\end{lemma}
\begin{proof}
If the triple trace is absent, choose \(u\notin K\).
The edge \(Q=\{1,x,y,u\}\) is missing. Saturation gives an \(s\)-matching
disjoint from \(Q\), hence from \(R=\{1,x,y\}\).
Compress its union into the first \(4s\) vertices outside \(R\).
This operation can be performed by an order-preserving injection that
moves every vertex downwards, so the matching remains in the shifted
family. Since \(|K\setminus R|=4s\), its residual is \(R\), contrary to
minimality.

For the pair choose distinct \(u,v\notin K\), which requires \(q\ge2\).
Absence of the pair makes \(Q=\{1,x,u,v\}\) missing.
An \(s\)-matching disjoint from \(Q\) compresses into
\(K\setminus\{1,x\}\), of size \(4s+1\). It leaves one further vertex
\(y\), and hence residual \(\{1,x,y\}\). The first coordinate of its
increasing pair is at most \(x<\delta_1\), again a contradiction.
Both compressed matchings still avoid 1.
\end{proof}

\paragraph{The low seeds.}
For a column \(E=\{a<b<c<d\}\), both \(D\cup\{a\}\) and
\(D\cup\{b\}\) are present. If \(b>\delta_2\), the ordered four-set
\(D\cup\{b\}\) is coordinatewise below \(E\).
If \(b<\delta_2\), the pair obtained by sorting \(\{\delta_1,b\}\)
is lexicographically below \((\delta_1,\delta_2)\);
Lemma \ref{lem:forcing5}, with \(q\ge1\), and completion give that seed.
Lowering \(b\) to \(a\) gives the other one.
This argument and the forced-trace lemma hold for every \(s\ge1\);
they do not require a four-column subboard.

This is the saturation/compression mechanism of
\cite[Lemma 2.5 and Section 4, especially Lemma 4.1]{HHL},
applied with the additional comparisons displayed above.
For partial orders, a triple is forced only when a guaranteed comparison
shows \(x<\delta_1\) or \(y<\delta_1\), or one vertex equals
\(\delta_1\) and the other precedes \(\delta_2\).
No incomparable pair is ordered arbitrarily.
The forcing row is \(-x_H\le-1\), with its images averaged over
\(S_{4-k}\). Pair forcing is never used at \(q=1\), or without vertex 1.

The preceding support-profile inequalities also remain available.
In this refinement each is applied to its specified two- or three-column
support before averaging over the stabilizer. Its right side is still
the exact maximum over all legal profiles, including for signed
functionals. The support census is inherited; the refinement couples
it to the local order and the forced presences.

\subsection{Dual arithmetic and global integer rounding}
For necessary rows \(Ax\le b\), semantic bounds \(l_i\le x_i\le u_i\),
and \(\Phi=c\cdot x-c_0\), every rational \(y\ge0\) gives
\begin{equation}\label{eq:dual33}
 \Phi\le y\cdot b+
 \sum_i\max\{(c-A^\mathsf Ty)_il_i,(c-A^\mathsf Ty)_iu_i\}-c_0=:U.
\end{equation}
Indeed sum \(y\) times the rows and bound each residual coordinate on its
interval. The endpoint certificates use nonnegative rational multipliers.
For every certificate, including each leaf of the order forest,
the residual term accounts exactly for rational rounding.
No solver tolerance or equality of the residual to zero is assumed.

There are \(\binom s4\) boards. With
\(\Delta_*=\max\{0,B_4(n,s)-A_4(s)\}\), the sufficient check is
\begin{equation}\label{eq:round33}
 \binom s4 U<\Delta_*+1.
\end{equation}
By \eqref{eq:coupled-identity}, \(|\F|-A_4(s)\) is an integer at most
the left side, hence at most \(\Delta_*\).
For an order tree, replace \(U\) by the maximum of all its leaf bounds.
Lemma \ref{lem:prefix5} makes this a bound for every board.
This rounds the global cardinality, not each board or each orbit mean
separately; the means remain real variables.

\begin{center}
\begin{tabular}{@{}lrrr@{}}
\toprule
Endpoint certificate & Cases & Shared rows & Positive multipliers\\
\midrule
Ordinary, 291 coordinates & 52 & 1969 & 9995\\
Minimum-completion, 469 coordinates & 3 & 758 & 1103\\
Ordered trees, leaf-specific coordinates & 33 & --- & 711130\\
\bottomrule
\end{tabular}
\end{center}
All 88 distributed endpoint bounds satisfy \eqref{eq:round33}.
The main cardinality proof uses the 51 records selected in
Corollary \ref{an:cor:critical}, together with its two fixed inequalities.
The other 37 ordinary upper records are retained for the structural gap
bounds. The 48 lower records at $s\ge25$ are superseded by the analytic
clique band and are not distributed.
The first two groups each use a shared row dictionary; the ordered
trees reconstruct rows at each dual leaf. The positive multipliers
total 722228 occurrences. The three minimum-completion points are
\((22,103),(27,125),(34,156)\).
The exact positive global rounding margins, in this order, are
\[
 \frac{717402531195218849}{200000000000000},\quad
 \frac{115229982289222811}{20000000000000},\quad
 \frac{740832624886150683}{62500000000000}.
\]
The archive records each row with its literal witness and each bound
with its multipliers; the checker recomputes the coefficients and signs.

The larger target at an upper crossing is essential. For \(s=6,n=31\)
and \(s=8,n=40\), the shifted family of four-sets using at least two
vertices of \([2s+1]\) has, respectively, 17797 and 52428 edges,
exceeding \(A_4(s)=17550,52360\), but not \(B_4(n,s)=18815,55430\).
It has matching number \(s\) and an \(s\)-matching avoiding 1.
A missing edge uses at most one initial vertex; outside it, pair
\(2s\) remaining initial vertices and complete with \(2s\) unused vertices.
This proves saturation and supplies a matching disjoint from the added edge.
Thus ONE does not force the clique bound at every small upper crossing;
these examples satisfy EMC.

\subsection{The 33 order trees and strict ONE separation}\label{sec:forest5}
\begin{proposition}[The remaining finite endpoints]\label{prop:forest5}
Under the declared board premises, the following 33 points satisfy
\(|\F|\le\max\{A_4(s),B_4(n,s)\}\) for every shifted saturated ONE family
with matching number \(s\):
\[
\begin{aligned}
 n&=n_4(s)-1 &&s=6,8,10,12,14,16,18,20,22,24,\\
 n&=n_4(s)   &&s=5,\ldots,21,23,25,26,28,30,32.
\end{aligned}
\]
\end{proposition}
\begin{proof}[Proof using the exact finite records]
For each point the original archive supplies one tree.
The complete forest has 413 nodes: 115 splits, 295 rational dual leaves and
three analytic leaves; the maximum prefix length is 7.
Every split keeps exactly the children in Lemma \ref{lem:prefix5}.
At a dual leaf the checker reconstructs its stabilizer, all necessary
rows and the rational bound \eqref{eq:dual33}, including every residual
coefficient. The global bound satisfies \eqref{eq:round33}.

An analytic leaf has precisely the prefix \((16,17,18)\).
Any present pair or triple would shift into \(D\), contradicting absence
of small traces there. Thus all small traces are absent and
\(\Phi\le0\). No infeasibility or Farkas leaf is used.

All 711130 row and multiplier occurrences are accounted for:
69937 completions, 391523 order rows, 237183 matching rows,
6321 support rows, 638 pair forcings, 5243 triple forcings and
285 wide inequalities. The ordered-tree leaves use no middle or lower
inequalities. The distributed checker reconstructs every leaf and
computes its exact bound.
The exhaustive maximum and \eqref{eq:coupled-identity} then prove the
stated integer target. Section \ref{sec:reproduce} identifies the
original records and executable checks.
\end{proof}

There is a separate arithmetic check of order coverage.
If \(r\) residual vertices and \(r_i\) vertices of column \(i\) remain
after \(p\), with \(k\) seen columns, then the number of canonical
completions of the prefix is
\begin{equation}\label{eq:prefixmass5}
 {\cal N}(p)=
 \frac{(19-|p|)!}{r!\,\prod_{i=0}^3r_i!\,(4-k)!}.
\end{equation}
Interleave the remaining labelled chains and divide by the free
renaming action on unseen columns. At the root this is
\(18!/[2!(4!)^5]=402026625\).
Distinct children have disjoint extensions, and their counts sum to the
parent's. This identity is checked at every split of all 33 trees.
It counts vertex orders, not hypergraphs.

\begin{corollary}[Strict ONE gaps at the new upper points]\label{cor:onegaps5}
At each upper point in Proposition \ref{prop:forest5}, let
\[
 g_{s,n}=\binom s4\max_{\text{leaves}}U,\qquad
 h_{s,n}=B_4(n,s)-A_4(s)-\floor{g_{s,n}}.
\]
Under the same premises, every shifted ONE family of matching number
exactly \(s\) has size at most \(B_4(n,s)-h_{s,n}\).
The positive integers \(h_{s,n}\) are:
\[
\begin{array}{rrr|rrr}
s&n&h_{s,n}&s&n&h_{s,n}\\ \hline
5&26&1&17&80&1233\\
6&31&31&18&85&4130\\
7&35&52&19&89&4682\\
8&40&193&20&94&9146\\
9&44&37&21&98&2435\\
10&49&50&23&107&8514\\
11&53&46&25&116&17864\\
12&58&478&26&120&3350\\
13&62&432&28&129&13111\\
14&67&1840&30&138&25365\\
15&71&2047&32&147&41960\\
16&76&1166&&&
\end{array}
\]
In particular a shifted family attaining \(B_4(n,s)\) at one of
these 23 points cannot have property ONE.
\end{corollary}
\begin{proof}
Enlarge the shifted ONE family to a saturated shifted family of the
same matching number by the enlargement in Section \ref{sec:fulltrace}.
Its matching avoiding 1 persists.
The forest bounds its cardinality by \(A_4(s)+\floor{g_{s,n}}\).
The displayed gaps are exact integer subtractions from the certified
rational bounds.
\end{proof}
For example, at \((s,n)=(5,26)\),
\[
 g_{5,26}=\frac{65774380902950387}{600000000000000}<110,\quad
 A_4(5)=8855,\quad B_4(26,5)=8965,
\]
and the positive rounding margin is
\[
 111-g_{5,26}=\frac{825619097049613}{600000000000000}.
\]
Consequently ONE families have at most 8964 edges there.
At \(s=28,30,32\) the upper-point bounds even round to \(A_4(s)\).
This does not restore the false uniform ONE-to-clique implication
illustrated above, or assert quantitative stability for arbitrary families.

\subsection{The four small points on the full carrier}\label{sec:small}
For \(s=2,3,4\), use all of \(K=[4s+3]\), with its \(s\) columns
and residual \(D\), rather than a four-column subboard.
The 11-, 15- and 19-vertex carriers have respectively
550, 1925 and 5016 labelled subsets of sizes 2, 3 and 4.
At the four points below \(q=2,2,2,3\), so the weights on
pairs, triples and quadruples are \((1,2,1)\) or \((3,3,1)\).
The forbidden mixed matching has \(s+1\) traces.

\begin{proposition}[Full-carrier small certificates]\label{prop:small}
For shifted ONE families with matching exactly \(s\), the following
rational upper bounds \(U_{s,n}\) hold; consequently their sizes are
at most \(\floor{U_{s,n}}\).
\begin{center}
\small
\begin{tabular}{@{}rrrrr@{}}
\toprule
\(s\)&\(n\)&\(U_{s,n}\)&\(\floor{U_{s,n}}\)&\(M(n,s)\)\\
\midrule
2&13&\(3845000000000003/10000000000000\)&384&385\\
3&17&\(13798385978428377/10000000000000\)&1379&1379\\
4&21&\(38760000000000019/10000000000000\)&3876&3876\\
4&22&\(531935000000001/125000000000\)&4255&4255\\
\bottomrule
\end{tabular}
\end{center}
No finite HHL inequality or support classification is an input.
\end{proposition}
\begin{proof}
Enlarge while preserving ONE as in Section \ref{sec:fulltrace}.
Lemmas \ref{lem:fulltrace}, \ref{lem:prefix5} and \ref{lem:forcing5}
give all required semantics. In the records the residual labels
\(4s,4s+1,4s+2\) stand for \(1,\delta_1,\delta_2\).
After \(k\) named columns, average only the group \(S_{s-k}\)
permuting unseen columns. Variables are real means in \([0,1]\).
Columns and the two low seeds are fixed present; small subsets
of \(D\) are absent. The only selected row types are guaranteed
lowering, completion, disjoint \((s+1)\)-matchings, and pair/triple
lexicographic forcing. Their validity was proved above.

For a leaf, put \(c_H=\binom q{4-|H|}\), including the multiplicity
if orbit coordinates are used. From \(Ax\le b\), box
\(\ell\le x\le u\), and a nonnegative rational dual \(y\), one gets
\[
 |\F|\le y\cdot b+
 \sum_i\max\{(c-A^{\mathsf T}y)_i\ell_i,\,
                 (c-A^{\mathsf T}y)_iu_i\}.
\]
This is the complete cardinality, not a local excess multiplied by
\(\binom s4\). Every coefficient and box correction is rational and exact.

The four trees have 129 nodes: 34 splits, 94 dual leaves and one
analytic leaf, with 213845 selected row/multiplier occurrences.
The per-point dual counts are \(4,35,4,51\).
A leaf beginning with all three residual vertices has no small trace,
since any such trace would shift into \(D\); its analytic bound is
\(A_4(s)\). Every split lists exactly the choices of
Lemma \ref{lem:prefix5}. With \(r,r_i\) remaining chain sizes,
the number of canonical completions is
\[
 \frac{(4s+3-|p|)!}{r!\prod_{i=0}^{s-1}r_i!\,(s-k)!}.
\]
At the four roots these counts are
\(1575,525525,402026625,402026625\).
They add at every split. The maximum over all leaves gives the four
displayed \(U_{s,n}<M(n,s)+1\); global integrality gives the bound.
The distributed checker lifts each geometric witness to all labelled
subsets by summing the actual permutation action, and applies the
box correction there. It verifies all 94 rational dual bounds.
The certificates and executable check are identified in
Section \ref{sec:reproduce}.
\end{proof}
At \((2,13)\), ONE has the strict bound 384 while the complete
two-cover has 385 edges. The other three ONE bounds suffice for
the general target without a strict gap.

\section{Finite board inequalities and the weight tail}\label{app:range92}
This section gives critical ONE bounds for the global induction.
It reconstructs the finite ingredients of Hou--Hu--Liu (HHL) \cite{HHL}
that the present certificates actually use. These are not inputs to the
local stability theorems. An actual selected board consists of four columns of
a selected maximum matching and the lexicographically minimal
residual three-set. Lemmas \ref{lem:fulltrace} and \ref{lem:forcing5}
prove the trace, completion and seed constructions used here.
The next two lemmas prove the support and upper-cube statements,
C1, and only the seven trace thresholds needed from C2.
The top-star row families are justified explicitly below.
The residual-row mechanism of HHL Section 6.1 follows from disjoint
traces and present columns or seeds.
The old numerical 15- and 11-vertex bounds, the old numerical top-star
bound and C3 are not imported. This assembly uses neither HHL Lemma 3.1
nor its generic localization theorem or deletion-chain criterion.

\begin{proposition}[Critical ONE bounds from 73]\label{thm:range92}
Let \(s\ge73\) and
\(n\in\{a_s-1,a_s\}\). Every shifted saturated ONE family
\(\F\subseteq\binom{[n]}4\) with \(\nu(\F)=s\) satisfies
\[
 |\F|\le A_4(s).
\]
\end{proposition}
Its proof uses the layer inequalities and the elementary weight
bounds at the end of this section; it makes no assertion about
non-ONE families before the induction in Section \ref{sec:globalinduction}.

\subsection{Support costs and rectangle persistence}\label{sec:supports92}
An actual 19-vertex board consists of a residual three-set \(D\) and
four ordered columns with levels \(0,1,2,3\). Write
\(Q=\{0,1,2,3\}^4\), \(\mathcal M\subseteq Q\) for its missing wide
quadruples, \(M=|\mathcal M|\), and \(T,P\) for the numbers of present
wide triple and pair traces, with their column supports distinguished.
Lemma \ref{lem:fulltrace} makes \(\mathcal M\) an up-set and present traces
down-sets. All four full columns and the low seeds
\(D\cup\{(j,\ell)\}\), \(\ell\in\{0,1\}\), are present; there are no
five disjoint present traces. A present trace forces each wide quadruple
extending it to be present. Thus a trace, a disjoint seed and three mutually
disjoint wide quadruples cannot all be present. Their three quadruples
give a \emph{seed clause} that must meet \(\mathcal M\).

Call \(\{1,2,3\}^4\) the upper cube. A missing top-star fixes one
coordinate to 3 and lets the other three range over \(\{1,2,3\}\).
In the no-top-star case, up-closure makes the four permutations of
\((3,1,1,1)\) present, and therefore every quadruple with at most one
coordinate in \(\{2,3\}\) is present.

\begin{lemma}[Support obstructions and the upper cube]\label{lem:support-semantic}
On an actual selected board a pair support has at most four traces and
a triple support at most 32. The pair down-set avoids any two disjoint
values whose levels in some coordinate are not exactly \(\{0,1\}\).
The triple down-set avoids any three disjoint values omitting a low
level in some coordinate. If the present upper cube has a 3-matching,
there are no wide pair or triple traces.
\end{lemma}
\begin{proof}
A forbidden pair configuration leaves a low level unused in one
support column. Add its low seed and the two outside full columns.
A forbidden triple configuration similarly admits a disjoint low seed
and the outside full column. Either construction gives five disjoint
traces, contradicting Lemma \ref{lem:fulltrace}.
This proves the support obstructions on the actual board.

For pairs, if a down-set contains a value at least 2 in one coordinate,
it contains \((2,0)\) after interchanging the coordinates. The value
\((0,1)\) would form a forbidden pair with it, so the diagram lies on
one axis. Otherwise it lies in \(\{0,1\}^2\). Both possibilities have
size at most four.

For triples Lemma \ref{de:lem:cap} below gives the bound 32 by
complementary binary blocks. This value and its equality diagrams are
due to \cite[Lemma 5.2]{HHL}. The support census is still used to check
signed facets and the size-24 cost; the scalar cap and the size-28
cost have direct proofs.

For the last assertion take three disjoint present upper quadruples
and a proposed wide trace \(H\). Choose a column outside its support
and the level-0 seed there. In a coordinate where \(H\) uses a positive
level \(f\), replace \(f\) by 0 in the unique quadruple using \(f\).
Leave the other levels fixed. If \(H\) uses 0, no change is needed.
The three resulting quadruples are coordinatewise smaller, remain
disjoint, and avoid both \(H\) and the seed. They again give five
disjoint traces. This is the lowering argument of
\cite[Lemma 5.3]{HHL}, now using the proved trace and seed lemmas.
\end{proof}

\subsection{Direct proofs for dense triple supports}\label{sec:dense-supports}
Call a down-set $T\subseteq\{0,1,2,3\}^3$ \emph{legal} if it contains
no three coordinatewise disjoint values omitting a low level in some
coordinate. Actual triple supports are legal by
Lemma \ref{lem:support-semantic}. Put $L=\{0,1\}$ and $H=\{2,3\}$.
Indices for a triple support are $0,1,2$; its outside board column is 3.
Write $[x]$ for the trace encoded by a level tuple $x$; $(x,t)$ adds
level $t$ in column 3.

\begin{lemma}[Complementary binary blocks]\label{de:lem:blocks}
Let $C_S$ be the block whose high coordinates are exactly
$\varnothing\ne S\subsetneq\{0,1,2\}$. For a legal $T$, put
$a=|T\cap C_S|$ and $b=|T\cap C_{S^c}|$.
If both are positive, $a,b\le4$; always $a+b\le8$.
\end{lemma}
\begin{proof}
Antipodes in $C_S$ exchange 0 with 1 and 2 with 3 in the respective
coordinates. An antipodal pair there and any point of $C_{S^c}$
form a bad three-matching: in a coordinate of $S$ one low level is
omitted. If $b>0$, at most one member of each of the four antipodal
pairs belongs to $T$. The same argument interchanges the blocks.
If one count vanishes the sum is at most the size of the other block.
\end{proof}

\begin{lemma}[The triple cap]\label{de:lem:cap}
A legal down-set in $\{0,1,2,3\}^3$ has size at most 32.
\end{lemma}
\begin{proof}
If it meets $H^3$, it contains $222$. If any point has level 3 in
coordinate $i$, down-closure supplies $w=3e_i$, the point $u$
with level 2 in coordinate $i$ and 1 elsewhere, and the point $v$
with level 0 in coordinate $i$ and 2 elsewhere.
These three points form a bad matching. Thus no level 3 occurs,
and the down-set is exactly $\{0,1,2\}^3$, of size 27.
Otherwise the all-high block is empty. The all-low block contributes
at most eight; the other six blocks form three complementary pairs,
each contributing at most eight by Lemma \ref{de:lem:blocks}.
\end{proof}
The value 32 and its four equality diagrams were already established
by the finite calculation of \cite[Lemma 5.2 and Section 9.3]{HHL}.
The arguments here give a direct proof and the following denser-support
description. The signed facets used elsewhere still require their
own exact checks.

\subsection{The dense support theorem in dimension three}
Define three slabs and a majority-low container by
\[
 S_i=\{x\in\{0,1,2,3\}^3:x_i\le1\}\quad (i=0,1,2),\qquad
 J=\{x:\#\{i:x_i\ge2\}\le1\}.
\]
Each has size 32. Partition the cube into the all-low block $C=L^3$, the
all-high block $H^3$, and the six blocks
\[
 A_i=\{x:x_i\in H,\ x_j\in L\ (j\ne i)\},\qquad
 B_i=\{x:x_i\in L,\ x_j\in H\ (j\ne i)\}.
\]
Thus $J=C\cup A_0\cup A_1\cup A_2$. Write $c,a_i,b_i$ for the corresponding
intersection sizes with $T$.

\begin{lemma}[Three local restrictions]\label{de:lem:local}
Assume $T$ is legal and each $a_i>0$.
\begin{enumerate}
\item If $b_i>0$, the other two $a$-counts are at most 7.
\item If $b_i\ge3$, every point of $T\cap B_i$ has its low coordinate equal
to 0, and the other two $a$-counts are at most 6.
\item If $b_i\ge3$ and $b_j>0$ for $i\ne j$, the all-low point having 1
in coordinates $i,j$ and 0 in the third coordinate is absent. Hence $c\le6$.
If all $b_i$ are positive and at least two are at least 3, then $c\le4$.
\end{enumerate}
\end{lemma}
\begin{proof}
Coordinate permutation reduces all checks to explicit triples. For (i),
$a_0,b_0>0$ force $200,022\in T$. The points $200,022,131$ form a bad
3-matching; hence $131$ is absent and $a_1\le7$. Interchanging the last
two coordinates gives $a_2\le7$.

For (ii), if $122\in T$ and $b_0\ge3$, the down-set $T\cap B_0$ contains
$023$ or $032$. In the first case $200,112,023$ is bad, with
$112\le122$. In the second case $200,121,032$ is bad, with $121\le122$.
Thus $122\notin T$, and down-closure forbids every $B_0$ point with first
coordinate 1. A down-set of size at least three in
$\{0\}\times H\times H$ contains both $023$ and $032$.
Now $200,032,121$ forbids $121$, and therefore also $131$; so $a_1\le6$.
Likewise $200,023,112$ forbids both $112$ and $113$, giving $a_2\le6$.

For (iii), $b_0\ge3$ supplies $023$, and $b_1>0$ supplies $202$.
Then $023,202,110$ is bad. Absence of $110$ also forbids $111$, giving
$c\le6$. When all three $b$-counts are positive and at least two are large,
apply this argument to all three pairs of indices: $110,101,011,111$
are absent, leaving at most four points of $C$.
\end{proof}

\begin{theorem}[Unique dense container and sharp threshold]\label{de:thm:dense}
If a legal down-set $T\subseteq\{0,1,2,3\}^3$ has $|T|\ge29$, then $T$ is contained
in exactly one of $S_0,S_1,S_2,J$. Consequently the legal down-sets of size
32 are precisely these four. The threshold 29 cannot be lowered to 28.
\end{theorem}
\begin{proof}
The all-high case in Lemma~\ref{de:lem:cap} has size 27, so $T$ contains no
all-high point. Suppose $T$ is contained in none of the four proposed
containers. Being outside every $S_i$ forces $2e_i\in T$, so all $a_i>0$.
Being outside $J$ forces at least one $b_i>0$.
If $b_i>0$, Lemma~\ref{de:lem:blocks} gives $a_i,b_i\le4$.
Put $r=\#\{i:b_i>0\}$ and $h=\#\{i:b_i\ge3\}$.
The following bounds follow directly from Lemma~\ref{de:lem:local} and
$c\le8$. The middle expression exhibits every term, so the table is a
nine-case argument, not an enumerated support census.
\begin{center}
\begin{tabular}{cccl}
\toprule
$r$&$h$&bound for $c+\sum_i(a_i+b_i)$&total\\
\midrule
1&0&$8+6+7+7$&28\\
1&1&$8+8+6+6$&28\\
2&0&$8+6+6+7$&27\\
2&1&$6+8+6+6$&26\\
2&2&$6+8+8+6$&28\\
3&0&$8+6+6+6$&26\\
3&1&$6+8+6+6$&26\\
3&2&$4+8+8+6$&26\\
3&3&$4+8+8+8$&28\\
\bottomrule
\end{tabular}
\end{center}
For example a positive $b_i\le2$ contributes at most $4+2=6$; a large
$b_i$ contributes at most $4+4=8$. A zero $b_i$ leaves only $a_i$, bounded
by 7 or 6 using another positive or large $b$-count. Every row contradicts
$|T|\ge29$.

The containers have pairwise intersections at most 24:
$|S_i\cap S_j|=16$ for $i\ne j$, and $|S_i\cap J|=24$.
Thus the container is unique. A slab has no three disjoint support values in its low coordinate. In a 3-matching inside $J$, each coordinate needs
at least one high value, whereas each point has at most one high coordinate.
There are exactly three high occurrences, one in each coordinate, so the
other two values in each coordinate are 0 and 1. Such a matching is not
bad. Thus $J$ is legal and the equality assertion follows.

Finally $W=\{x:x_0=0\text{ or }x_1=0\}$ is a down-set of size
$16+16-4=28$, in none of the four containers. Any three of its points
have two sharing one of the two indicated zero-coordinate vertices,
so $W$ has no 3-matching. This proves sharpness.
\end{proof}

\subsection{A dense slab forces the missing rectangle}
\begin{theorem}[Slab-to-rectangle]\label{de:thm:rectangle}
Under the board interface and absence of a missing top-star, suppose a triple
support $T\subseteq S_i$ has $|T|\ge29$. Then
\[
 R_{i3}=\{q\in Q:q_i,q_3\ge2\}\subseteq\mathcal M,
 \qquad |R_{i3}|=64.
\]
No hypothesis about present upper-cube 3-matchings is needed.
\end{theorem}
\begin{proof}
The binary block with coordinate $i$ low and the other two support
coordinates high has eight points; at most three are absent from $T$.
Five points in a binary cube of size eight contain an antipodal pair
$t,t'$. The two traces use levels 0,1 in column $i$, and levels 2,3 in the
other two support columns.

Let $q_i=q_3=2$ and let the other coordinates of $q$ be 0.
The known present no-top-star point $p=p^{(i)}$ has level 3 in column $i$
and level 1 elsewhere. The sets
\[
 [t],\ [t'],\ [q],\ [p],\ D\cup\{(3,0)\}
\]
are pairwise disjoint. Therefore $q$ must be missing. Its full up-closure
in $Q$ is exactly $R_{i3}$, of size $2\cdot2\cdot4\cdot4=64$.
\end{proof}

\subsection{A dense majority support forces 80 missing quadruples}
Throughout this section $T\subseteq J$ is a down-set with $|T|\ge29$.
Its hole set $J\setminus T$ has size at most three.
The no-top-star condition is \emph{not} needed in this section.

\begin{lemma}[Thirty-two forced points]\label{de:lem:forced}
Under the board interface,
$F=H^3\times\{0,1,2,3\}\subseteq\mathcal M$ and $|F|=32$.
\end{lemma}
\begin{proof}
Fix $q\in F$. For each $i=0,1,2$, construct a triple $t^{(i)}$ whose high
coordinate is $i$, with value $5-q_i$. In each coordinate distribute the
two remaining low levels 0,1 between the other two triples. There are
$2^3=8$ such unordered matchings (the unique high coordinate labels each
triple). The twelve triple values which occur each belong to exactly two
of these eight matchings: two low coordinates of a given triple fix two
orientation bits, and the bit in its high coordinate remains free.
At most three absent values destroy at most six matchings. Hence a
matching of three present triples avoiding $q$ exists.
Choose $z\in L\setminus\{q_3\}$. These triples, $[q]$, and the present
seed $D\cup\{(3,z)\}$ are pairwise disjoint. Therefore $q$ is missing.
\end{proof}

\paragraph{The hole structure.}
Within $A_i$, use binary coordinates $(x_i-2,x_j,x_k)$.
Every point of binary weight at most one belongs to $T$, since its
principal upper set in $A_i$ has at least four points. Also $C\subseteq T$:
the point $111$ has seven points above it inside $J$, and every other
point of $C$ lies below it. Thus all holes lie among the tops and coatoms
of the three $A_i$ blocks. Denote by
\[
 E_i=(3\text{ in }i,\ 1\text{ elsewhere}),\qquad
 C_{i,j}=(3\text{ in }i,\ 0\text{ in }j,\ 1\text{ in the third})
\]
the top and the two low-coordinate coatoms. The remaining coatom has
level 2 in coordinate $i$ and 1 elsewhere. Every missing coatom forces
its top missing. Consequently there are at most two missing $C_{i,j}$.
If there are two, they have the same high-coordinate index $i$, and the
holes are exactly $E_i,C_{i,j},C_{i,k}$.

\paragraph{A closed pairing on the 24 double-high triples.}
Put $B=B_0\cup B_1\cup B_2$, of size 24. Choose an oriented 3-cycle on
the coordinate indices. For each directed edge $i\to j$, with $k$ the
third coordinate, and $a,b\in\{0,1\}$, define
\begin{equation}\label{de:eq:pair}
 \begin{array}{lll}
 x_i=\epsilon_i,&x_j=2+a,&x_k=2+b,\\
 y_i=2+a,&y_j=1-\epsilon_j,&y_k=3-b.
 \end{array}
\end{equation}
For any fixed $\epsilon\in\{0,1\}^3$, these twelve pairs partition $B$:
the outgoing edge from $i$ uses the four points of $B_i$ at low level
$\epsilon_i$, and the incoming edge uses the four at low level
$1-\epsilon_i$. Each coordinate of $x$ differs from the corresponding
coordinate of $y$.

\begin{lemma}[Present complementary traces by a cyclic rule]\label{de:lem:cycle}
The cycle and $\epsilon$ can be chosen so that for every pair $x,y$ in
\eqref{de:eq:pair}, the unused two levels in each coordinate partition into
two present triples $h,h'\in T$. No matching search or archived pairing
is required.
\end{lemma}
\begin{proof}
\emph{Ordinary case: at most one missing low-coordinate coatom.}
Set $\epsilon=000$. With no missing $C_{i,j}$ choose either cycle; with
one missing $C_{u,v}$ choose the cycle in which $v$ is not the successor
of $u$. For every edge $i\to j\to k\to i$, take
\[
 \begin{array}{lll}
 h_i=3-a,&h_j=0,&h_k=1,\\
 h'_i=1,&h'_j=3-a,&h'_k=0.
 \end{array}
\]
These triples partition the unused levels. If $a=1$, they have binary
weight one in $A_i,A_j$, so are present. If $a=0$, they are
$C_{i,j},C_{j,k}$, neither missing by the orientation choice.

\emph{Exceptional case: two missing low-coordinate coatoms.}
Relabel their common high index as 0; the holes are exactly
$311,310,301$. Blocks $A_1,A_2$ are complete. Choose the cycle
$0\to1\to2\to0$ and $\epsilon=(0,0,1)$.
For an edge $i\to j$ the remaining levels are
\[
 \{1-\epsilon_i,3-a\},\quad
 \{\epsilon_j,3-a\},\quad \{0,1\}
\]
in coordinates $i,j,k$. Take
\[
 \begin{array}{lll}
 h_i=3-a,&h_j=\epsilon_j,&h_k=e,\\
 h'_i=1-\epsilon_i,&h'_j=3-a,&h'_k=1-e.
 \end{array}
\]
Use $e=0$ on $0\to1$ and $1\to2$, and $e=1$ on $2\to0$.
On the first and last edge, the triple in $A_0$ has the form
$(3-a,0,0)$, hence is present; its companion belongs to a complete block.
On the middle edge both triples belong to complete blocks.
Rotating the labels handles either other exceptional index.
These are all possibilities for at most three holes.
\end{proof}

\begin{theorem}[Majority-to-80]\label{de:thm:80}
Under the board interface, $T\subseteq J$ and $|T|\ge29$ imply $M\ge80$.
Neither absence of a missing top-star nor absence of an upper-cube
3-matching is an additional hypothesis.
\end{theorem}
\begin{proof}
For each of the twelve base pairs $x,y$ in Lemma~\ref{de:lem:cycle}, pair the
eight wide quadruples above it as
\begin{equation}\label{de:eq:fourpairs}
 \{(x,0),(y,2)\},\quad \{(x,1),(y,3)\},\quad
 \{(y,0),(x,2)\},\quad \{(y,1),(x,3)\}.
\end{equation}
These 48 pairs partition $B\times\{0,1,2,3\}$, a set of 96 points.
Consider one pair, written $q=(x,\ell), r=(y,t)$ with $\ell\in L,t\in H$;
the version with $x,y$ reversed is identical. Let $h,h'\in T$ be the
complementary triples. Completion makes $(h',5-t)$ present, and the seed
$D\cup\{(3,1-\ell)\}$ is present. The five sets
\[
 [h],\ [(h',5-t)],\ D\cup\{(3,1-\ell)\},\ [q],\ [r]
\]
partition the 19 vertices: in the first three columns the four traces
$x,y,h,h'$ use every level, and in the fourth column the levels are
$\ell,t,1-\ell,5-t$. Thus $q,r$ cannot both be present. Each of the
48 disjoint pairs contributes a missing point. Their union has exactly
two high coordinates among its first three, whereas the 32 forced points
of Lemma~\ref{de:lem:forced} have three. The sets are disjoint, giving
$M\ge32+48=80$.
\end{proof}

\begin{corollary}[The dense rectangle alternative]\label{de:cor:alternative}
On a board satisfying the interface and having no missing top-star,
\[
 |\mathcal T_I|\ge29\quad\Longrightarrow\quad
 M\ge80\ \text{or}\ R_{ij}\subseteq\mathcal M\text{ for some }i<j.
\]
The absence of an upper-cube three-matching is unnecessary for this
alternative. The size-28 cost is proved constructively below;
the size-24 cost retains the finite proof in Lemma \ref{lem:supports92}.
\end{corollary}
\begin{proof}
Relabel $I$ as columns $0,1,2$. Lemma~\ref{lem:support-semantic} and
Theorem~\ref{de:thm:dense} give the unique slab or majority container.
Apply Theorem~\ref{de:thm:rectangle} or Theorem~\ref{de:thm:80}, respectively.
\end{proof}

\subsection{A constructive cost at support size 28}

\begin{lemma}[The size-28 containers]\label{sp:lem:containers}
Every legal down-set $T\subseteq\{0,1,2,3\}^3$ of size 28 lies in a slab
$S_i$, lies in $J$, or is a coordinate permutation of
\[
 W=\{x:x_0=0\text{ or }x_1=0\}.
\]
\end{lemma}
\begin{proof}
By Lemma \ref{de:lem:cap}, the all-high block is empty. Outside the slabs
and $J$, all $a_i$ are positive and some $b_i>0$. In the nine-case table
in the proof of Theorem \ref{de:thm:dense}, only
$(r,h)=(1,0),(1,1),(2,2),(3,3)$ can attain 28.
For $(1,0)$, normalize $b_0>0$. Equality requires
$a_0=4,b_0=2,a_1=a_2=7,c=8$.
The two-point ideal in $B_0$ contains $022$ and one of $023,032,122$.
These alternatives give the bad matchings
\[
 (200,112,023),\qquad(200,121,032),\qquad(200,122,031),
\]
respectively. The auxiliary points are present because a seven-point
ideal in $A_1$ or $A_2$ omits only its maximum.

For $(1,1)$, equality requires $a_0=b_0=4,a_1=a_2=6,c=8$.
Lemma \ref{de:lem:local} gives $T\cap B_0=\{0\}\times H^2$.
The two omitted points in $A_1$ are $121,131$, so $130$ is present;
those in $A_2$ are $112,113$, so $103$ is present.
The bad matchings $(201,023,130)$ and $(210,032,103)$ exclude $201,210$.
Down-closure leaves only $200,300$ in $A_0$, a contradiction.

For $(2,2)$, normalize $b_0,b_1>0$.
Lemma \ref{de:lem:local} excludes $110$, so $T\subseteq W$ and equality
of sizes gives $T=W$.
For $(3,3)$ the same lemma excludes $110,101,011,111$, leaving at most
two points in each $A_i$, whereas equality requires $a_i=4$.
All other rows are at most 27. Finally, $W$ is legal: three of its
triples repeat a zero-level vertex in column 0 or 1.
\end{proof}

We use two elementary missing-point rules. Four known present traces
disjoint from one another and from $[q]$ force
$U(q)=\{r\in Q:r\ge q\}\subseteq\mathcal M$.
Three known present traces disjoint from one another and from the
disjoint quadruples $[q],[r]$ force at least one of $q,r$ missing.
Thus $h$ disjoint pairs outside an already forced set $F$ give
$M\ge |F|+h$. Absence of a missing top-star supplies the four present
quadruples $p^{(i)}$, with level 3 in column $i$ and 1 elsewhere.

\begin{lemma}[Eight cyclic pairs with four holes]\label{sp:lem:eight}
Let $T\subseteq J$ be a down-set of size 28. Fix the cycle
$0\to1\to2\to0$ and set $\epsilon_i=0$ in \eqref{de:eq:pair}.
At least eight of its twelve pairs have complementary triples in $T$.
\end{lemma}
\begin{proof}
The core $C=L^3$ is complete: even $111$ has seven successors in $J$.
The four holes lie in the three binary cubes $A_i$.
For the pair associated with $i\to j$, third index $k$, and $a,b\in L$,
try $e=0,1$ in
\begin{equation}\label{sp:eq:complement}
 \begin{array}{lll}
 h_i=3-a,&h_j=0,&h_k=e,\\
 h'_i=1,&h'_j=3-a,&h'_k=1-e.
 \end{array}
\end{equation}
These are complementary to $x,y$. Their presence does not depend on $b$;
each of the six slots $(i,a)$ therefore contributes zero or two pairs.

If a slot with $a=1$ fails, its $e=0$ choice forces $h'=(1,2,1)$
absent, in coordinate order $i,j,k$: $h=(2,0,0)$ has eight successors
in $A_i$ and is present. Failure also at $e=1$ requires $(2,0,1)$
absent in $A_i$ or $(1,2,0)$ absent in $A_j$.
The former costs four holes in addition to the hole in $A_j$.
Hence the holes are exactly the face $x_i=1$ in $A_j$.
Only the two slots on $i\to j$ fail; the other four are good.

Otherwise all three $a=1$ slots are good.
If $(3,0,0)$ is absent in an arm, all four holes form its high face;
the $a=0$ slot between the other two arms is good.
If every such point is present, failure of an $a=0$ slot on $i\to j$
requires the maximum $E_j$ absent and at least one of $C_{i,j},C_{j,k}$
absent, where $C_{u,v}$ has level 3 at $u$, 0 at $v$, and 1 elsewhere.
Failure on all three arcs would require three distinct maxima and at
least two distinct coatoms, since one coatom serves at most two arcs.
Five holes are impossible. There is a fourth good slot.
\end{proof}

Every retained pair lifts to the four pairs in \eqref{de:eq:fourpairs}.
The same three-trace witness used in Theorem \ref{de:thm:80} proves each
clause. They are disjoint and lie above the double-high block
$B=B_0\cup B_1\cup B_2$.

\begin{lemma}[The two exceptional majority cores]\label{sp:lem:cores}
For $T\subseteq J$ of size 28, the orientation argument of
Lemma \ref{de:lem:forced} forces all 32 points of
$H^3\times\{0,1,2,3\}$, except for the following hole sets, up to
coordinate permutation:
\[
 Z_I=\{300,301,310,311\},\qquad
 Z_{II}=\{310,311,013,113\}.
\]
For these two types it forces 16 and 24 core points, respectively.
With the no-top-star premise these counts increase to 24 and 28.
\end{lemma}
\begin{proof}
Fix $q\in H^3\times\{0,1,2,3\}$.
There are eight orientations of three complementary small triples,
one high in each column with value $5-q_i$, distributing 0 and 1
between the other two triples. Each candidate triple occurs in two
orientations. A surviving orientation and a low seed disjoint from $q$
force $q$ missing.

Four holes can kill all eight orientations only if all are relevant
and the four pairs of orientations they remove partition the cube.
A high-level-2 hole forces a high-level-3 hole above it, at least one
irrelevant to $q$. Thus all four relevant holes have high level 3.
A hole in $A_i$ corresponds to an edge of the orientation cube in
direction $i$. A perfect matching of that cube uses an even number of
edges in each direction: cutting in that direction leaves four vertices
on each side, and internal edges cover them in pairs.
The direction counts are $4+0+0$ or $2+2+0$.

In the first case all holes form a high face, giving $Z_I$.
In the second case the two holes in each arm form an upper face of its
low-coordinate square. The two pairs of orientation edges are disjoint
only if their faces fix the same remaining orientation bit; faces fixing
different bits intersect. The common low coordinate has complementary
values in the two small triples, so the two upper-face constraints
remove opposite halves. This gives $Z_{II}$.
For $Z_I$, the surviving core is $q_0=3$ (16 points);
for $Z_{II}$ it is $q_0=3$ or $q_2=3$ (24 points).

In both types $003,130\in T$. The five traces
\[
 [003],\quad[(130,3)],\quad[3111],\quad D\cup\{(3,0)\},
 \quad[2222]
\]
are disjoint. Thus $U(2222)=H^4$ is missing. Its union with the
orientation core has size 24 in type I and 28 in type II.
\end{proof}

\begin{theorem}[Constructive support cost]\label{sp:thm:64}
Under the board interface, if there is no missing top-star, then
$|\mathcal T_I|\ge28$ implies $M\ge64$.
No separate upper-cube 3-matching premise is used after support legality
and the interface have been established.
\end{theorem}
\begin{proof}
Delete maximal elements to reduce the actual support to size 28;
all retained traces and their completions remain present.
Lemma \ref{sp:lem:containers} supplies the following complete cases.

\paragraph{Majority.}
Outside types I and II, Lemmas \ref{sp:lem:eight} and
\ref{sp:lem:cores} give $M\ge32+4\cdot8=64$.
For type I the fixed cycle keeps exactly eight base pairs.
For $a,b,\ell\in L$ add the eight pairs
\begin{equation}\label{sp:eq:typeI}
 (2,2+a,2+b,\ell)\ ;\ (3,1-a,1-b,2+\ell).
\end{equation}
Use $h=(0,a,3-b)$, $h'=(1,3-a,b)$, seed $1-\ell$, and completion
level $3-\ell$. The two small triples are in the complete arms 1 and 2;
the levels partition each column. The first endpoints have three high
support coordinates and low last coordinate, outside the forced core;
the second have only one high support coordinate. Hence the eight pairs
are mutually disjoint, avoid the core, and avoid all pairs above $B$.
This gives $24+32+8=64$.

For type II, all slots on $0\to1$ and the $a=1$ slots on the other arcs
are good. The unused points $x=(3,2,1)$, $y=(1,3,2)$ admit the present
complementary triples $003,210$. Lifting this additional base pair by
\eqref{de:eq:fourpairs} gives four new disjoint pairs above $B$.
Thus $28+32+4=64$.

\paragraph{Slab.}
Normalize $T\subseteq S_0$ and put $K=L\times H^2$.
At least four points of $K$ are present.
If an antipodal pair $h,h'\in T\cap K$ exists, then
$[h],[h'],[3111],D\cup\{(3,0)\},[2002]$ are disjoint.
Consequently $U(2002)$ is missing, of size 64.

Otherwise $T\cap K$ has exactly four points and all holes lie in $K$.
In binary coordinates $(x_0,x_1-2,x_2-2)$, a four-point ideal is a
lower face or the set of weight at most one: a point of weight two
already forces its four-point principal ideal.
Up to swapping columns 1 and 2, the holes are therefore the face
$x_0=1$, the face $x_1=3$, or the weight-at-least-two set.
All three types force $2022$, using $023,(130,3),3111$ and seed 0.
For the first and third types, $032,(103,3),3111$ and seed 0 also
force $2202$. The two up-sets have union of size 48.
For $a,b,c,d\in L$ add the sixteen pairs
\begin{equation}\label{sp:eq:slab}
 (3-a,2+b,2+c,d)\ ;\ (2+a,b,c,2+d).
\end{equation}
The witnesses are $h=(0,1-b,3-c)$, $h'=(1,3-b,1-c)$, seed $1-d$,
completion $3-d$. Both small triples lie outside $K$ and are present.
The first endpoints have low last coordinate; the second have both
middle coordinates low. They avoid the forced up-sets and are all
distinct, giving $48+16=64$.

For the face $x_1=3$, use $002,(123,3),3111$ and seed 0 to force
$2302$ instead. Its up-set together with $U(2022)$ has size 40.
Keep \eqref{sp:eq:slab} and add, for $a,c,d\in L$,
\begin{equation}\label{sp:eq:slabextra}
 (3-a,1,2+c,d)\ ;\ (2+a,2,c,2+d).
\end{equation}
Here $h=(0,3,1-c)$ and $h'=(1,0,3-c)$ are present, with seed $1-d$
and completion $3-d$. These eight pairs avoid the core and the first
sixteen pairs: their first endpoints have middle coordinate 1 instead
of high, and their second have 2 instead of low. Thus $40+16+8=64$.

\paragraph{The exceptional container $W$.}
The following rows each give four known traces disjoint from $[q]$:
\begin{center}
\begin{tabular}{@{}ccccc@{}}
\toprule
$q$&Small trace&Completion&No-top-star trace&Seed level\\
\midrule
1202&032&$(203,3)$&3111&0\\
2102&302&$(023,3)$&1311&0\\
2200&032&$(303,2)$&1113&1\\
\bottomrule
\end{tabular}
\end{center}
All small traces belong to $W$.
The first two up-sets have sizes 48 and intersection 32.
The third has size 64 and intersects their union in 32 points.
Their union therefore has size 96, which suffices.
\end{proof}

The proof uses geometric cases and explicit formulas.
The companion module \texttt{emc4/support28.py} additionally constructs
and checks the witnesses on all 99 labelled supports (21 coordinate
orbits), without a stored packing list.
The census is corroboration of the written classification.
The cyclic pairing and four-pair lift are the same constructions used
above for supports of size at least 29.


\begin{lemma}[The retained no-top-star bounds]\label{lem:no-topstar-finite}
Suppose the actual board has no missing top-star and no present
upper-cube 3-matching. Then \(M\ge33\).
The per-support triple caps at
\(M=33,34\text{--}35,36\text{--}41,42\text{--}47\) are
\(0,1,4,7\), respectively. A pair support is empty for \(M\le59\)
and has at most one trace for \(60\le M\le63\).
\end{lemma}
\begin{proof}
We specify the two exhaustive searches and their soundness invariants.
They are the consumed parts of HHL's C1 and C2, with the exact released
programs and their completed executions identified in the accompanying
source and reproduction records. C1 and the seven consumed C2 records
were rerun during this audit, with complete outputs and timeout checks;
the source's fast checker alone cannot replace those executions.

First translate the present upper cube to a down-set
\(C\subseteq\{0,1,2\}^4\). Absence of a missing top-star forces the four
permutations of \((2,0,0,0)\) into \(C\).
Represent \(C\) by 27 heights \(h_{abc}\in\{0,1,2,3\}\),
nonincreasing in \(a,b,c\), and enumerate them in lexicographic order.
At each cell the upper limit is the minimum of its earlier neighbours;
the forced points give the lower limits. This visits every admissible
height assignment once. Filling every remaining cell with its maximum
permitted value gives the greatest monotone continuation, by induction
over the cells. Thus a prefix may be discarded when this upper bound
on \(|C|\) is at most 48.

At every remaining leaf test the 216 matchings
\[
 \{(t,\pi_1(t),\pi_2(t),\pi_3(t)):t=0,1,2\},
 \qquad \pi_i\in S_3.
\]
Every upper 3-matching has a unique such representation after ordering
by its first coordinate. The exact run checks 3116823 complete
candidates of size at least 49; each contains a matching. Hence
\(|C|\le48\) and \(M\ge|\mathcal M\cap\{1,2,3\}^4|\ge81-48=33\).

For the second search, fix a pair or triple value \(v\) on a labelled
support and let \(\mu(v)\) be the minimum size of an up-set
\(\mathcal N\subseteq Q\) satisfying the following necessary conditions.
It avoids the four top-star minima and every completion of \(v\);
it hits all 216 upper-matching clauses; and it hits every residual
3-matching disjoint from \(v\) and from any disjoint low seed.
If none exists set \(\mu(v)=+\infty\). An actual missing family with
trace \(v\) is feasible, so \(M\ge\mu(v)\).
These conditions deliberately impose no sufficiency claim for boards.

Here is why the finite search is exhaustive. Denote the forced-present points,
forbidden to \(\mathcal N\), by \(F\) and the principal up-set of a point \(x\) by
\(U_x\). A point with \(U_x\cap F\ne\varnothing\) cannot be selected;
delete it from each clause. An empty clause proves infeasibility.
Remove duplicate clauses and clauses containing another retained clause.
At a search state \(N\), selected points form an up-set avoiding \(F\).
A singleton unhit clause forces its principal up-set into \(N\).
Any \(h\) disjoint unhit clauses require at least \(h\) additional
points, so \(|N|+h\) is a lower bound. For a chosen unhit clause branch
over \(N\cup U_x\) for every point \(x\) in it, omitting only duplicate
states, forbidden states, or states meeting the current size cutoff.
Every feasible smaller extension lies in one of these branches.
When all clauses are hit, the state is feasible and can lower the
cutoff. These are all numerical pruning rules; branch-order heuristics
do not discard states. Generation of the residual clauses chooses
three available levels per coordinate, fixes their order in the first
coordinate and permutes the other three, covering every residual matching.

Only the following seven lower bounds are needed:
\begin{center}
\begin{tabular}{@{}lrrrrrrr@{}}
\toprule
Trace \(v\)&\(00\)&\(01\)&\(000\)&\(001\)&\(002\)&\(003\)&\(011\)\\
\(\mu(v)\ge\)&60&64&34&36&42&48&48\\
\bottomrule
\end{tabular}
\end{center}
All seven records in the pinned certificate have exact mode: with
cutoff one above the displayed bound the completed search returns the
displayed value. The full verifier checks both equalities and rejects
timeouts and nonzero process exits. Only the lower bounds are used here.
Permuting columns transports each bound without requiring symmetry of
the actual board.

Down-closure now gives the caps directly. For \(M=33\), even \(000\)
is forbidden. Through 35, excluding permutations of \(001\) leaves
only \(000\). Through 41, excluding \(002\) and \(011\) leaves \(000\)
and the three values with one coordinate equal to 1. Through 47,
excluding \(003\) and \(011\) leaves \(000\) and the six values with
a single positive coordinate equal to 1 or 2. For pairs, excluding
\(00\) leaves none; excluding \(01\) and its permutation leaves only
\(00\). No other source threshold, critical pattern or rectangle
enumeration is needed for these conclusions.
\end{proof}

\begin{lemma}[Two support costs and a rectangle alternative]\label{lem:supports92}
Suppose the actual board has neither a missing top-star nor a present
upper-cube 3-matching. For a triple support \(I\),
\[
 |\mathcal T_I|\ge24\ \Longrightarrow\ M\ge56,
 \qquad |\mathcal T_I|\ge28\ \Longrightarrow\ M\ge64.
\]
If \(|\mathcal T_I|\ge29\), then either \(M\ge80\) or
\[
 R_{ij}:=\{q\in Q:q_i,q_j\ge2\}\subseteq\mathcal M
 \quad\text{for some }i<j.
\]
\end{lemma}
\begin{proof}
Encode a triple down-set by its 16 heights in \(\{0,\ldots,4\}\),
nonincreasing along rows and columns. Recursively allowing each height
up to the minimum of its predecessors enumerates all 232848 down-sets.
A support 3-matching is forbidden when some coordinate does not use both
low levels. The 2016 forbidden matchings have 51 minimal down-closures;
excluding these leaves 26893 legal down-sets, with maximum size 32.
The parallel pair census has 70 down-sets, 10 legal, with maximum size 4.
These maxima and their antecedent classification are due to HHL.

For a fixed legal diagram, mark its wide extensions and all quadruples
with at most one high coordinate present. Generate the upper-cube
matching clauses and the seed clauses of its triples. A clause not
already hit by a forced missing point must be hit outside the forced
present set. Singleton residues force their point missing; add its
up-closure and iterate. If the resulting forced missing set is \(F\),
any \(h\) pairwise disjoint residual clauses outside \(F\) imply
\begin{equation}\label{eq:disjointcost92}
 M\ge |F|+h.
\end{equation}
For size 24, the exact certificate regenerates all representatives under
coordinate permutations, all clauses, and every claimed disjointness:
\begin{center}
\begin{tabular}{@{}rrrrl@{}}
\toprule
Support size&Labelled diagrams&Orbits&Listed clauses&Consequence\\
\midrule
24&1212&220&4338&\(M\ge56\)\\
\bottomrule
\end{tabular}
\end{center}
The size-28 implication is Theorem \ref{sp:thm:64}.
The rectangle alternative is Corollary \ref{de:cor:alternative};
it uses explicit slab and majority constructions and no stored packing.
For a larger support, delete maximal elements until the required size
is reached. Down-set structure and legality persist, and the smaller
diagram's extensions and clauses remain necessary. This extends the
size-24 certificate to every larger support.
\end{proof}

\begin{lemma}[Persistence through eleven additions]\label{lem:persistence92}
Suppose \(R_{ij}\subseteq\mathcal M\), every completion of a present
trace is present, and every seed clause is hit. If \(M\le75\), then
\(T\le96\) and \(P\le4\). This assertion does not require an up-set.
\end{lemma}
\begin{proof}
By permuting columns take \(R=R_{01}\). For a pair or triple trace \(H\),
let \(C(H)\) be its wide completions. If \(C(H)\cap R\ne\varnothing\),
the trace is impossible. Otherwise remove clauses already hit by \(R\)
and delete \(C(H)\) from each remaining clause. These residues must
be hit by \(\mathcal M\setminus R\).

The enumeration regenerates all 352 traces and 359424 seed clauses.
Completion excludes 148 traces. Another 100 traces, comprising 96 triples
and 4 pairs, require no new missing point by this test. For each of the
remaining 104 traces the certificate lists 12 disjoint residual clauses
outside \(R\), 1248 clauses in total. Such a trace would require
\(M\ge64+12=76\). Counting the only individually permitted traces proves
the bounds for \(M\le75\); simultaneous realizability is not assumed.
\end{proof}
The rectangle and its \(96/4\) cap for \(M\le66\) already occur in
HHL's C3 argument. The new content here is persistence up to 75 under
the displayed premises. The global proof below only needs persistence
up to 71.

\subsection{Integer orbit counts in the top-star branch}\label{sec:orbit92}
The symmetry reduction must retain integrality of counts, even though
averaged indicators need not be binary.

\begin{lemma}[Orbit-count integrality]\label{lem:orbit92}
Let a finite group \(G\) permute a finite set \(\Omega\), and let
\(z\in\{0,1\}^{\Omega}\). If the group average of \(z\) has value
\(x_j\) on an orbit \(O_j\) of size \(m_j\), then
\[
 m_jx_j=\sum_{\omega\in O_j}z_\omega\in\{0,1,\ldots,m_j\}.
\]
Every necessary linear system closed under \(G\) remains valid on its
averaged quotient. No invariance of \(z\) is required.
\end{lemma}
\begin{proof}
Each position in an orbit receives every orbit element equally often
under the group action. Its average is therefore the displayed count
divided by \(m_j\). Average each inequality over its translates to obtain
the quotient system; linearity preserves validity.
\end{proof}

Fix the fourth column of a missing top-star and let \(G=S_3\) permute
the other columns. There are 608 labelled indicators: 256 missing
quadruples, 256 present triples and 96 present pairs. They form 166
orbits: 20 of size 1, 96 of size 3 and 50 of size 6.
The row generator reconstructs 40345 necessary quotient inequalities
from monotonicity, completion, matching obstructions, the support caps
32/4 and all seed residues. These are the adapted row families of HHL
Appendix A.1. Their necessity is now explicit: Lemma \ref{lem:fulltrace}
gives monotonicity and completion; Lemma \ref{lem:support-semantic}
gives the pair/triple obstruction rows and caps. For each trace \(H\),
a disjoint seed and residual 3-matching \(Q_1,Q_2,Q_3\) give
\(1_H\le\sum_i1_{Q_i\text{ missing}}\), since otherwise five traces
would be disjoint. Enumerating three available values per coordinate,
anchored in the first coordinate and permuted in the others, gives
every such residual row. A seed using an additional vertex in a
trace-supported column leaves fewer than three values there and
creates no residual 3-matching. These statements justify T1--T2 and
T4--T9; the adapted cardinality and fixing rules below justify T3/T10.
Averaging these labelled rows over \(S_3\) is legitimate without
assuming symmetry of the actual board.

The slice with fourth coordinate 3 has size 64, including the 27 missing
top-star points. Partition by its number \(c\in\{0,\ldots,37\}\) of
present points. Add total budget \(M\le71\) and slice missing count
\(64-c\). In the source's alternative notation, the new budget is
\(\text{lower missing}-\text{top present}\le7\); the old bound 2 is
not retained. Initial 0/1 forcing uses only up/down closure and these
cardinalities: a missing point would force all its successors missing,
and a present point all its predecessors present. A trial violating a
forced value or a cardinality bound forces the opposite value. Iterate
to a fixed point. The forced sets are \(S_3\)-invariant, hence give
valid fixed bounds in the quotient; all remaining bounds are \([0,1]\).

\begin{lemma}[Integral top-star certificate]\label{lem:integer-topstar}
For an actual board with a missing top-star and \(M\le71\),
\[
 \alpha T+\beta P\le M,
 \qquad \alpha=\frac{18}{35},\quad\beta=\frac{18}{71}.
\]
\end{lemma}
\begin{proof}
For each of the 38 slice classes, the certificate gives a binary tree
over the valid initial box. At a split, an orbit count satisfies either
\(m_jx_j\le a\) or \(m_jx_j\ge a+1\), where \(a\) is an integer.
Lemma \ref{lem:orbit92} ensures that every actual board follows a child.
The bounds of both children are retained and checked; no real-valued
point outside the integer-count lattice needs to follow a child.

Here is the exact leaf calculation. Write the necessary rows as
\(a_i\cdot x\le b_i\), a leaf box as \(\ell\le x\le u\), and its
objective as \(f(x)=\boldsymbol c\cdot x=M-\alpha T-\beta P\).
For nonnegative integer multipliers \(z_i\) and scale \(D_*=2485000000\), put
\[
 r=D_*\boldsymbol c+\sum_i z_i a_i,\qquad
 L=\frac{-\sum_i z_i b_i+\sum_j\min\{r_j\ell_j,r_ju_j\}}{D_*}.
\]
Every feasible point obeys
\[
 D_*f(x)=r\cdot x-\sum_i z_i(a_i\cdot x)
 \ge\sum_j\min\{r_j\ell_j,r_ju_j\}-\sum_i z_i b_i=D_*L.
\]
The residual coefficients \(r_j\) are evaluated exactly, including their
box penalty. For an infeasibility leaf take \(\boldsymbol c=0\);
then \(L>0\) contradicts \(0\ge L\).

The verifier checks all regenerated row references and 8633 selected
multipliers, every split, all roots, and absence of cycles, reused or
unvisited nodes. The complete forest has 55 splits, 84 objective leaves
and 9 infeasibility leaves: 148 nodes, maximum depth 8. The minimum
objective lower bound is \(574507909/4970000000>0\), and the minimum
Farkas margin is \(1/50\). Thus each actual board follows a path ending
in an objective leaf that proves the desired inequality; an infeasibility
leaf cannot contain it. No discovery solver is used as a premise.
\end{proof}

\begin{proposition}[Wide-layer bound]\label{prop:wide-layer}
Every actual selected board satisfies
\begin{equation}\label{eq:wide92}
 \frac{18}{35}T_3+\frac{18}{71}P_2\le M_4.
\end{equation}
Here the subscript is the number of columns met by a trace, not counting \(D\).
\end{proposition}
\begin{proof}
If the upper cube has a present 3-matching, \(T=P=0\). Otherwise
\(T\le128\), \(P\le24\). For \(M\ge72\) the margin
\(M-\alpha T-\beta P\) is at least \(216/2485>0\).
For \(M\le71\) with a top-star use Lemma \ref{lem:integer-topstar}.
In the remaining branch Lemma \ref{lem:no-topstar-finite} gives
\(M\ge33\) and the triple and pair caps through 47. The other cases are:
\begin{center}
\begin{tabular}{@{}rlll@{}}
\toprule
\(M\)&Triple cap&Pair cap&Minimum margin\\
\midrule
48--55&\(T\le4\cdot23\)&\(P=0\)&\(24/35\)\\
56--59&\(T\le4\cdot27\)&\(P=0\)&\(16/35\)\\
60--63&\(T\le4\cdot27\)&\(P\le6\)&\(7296/2485\)\\
64--71, all supports \(\le28\)&\(T\le112\)&\(P\le24\)&\(112/355\)\\
64--71, some support \(\ge29\)&\(T\le96\)&\(P\le4\)&\(33832/2485\)\\
\bottomrule
\end{tabular}
\end{center}
The first three lines use Lemma \ref{lem:supports92} and the retained
pair caps. In the last line that lemma forces an included rectangle,
since \(M<80\), and Lemma \ref{lem:persistence92} applies. These cases
exhaust the range; no near-maximum gap is needed.
\end{proof}

\subsection{Explicit residual witnesses on 15 and 11 vertices}\label{sec:residual-layer}
For an actual board write \(T_i,P_i,M_i\) for present triples, present
pairs and missing quadruples meeting exactly \(i\) columns. Fix
\(k\in\{2,3\}\) columns together with \(D\). On this subboard let
\(\widehat M,\widehat T,\widehat P\) count traces of cardinality and
spread \((4,k),(3,k-1),(2,k-2)\), respectively.

\begin{lemma}[Residual inequalities]\label{lem:lower}
On the subboards of an actual selected board,
\[
 \frac9{16}\widehat T+\frac9{32}\widehat P\le\widehat M\quad(k=3),
 \qquad
 \frac23\widehat T+\frac13\widehat P\le\widehat M\quad(k=2).
\]
Consequently,
\begin{equation}\label{eq:newlower}
 \frac98T_2+\frac{27}{32}P_1\le M_3,\qquad 2T_1+2P_0\le M_2.
\end{equation}
\end{lemma}
\begin{proof}
If \(H,R_1,\ldots,R_k\) are disjoint, \(H\) is a triple or pair of
the specified spread, and each \(R_i\) is a full column, low seed or
quadruple of spread \(k\), their indicators satisfy
\begin{equation}\label{eq:residualrow}
 1_{H\text{ present}}\le
 \sum_{i:\,R_i\text{ has spread }k}1_{R_i\text{ missing}}.
\end{equation}
Otherwise these traces, with the \(4-k\) outside full columns, form
five disjoint present traces. This is HHL's residual-row mechanism.

Transport each literal row below under
\(\Gamma_k=S_3(D)\times((S_2\times S_2)^k\rtimes S_k)\), permuting
\(D\), columns, and levels within each low/high pair. The group preserves
the carriers and fixed present sets, so every transported row is valid
without symmetry of the actual assignment. Multiply each by its listed
\(z\), clear denominators by \(d_k\), and sum all transports.
The resulting labelled coefficients are:
\begin{center}
\small\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}rrrrrrrr@{}}
\toprule
\(k\)&\(d_k\)&\(|\Gamma_k|\)&Rows&Occurrences&Triple&Pair&Max. missing\\
\midrule
3&32&2304&23&52992&41472&20736&73728\\
2&3&192&8&1536&384&192&576\\
\bottomrule
\end{tabular}
\end{center}
Every labelled triple and pair has the displayed coefficient, and every
missing quadruple has load at most the displayed maximum. The carrier
sizes \((M,T,P)\) are \((480,288,54)\) and \((260,68,3)\), with orbit
counts \((13,9,5)\) and \((19,7,1)\). Orbits are determined by occupancy
in \(D\) and the sorted low/high occupancies of the columns. These
counts and all 54528 transports are checked explicitly. Divide by 73728
or 576 to obtain the subboard bounds.

Sum over the four three-column and six two-column subboards. The
multiplicities for triples, pairs and missing quadruples are \((2,3,1)\)
and \((3,6,1)\), respectively, giving \eqref{eq:newlower}. In an actual
board \(P_0=0\), because a pair in \(D\) and four full columns would
already be five disjoint traces; keeping it displays the multiplicity.
\end{proof}
The eight 11-vertex geometries use the displayed primitive witnesses,
with multipliers scaled by \(4/3\).

\paragraph{The 31 literal rows.}
Write \(D=\{d_0,d_1,d_2\}\), with columns
\(\{a_0,a_1,a_2,a_3\}\), \(\{b_0,b_1,b_2,b_3\}\), and, for \(k=3\),
\(\{c_0,c_1,c_2,c_3\}\). Juxtaposition denotes a set. Each row specifies
\(H,R_1,\ldots,R_k,z\) in \eqref{eq:residualrow}; full columns and
low seeds contribute no missing load. The tables decode the exact data.

\begin{center}
\small\setlength{\tabcolsep}{4pt}\renewcommand{\arraystretch}{1.10}
\begin{tabular}{@{}rllllr@{}}
\toprule
\multicolumn{6}{c}{15-vertex subboard}\\
Row & \(H\) & \(R_1\) & \(R_2\) & \(R_3\) & \(z\)\\
\midrule
1 & \(a_2a_3\) & \(d_0d_1d_2a_0\) & \(b_0b_1b_2b_3\) & \(c_0c_1c_2c_3\) & \(27/32\)\\
2 & \(a_0a_2\) & \(d_0d_1d_2a_1\) & \(b_0b_1b_2b_3\) & \(c_0c_1c_2c_3\) & \(27/8\)\\
3 & \(a_0a_1\) & \(d_0d_1d_2b_0\) & \(a_2b_2b_3c_0\) & \(a_3b_1c_1c_3\) & \(27/32\)\\
4 & \(d_0a_2\) & \(d_1a_3b_0c_0\) & \(a_0b_1b_2c_1\) & \(d_2a_1b_3c_3\) & \(81/16\)\\
5 & \(d_0a_0\) & \(d_1a_2b_2c_0\) & \(a_1b_0b_3c_1\) & \(d_2a_3b_1c_3\) & \(81/16\)\\
6 & \(a_2a_3b_2\) & \(d_0d_1d_2b_0\) & \(a_0b_1c_0c_1\) & \(a_1b_3c_2c_3\) & \(27/4\)\\
7 & \(a_0a_2b_2\) & \(d_0d_1d_2b_0\) & \(a_3b_1c_0c_2\) & \(a_1b_3c_1c_3\) & \(15\)\\
8 & \(a_0a_2b_2\) & \(d_0d_1d_2c_0\) & \(a_3b_0b_3c_1\) & \(a_1b_1c_2c_3\) & \(12\)\\
9 & \(a_0a_1b_2\) & \(d_0d_1d_2c_0\) & \(a_2b_0b_3c_1\) & \(a_3b_1c_2c_3\) & \(3/2\)\\
10 & \(a_0a_1b_2\) & \(d_0d_1d_2c_0\) & \(a_2b_0b_1c_2\) & \(a_3b_3c_1c_3\) & \(21/4\)\\
11 & \(a_0b_2b_3\) & \(d_0d_1d_2a_1\) & \(a_2b_0c_0c_2\) & \(a_3b_1c_1c_3\) & \(27/4\)\\
12 & \(a_0a_2b_0\) & \(d_0d_1d_2b_1\) & \(a_1b_2c_0c_2\) & \(a_3b_3c_1c_3\) & \(219/32\)\\
13 & \(a_0a_2b_0\) & \(d_0d_1d_2c_0\) & \(a_1b_1b_2c_1\) & \(a_3b_3c_2c_3\) & \(21/4\)\\
14 & \(a_0a_2b_0\) & \(d_0d_1d_2c_0\) & \(a_3b_1b_2c_1\) & \(a_1b_3c_2c_3\) & \(477/32\)\\
15 & \(a_0a_1b_0\) & \(d_0d_1d_2b_1\) & \(a_2b_2c_0c_1\) & \(a_3b_3c_2c_3\) & \(27/4\)\\
16 & \(d_0a_2b_2\) & \(d_1a_0b_0c_0\) & \(d_2a_3b_3c_2\) & \(a_1b_1c_1c_3\) & \(93/32\)\\
17 & \(d_0a_2b_2\) & \(d_1a_3b_0c_0\) & \(d_2a_0b_1c_2\) & \(a_1b_3c_1c_3\) & \(525/32\)\\
18 & \(d_0a_2b_2\) & \(a_0b_0c_0c_1\) & \(d_1a_3b_1c_2\) & \(d_2a_1b_3c_3\) & \(15/16\)\\
19 & \(d_0a_0b_2\) & \(d_1a_2b_0c_0\) & \(d_2a_1b_1c_2\) & \(a_3b_3c_1c_3\) & \(273/16\)\\
20 & \(d_0a_0b_2\) & \(a_2b_0c_0c_1\) & \(d_1a_3b_1c_2\) & \(d_2a_1b_3c_3\) & \(375/16\)\\
21 & \(d_0a_0b_0\) & \(d_1a_1b_1c_0\) & \(d_2a_2b_2c_2\) & \(a_3b_3c_1c_3\) & \(603/32\)\\
22 & \(d_0a_0b_0\) & \(a_1b_1c_0c_1\) & \(d_1a_2b_2c_2\) & \(d_2a_3b_3c_3\) & \(27/32\)\\
23 & \(d_0a_0b_0\) & \(a_2b_1c_0c_1\) & \(d_1a_1b_2c_2\) & \(d_2a_3b_3c_3\) & \(9/16\)\\
\bottomrule
\end{tabular}
\end{center}

\begin{center}
\small\setlength{\tabcolsep}{4pt}\renewcommand{\arraystretch}{1.10}
\begin{tabular}{@{}rlllr@{}}
\toprule
\multicolumn{5}{c}{11-vertex subboard}\\
Row & \(H\) & \(R_1\) & \(R_2\) & \(z\)\\
\midrule
1 & \(d_0d_1\) & \(a_0a_1a_2a_3\) & \(b_0b_1b_2b_3\) & \(1\)\\
2 & \(a_0a_2a_3\) & \(d_0d_1d_2a_1\) & \(b_0b_1b_2b_3\) & \(8/3\)\\
3 & \(a_0a_1a_2\) & \(d_0d_1d_2b_0\) & \(a_3b_1b_2b_3\) & \(8/3\)\\
4 & \(d_0a_2a_3\) & \(d_1a_0b_0b_2\) & \(d_2a_1b_1b_3\) & \(4\)\\
5 & \(d_0a_0a_2\) & \(d_1a_1b_0b_2\) & \(d_2a_3b_1b_3\) & \(16\)\\
6 & \(d_0a_0a_1\) & \(d_1a_2b_0b_2\) & \(d_2a_3b_1b_3\) & \(4\)\\
7 & \(d_0d_1a_2\) & \(d_2a_0b_0b_2\) & \(a_1a_3b_1b_3\) & \(8\)\\
8 & \(d_0d_1a_0\) & \(d_2a_2b_0b_2\) & \(a_1a_3b_1b_3\) & \(8\)\\
\bottomrule
\end{tabular}
\end{center}


\subsection{A common counting functional for propagation}\label{sec:assembly92}
On an actual board let $T_z,P_z$ count present triple and pair traces
meeting $z$ columns, and let $M_z$ count missing quadruples of spread $z$.
There are no pair or triple traces entirely in $D$, so $P_0=T_0=0$.
We write $q=n-4s-3$ and use $q\ge2$ below; the partition bound treats
$q=1$. All comparisons keep this same board fixed while varying
the coefficients.
Let $D_s=(s-1)(s-2)(s-3)$ and define $G(s,q)=-D_s\Phi_{s,n}$. Explicitly,
\begin{align}\label{an:eq:G}
 G(s,q)={}&D_sM_4+(s-1)(s-2)M_3+2(s-1)M_2+6M_1\notag\\
 &-q(s-1)(s-2)T_3-q(q-1)(s-1)P_2-2q(s-1)T_2\notag\\
 &-3q(q-1)P_1-6qT_1.
\end{align}
The following layer inequalities proved above are used throughout:
\begin{align}\label{an:eq:layers}
 M_4&\ge\frac{18}{35}T_3+\frac{18}{71}P_2,&
 M_3&\ge\frac98T_2+\frac{27}{32}P_1,& M_2&\ge2T_1.
\end{align}
For the cover-ray argument we also use the support bounds
\begin{equation}\label{an:eq:caps}
 T_3\le128,\qquad P_2\le24.
\end{equation}
The scalar support caps have the direct proofs above. Signed support facets,
the other support costs, and the remaining layer calculations retain their
specified finite checks.

\subsection{Two incidence inequalities with direct proofs}
\begin{lemma}[Completion and shifting incidences]\label{an:lem:incidence}
On every actual selected board with $q\ge2$,
\begin{equation}\label{an:eq:incidence}
 8P_2\le3T_3,\qquad 3T_3\le8T_2.
\end{equation}
\end{lemma}
\begin{proof}
Each wide pair meets two columns. Adding one of the eight vertices in the other
two columns produces a present exact wide triple: completion is valid because
an external vertex is available. Count incidences of such a pair and one of its
wide triple completions. There are $8P_2$ incidences. A wide triple contains at
most three wide pairs, proving the first inequality.

For the second inequality, start with a present wide triple $H$ and mark one of
its three vertices $x$. Shift $x$ to the distinguished residual vertex $1$.
This is a genuine lowering in the underlying ordered ground set. Keeping an
external completion vertex unchanged shows that
$\{1\}\cup(H\setminus\{x\})$ is a present exact triple meeting two columns.
For any image, the deleted vertex must belong to one of the two unused board
columns, giving at most eight preimages. Thus $3T_3\le8T_2$.
\end{proof}
\begin{remark}
The second proof uses the actual minimum vertex, before any averaging that
forgets which residual vertex is $1$. The resulting count inequality is
invariant under residual and column permutations, so it survives averaging.
We do not assert that every point of the original linear relaxation satisfies
an unrecorded labelled minimum-shift constraint.
\end{remark}

\subsection{Two fixed counting inequalities}
The file \texttt{analytic\_anchors.json.gz} supplies two fixed rational
inequalities for the ordinary selected-board model. Their coefficients do not
vary with $s,q$; the primitive rows have the meanings proved in this paper.
\begin{lemma}[Fixed base and tangent]\label{an:lem:anchors}
Under the ordinary-board necessary rows,
\begin{align}\label{an:eq:base}
 12144M_4+552M_3+48M_2+6M_1
 &\ge6624T_3+3168P_2+576T_2+396P_1+72T_1,\\
 3172M_4+94M_3
 &\ge1680T_3+816P_2+96T_2+69P_1.\label{an:eq:tangent}
\end{align}
\end{lemma}
\begin{proof}[Exact rational proof interface]
The left side minus right side in \eqref{an:eq:base} is $G(25,12)$.
Call the difference in \eqref{an:eq:tangent} $H$.
The supplied records use respectively 247 and 160 positive rational
multipliers, each with denominator at most 100.

Here is the precise algebraic proof, so the certificates do not rely on solver
tolerances. Let $x_i$ be the orbit-presence coordinates. Change to defect
coordinates $z_i=x_i$ for pairs and triples and $z_i=1-x_i$ for quadruples.
The clique vector becomes $z=0$. Coordinates fixed by the semantic bounds are
zero in this new system; all free coordinates are nonnegative.
Every row used in these two certificates is tight at the clique vector, so it
becomes $a_r\cdot z\le0$.
For the target coefficient vector $c$, the supplied nonnegative rational
multipliers $y_r$ satisfy, on every free coordinate,
\[
 r=c+\sum_r y_ra_r\ge0.
\]
Consequently
\[
 c\cdot z=r\cdot z-\sum_r y_r(a_r\cdot z)\ge0.
\]
The minimum free residual for \eqref{an:eq:base} is
$9058789/414960>0$; for \eqref{an:eq:tangent} it is zero, with all residuals
nonnegative. The verifier reconstructs the primitive rows from their literal
witnesses, the coordinate multiplicities, clique tightness, and every rational
residual coefficient. Baseline rows are checked against the declared layer
formulas; their mathematical and finite proofs are those of this section.
\end{proof}

\subsection{A uniform clique band beginning at 25}
\begin{theorem}[Half-slope clique propagation]\label{an:thm:clique}
Let $s\ge25$ be an integer and $2\le q\le(s-1)/2$ an integer. For every actual
selected board satisfying the layer premises, $G(s,q)\ge0$.
Hence every shifted saturated ONE family in this band satisfies $|\F|\le A_4(s)$.
\end{theorem}
\begin{proof}
First work on the formal ray $s=25+u$, $q=12+u/2$, $u\ge0$. The board counts
are fixed while the coefficients vary. This is polynomial comparison on one
board, not the construction of a family with fractional parameters.
Expanding \eqref{an:eq:G} gives
\[
 G(25+u,12+u/2)=G_0+uG_1+u^2G_2+u^3G_3,
\]
where
\begin{align*}
 G_0={}&G(25,12),\\
 G_1={}&1586M_4+47M_3+2M_2-840T_3-408P_2-48T_2
       -\tfrac{69}{2}P_1-3T_1,\\
 G_2={}&69M_4+M_3-\tfrac{71}{2}T_3-\tfrac{35}{2}P_2-T_2-\tfrac34P_1,\\
 G_3={}&M_4-\tfrac12T_3-\tfrac14P_2.
\end{align*}
The first coefficient is nonnegative by \eqref{an:eq:base}. The next satisfies
\[
 G_1=\tfrac12H+2M_2-3T_1\ge0
\]
by \eqref{an:eq:tangent} and $M_2\ge2T_1$.
For the quadratic coefficient, the layer inequalities give
\[
 G_2\ge-\frac{T_3}{70}-\frac{P_2}{142}+\frac{T_2}{8}+\frac{3P_1}{32}.
\]
Apply \eqref{an:eq:incidence}; because the coefficient of $P_2$ is negative, its
\emph{upper} bound is used. This gives
\begin{equation}\label{an:eq:G2positive}
 G_2\ge\left(\frac3{64}-\frac1{70}-\frac3{1136}\right)T_3+
             \frac3{32}P_1
       =\frac{4763}{159040}T_3+\frac3{32}P_1\ge0.
\end{equation}
Finally,
\[
 G_3\ge\frac{T_3}{70}+\frac{P_2}{284}\ge0.
\]
All four Taylor coefficients are nonnegative, proving the entire ray, not
merely a finite sample. For fixed $s$ and nonnegative counts, $G(s,q)$ is
nonincreasing for $q\ge1$: both $q$ and $q(q-1)$ are nondecreasing and occur
only with negative trace coefficients. The band below the ray follows.
Summing $\Phi=-G/D_s\le0$ in \eqref{eq:coupled-identity} proves the cardinality claim.
\end{proof}

\subsection{Cover rays from two fixed endpoint anchors}
For $s>0$ define
\begin{align}\label{an:eq:Z}
 Z(s,q)&=\frac{24}{s}\,[B_4(4s+3+q,s)-A_4(s)]\notag\\
 &=4q^3+42q^2s+18q^2+148qs^2+126qs+22q
   -81s^3-162s^2-99s-18,
\end{align}
and set $J(s,q)=G(s,q)+Z(s,q)$, where $Z$ is a constant per board.
Since $\binom{s}{4}/D_s=s/24$, a boardwise inequality $J\ge0$ implies
\[
 |\F|-A_4(s)\le\binom{s}{4}\frac{Z(s,q)}{D_s}=B_4(n,s)-A_4(s).
\]
We use the upper-endpoint certificates at $(s,n)=(33,152)$ and
$(36,165)$, as fixed inequalities on the common four-column board. Exact residual-aware reconstruction
gives the positive boardwise margins
\begin{align}\label{an:eq:margins}
 J(33,17)&\ge m_o:=\frac{37290250580546743}{1562500000000}>0,\notag\\
 J(36,18)&\ge m_e:=\frac{426057745890672159}{50000000000000}>0.
\end{align}
These follow from the rational upper bounds for $\Phi$, before any
integer rounding. All consumed rows have four-column domain; thus these are
inequalities for the common board model, not assumptions about the existence
of a smaller-parameter family associated to a larger board.

\begin{theorem}[Two cover rays]\label{an:thm:cover}
The cover bound holds for actual shifted saturated ONE families at
\[
 n=\frac{9s+7}{2}\quad(s\ge33\text{ odd}),\qquad
 n=\frac{9s+6}{2}\quad(s\ge36\text{ even}).
\]
\end{theorem}
\begin{proof}
Expand $J$ on the formal rays $(s,q)=(33+u,17+u/2)$ and
$(36+u,18+u/2)$, respectively. Write $J=J_0+uJ_1+u^2J_2+u^3J_3$.
The constant coefficient is positive by \eqref{an:eq:margins}.
At either anchor $(s_0,q_0)$, applying the layers to the coefficients of $G$
gives
\begin{align*}
 G_1&\ge a_1T_3+b_1P_2+c_1T_2+d_1P_1+T_1,\\
 G_2&\ge a_2T_3+b_2P_2+\tfrac18T_2+\tfrac3{32}P_1,\\
 G_3&\ge\tfrac1{70}T_3+\tfrac1{284}P_2,
\end{align*}
where the exact coefficients at the two anchors are
\begin{center}\small
\begin{tabular}{@{}lrrrrrr@{}}\toprule
$(s_0,q_0)$&$a_1$&$b_1$&$c_1$&$d_1$&$a_2$&$b_2$\\\midrule
$(33,17)$&$-2969/35$&$-4924/71$&$39/8$&$117/32$&$-47/70$&$-131/142$\\
$(36,18)$&$-1889/35$&$-5615/142$&$53/8$&$183/32$&$-3/70$&$-111/284$\\\bottomrule
\end{tabular}
\end{center}
The $Z$ coefficients, in ascending powers of $u$, are
\[
 (145792,13196,398,4),\qquad(60966,8660,675/2,4).
\]
Using $T_3\le128$, $P_2\le24$ for negative coefficients and discarding
nonnegative terms gives
\begin{center}
\begin{tabular}{@{}lrrr@{}}\toprule
Anchor&lower bound for $J_1$&lower bound for $J_2$&lower bound for $J_3$\\\midrule
$(33,17)$&$1673628/2485$&$720442/2485$&$4$\\
$(36,18)$&$1994568/2485$&$1603491/4970$&$4$\\\bottomrule
\end{tabular}
\end{center}
All are strictly positive. Thus $J\ge0$ for every $u\ge0$ on either ray.
Restricting to integer ground-set sizes and summing proves the assertion.
\end{proof}
The strict margins in \eqref{an:eq:margins} suffice for propagation.
The numerical ONE gaps in Section \ref{sec:structural} continue to use
their separately checked endpoint bounds.

\subsection{Locating every critical point without a finite scan}
\begin{lemma}[Crossing localization]\label{an:lem:crossing}
For odd $s\ge3$,
\[
 a_s\le\frac{9s+7}{2}.
\]
For even $s\ge26$,
\[
 a_s\le\frac{9s+6}{2}.
\]
Consequently, for every integer $s\ge25$, the lower critical point satisfies
$a_s-1\le\lfloor(9s+5)/2\rfloor$.
\end{lemma}
\begin{proof}
Substitution in \eqref{an:eq:Z} gives
\[
 Z\left(s,\frac{s+1}{2}\right)=2(s^2-1)(2s+1)>0\qquad(s>1).
\]
At $q=s/2$, writing $s=26+u$ gives
\[
 Z\left(26+u,\frac{26+u}{2}\right)
 =4116+3110u+\frac{435}{2}u^2+4u^3>0\quad(u\ge0).
\]
For the stated parity, the corresponding $n$ is integral. Monotonicity of
$B_4(n,s)$ locates the crossing. Subtracting one and taking the integer part
gives the last assertion.
\end{proof}
\begin{corollary}[Critical endpoints from a finite anchor set]\label{an:cor:critical}
All critical ONE inputs hold for every $s\ge35$, and also for $s=33$,
using Theorems \ref{an:thm:clique} and \ref{an:thm:cover}. Every lower critical input
with $s\ge25$ follows from Theorem \ref{an:thm:clique}.
\end{corollary}
\begin{proof}
The lower point belongs to the clique band by Lemma \ref{an:lem:crossing}.
If the upper point also satisfies $2q\le s-1$, use that band again.
Otherwise, integrality and the crossing upper bound leave just one possible
value: $q=(s+1)/2$ in the odd case and $q=s/2$ in the even case.
The relevant cover ray applies to odd $s\ge33$ and even $s\ge36$.
\end{proof}
For the remaining finite range retain both endpoints for $5\le s\le24$,
the upper endpoints for $25\le s\le32$ and $s=34$, and the two cover anchors
$s=33,36$. These are 51 records: 15 ordinary, three minimum-preserving and
33 ordered trees. Together with the two fixed inequalities of
Lemma \ref{an:lem:anchors}, they give 53 endpoint-or-anchor obligations
for the main cardinality argument. The polynomial argument supplies all
other critical inputs. The four small full-carrier cases and the
layer proofs remain separate dependencies.

\subsection{The strong critical clique bound from the layers}
\begin{proposition}[Direct layer proof of a half-ray]\label{an:prop:71}
Using only \eqref{an:eq:layers} and \eqref{an:eq:incidence},
$G(s,q)\ge0$ whenever $s\ge71$ and $2\le q\le(s-1)/2$.
\end{proposition}
\begin{proof}
At $q=(s-1)/2$, substituting the three layer bounds in $G$ gives
$G\ge aT_3+bP_2+cT_2+dP_1+eT_1$, where
\begin{align*}
 a&=\frac{(s-73)(s-2)(s-1)}{70},&
 b&=\frac{(s-73)(s-3)(s-1)}{284},\\
 c&=\frac{(s-10)(s-1)}8,&
 d&=\frac{3(s-1)(s+6)}{32},&e&=s-1.
\end{align*}
For $s\ge73$ all are nonnegative. For $71\le s\le73$, $b\le0$, and
\eqref{an:eq:incidence} gives
\[
 G\ge\left(a+\frac38b+\frac38c\right)T_3+dP_1+eT_1.
\]
The coefficient in parentheses equals
\[
 \frac{(s-1)(2482s^2-178905s+303152)}{159040}.
\]
Writing $s=71+u$, its quadratic factor is
$112659+173539u+2482u^2>0$. Monotonicity in $q$ completes the proof.
\end{proof}
\begin{proof}[Proof of Proposition \ref{thm:range92}]
The following identities locate the upper crossing:
\begin{align*}
 Z\left(49+u,\frac{48+u}{2}\right)&=4728+9946u+397u^2+4u^3>0,\\
 Z\left(74+u,\frac{72+u}{2}\right)&=32904+22978u+\frac{1201}{2}u^2+4u^3>0
 \qquad(u\ge0).
\end{align*}
For odd $s\ge73$ the first gives $q\le(s-1)/2$ at $n=a_s$;
for even $s\ge74$ the second gives $q\le(s-2)/2$.
Both critical points therefore lie in the band of
Proposition \ref{an:prop:71}. Summing $-G/D_s$ in
\eqref{eq:coupled-identity} proves $|\F|\le A_4(s)$.
This proof uses the layer inequalities and the incidence lemma; it
does not use the two fixed anchors.
\end{proof}

\section{Structural consequences of the global proof}\label{sec:structural}
The strict margins in the preceding proof also constrain extremizers.
The following conclusions have explicitly stated domains; they do not
classify every crossing case or transfer quantitative stability
through arbitrary shifts.

\subsection{ONE gaps and their propagation}
\begin{proposition}[All finite upper gaps]\label{prop:allonegaps}
For \(5\le s\le72\), let \(U_s\) be the certified rational upper bound
on \(|\F|-A_4(s)\) at \(n=a_s\), including the board multiplicity.
Put \(h_s=B_4(a_s,s)-A_4(s)-\floor{U_s}\).
All 68 integers \(h_s\) are positive; their minimum is 1 at \(s=5\).
Every shifted ONE family of matching number exactly \(s\) on
\(n\ge a_s\) vertices satisfies
\[
 |\F|\le B_4(n,s)-h_s.
\]
For \(73\le s\le121\), the same conclusion holds with
\(h_s=B_4(a_s,s)-A_4(s)>0\); the minimum of these 49 gaps
is 75175 at \(s=97\).
\end{proposition}
\begin{proof}
At the base, saturation preserves the matching avoiding 1.
For \(5\le s\le72\), the 52 ordinary, three minimum-preserving
and 33 order-tree endpoint records retained in the supplement supply
the upper bounds. Exact global rounding gives the displayed \(h_s\).
The complete replay extracts all 68 fractions from these records
and checks their positivity. The 23 values in
Corollary \ref{cor:onegaps5} are a subset.
For \(73\le s\le121\), Proposition \ref{thm:range92} gives
\(|\F|\le A_4(s)\); exact binomial subtraction at the 49 crossings
gives the asserted positive differences.

Write \(\F[N]=\F\cap\binom{[N]}4\).
A matching of \(s\) edges avoiding 1 can be moved, by replacements
with unused smaller vertices, into \(\{2,\ldots,4s+1\}\).
Shiftedness and disjointness persist, so \(\F[a_s]\) still
has matching \(s\) and ONE. For every \(N\ge a_s\), the last-vertex
link argument of Lemma \ref{lem:link33} gives
\[
 B_4(N+1,s)-|\F[N+1]|
 \ge B_4(N,s)-|\F[N]|.
\]
The added link has at most \(B_3(N,s)\) edges, and Pascal's
identity gives exactly that increase in the cover size.
Thus the deficit at the base cannot be lost.
\end{proof}

\subsection{The stronger weight surplus for stability}
For reference the six layer comparisons are
\begin{equation}\label{eq:caps92}
\begin{aligned}
 \frac q{s-3}&\le\frac{18}{35},&
 \frac{q(q-1)}{(s-2)(s-3)}&\le\frac{18}{71},\\
 \frac{2q}{s-2}&\le\frac98,&
 \frac{3q(q-1)}{(s-1)(s-2)}&\le\frac{27}{32},\\
 \frac{3q}{s-1}&\le2,&
 \frac{6q(q-1)}{s(s-1)}&\le2.
\end{aligned}
\end{equation}

\begin{lemma}[Structural weight surplus]\label{lem:weightsmall}
Let $s\ge122$ and $4s+4\le n\le a_s$. The six left sides of
\eqref{eq:caps92}, in row order, are bounded componentwise by
$(1/2,1/4,1,3/4,3/2,3/2)$.
\end{lemma}
\begin{proof}
For \(s\ge122\) we prove
\[
 a_s\le N_s:=\floor{\frac{9s+3}{2}}.
\]
Write \(P(s)=24[B_4(N_s,s)-A_4(s)]\).
For \(s=2u\), \(N_s=9u+1\), direct binomial subtraction gives
\[
 P(2u)=64u^4-3844u^3-736u^2-44u.
\]
At \(u=61+v\) this becomes
\[
 10877520+15106728v+724676v^2+11772v^3+64v^4>0
 \qquad(v\ge0).
\]
For \(s=2u+1\), \(N_s=9u+6\), one obtains
\[
 P(2u+1)=64u^4-2944u^3-5296u^2-3104u-600.
\]
At \(u=48+v\) this becomes
\[
 1804200+7451104v+455504v^2+9344v^3+64v^4>0
 \qquad(v\ge0).
\]
The odd case holds already for \(s\ge97\); the common domain
\(s\ge122\) suffices. Positivity and monotonicity of \(B_4(n,s)\)
give the asserted crossing upper bound. Hence at both critical choices
\[
 q=n-4s-3\le \frac{s-3}{2}.
\]
Using also \(q(q-1)\le(s-3)(s-5)/4\), the six left sides of
\eqref{eq:caps92} are bounded componentwise by
\[
 (1/2,\ 1/4,\ 1,\ 3/4,\ 3/2,\ 3/2),
\]
strictly below the respective right sides.
\end{proof}
The polynomial checker reconstructs both identities from falling products.
These stronger coefficients are used for stability below; cardinality
already follows from the wider band in Section \ref{sec:assembly92}.

\subsection{Clique stability and equality}
The source of stability is a surplus in the same layer inequalities
that prove cardinality. If \(S_\tau\) is the small-trace contribution
and \(W_\tau\) is the missing-quadruple contribution on a board, then
\(W_\tau\ge(1+1/71)S_\tau\).
Summing the board identity gives
\(d=\sum_\tau(W_\tau-S_\tau)\ge X/71\), because the trace
multiplicities identify \(\sum_\tau S_\tau\) with the number \(X\)
of external edges. The proof below establishes this surplus with
the six explicit coefficient comparisons.

\begin{theorem}[Explicit clique stability for shifted ONE families]
\label{thm:cliquestability}
Let \(s\ge122\), \(4s+4\le n\le a_s\), and let \(\F\) be shifted
with matching number exactly \(s\) and Property ONE.
Put \(K=[4s+3]\), \(d=A_4(s)-|\F|\) and
\(X=|\F\setminus\binom K4|\). Then \(d\ge0\) and
\[
 X\le71d,\qquad
 \left|\F\mathbin{\triangle}\binom K4\right|\le143d.
\]
\end{theorem}
\begin{proof}
First take a saturated family at \(n=a_s\). Set
\(\lambda_4=1\), \(\lambda_3=1/(s-3)\) and
\(\lambda_2=1/\binom{s-2}2\).
Let \(e_1,\ldots,e_6\) be the six left sides of
\eqref{eq:caps92}, in row order. On a board \(\tau\), the total
positive contribution of its small traces is
\[
 S_\tau=\lambda_4(e_1T_3+e_2P_2)
        +\lambda_3(e_3T_2+e_4P_1)
        +\lambda_2(e_5T_1+e_6P_0).
\]
The notation \(T_z,P_z\) is that of the layer inequalities.
Let \(W_\tau\) be the total weighted contribution of all missing
quadruples, so the coupled functional is \(S_\tau-W_\tau\).

The proof of Lemma \ref{lem:weightsmall} bounds \(e\) by
\(v=(1/2,1/4,1,3/4,3/2,3/2)\) componentwise.
The layer coefficients are \(c=(18/35,18/71,9/8,27/32,2,2)\), and
\[
 (c_i/v_i)_{i=1}^6=(36/35,72/71,9/8,9/8,4/3,4/3).
\]
Thus \(c_i\ge(72/71)e_i\).
Multiply the three layer inequalities by \(\lambda_4,\lambda_3,
\lambda_2\). The weighted missing quadruples of spreads 4, 3 and 2
contribute at least \(72S_\tau/71\); those of spread 1 contribute
nonnegatively. Hence \(W_\tau-S_\tau\ge S_\tau/71\).
By \eqref{eq:coupled-identity},
\(d=\sum_\tau(W_\tau-S_\tau)\), whereas trace multiplicity gives
\[
 \sum_\tau S_\tau
 =\sum_{\substack{H\text{ a trace}\\|H|=2,3}}
       \binom{n-4s-3}{4-|H|}
 =X.
\]
Indeed Lemma \ref{lem:fulltrace} gives one small trace per edge
outside \(K\), with all its completions present by saturation.
It follows that \(X\le71d\).

Start with the original family, add isolated vertices up to \(a_s\), then
enlarge to a saturated shifted \(\mathcal G\supseteq\F\) of the
same matching number, as in Section \ref{sec:fulltrace}.
The original matching avoiding 1 persists, and the fixed set \(K\)
does not change. Therefore
\[
 X(\F)\le X(\mathcal G)
 \le71(A_4(s)-|\mathcal G|)
 \le71(A_4(s)-|\F|).
\]
This also gives \(d\ge0\). Finally
\(\left|\F\mathbin{\triangle}\binom K4\right|=d+2X\).
\end{proof}
The constants are sufficient, without an optimality assertion.
The quantitative statement requires both shiftedness and ONE.

\begin{proposition}[Clique rigidity from the strict anchor]
\label{prop:cliquerigidity25}
Let \(s\ge25\), \(4s+4\le n<a_s\), and let \(\F\) be shifted
with matching number exactly \(s\) and Property ONE.
If \(|\F|=A_4(s)\), then \(\F=\binom{[4s+3]}4\).
\end{proposition}
\begin{proof}
First prove rigidity for saturated shifted ONE families of size
\(A_4(s)\) throughout the band \(2\le q=n-4s-3\le(s-1)/2\).
On each selected board, the proof of Theorem \ref{an:thm:clique}
gives \(G(s,q)\ge G(25,12)\): all subsequent coefficients on the
half-slope ray are nonnegative, and \(G\) is nonincreasing in \(q\).
The strict residual in Lemma \ref{an:lem:anchors} gives
\[
 G(25,12)\ge r_0\sum_{i\text{ free}}z_i,
 \qquad r_0=\frac{9058789}{414960}>0,
\]
where \(z_i=x_i\) for small traces and \(z_i=1-x_i\) for
quadruples, as in the proof of that lemma.
By \eqref{eq:coupled-identity},
\[
 \sum_\tau G_\tau(s,q)
 =D_s\bigl(A_4(s)-|\F|\bigr)=0.
\]
All summands are nonnegative, so every free small-trace coordinate
vanishes on every board. These coordinates are averages of indicators;
thus all corresponding traces are absent. The small traces contained
entirely in \(D\) are already excluded by Lemma \ref{lem:fulltrace}.

Every trace meets at most four matching columns, which can be extended
to a selection of four columns since \(s\ge25\). Hence no small trace
escapes these boards. Lemma \ref{lem:fulltrace} then excludes every edge
outside \(K=[4s+3]\): such an edge has a trace of size 2 or 3.
Since \(|\F|=\binom{|K|}4\), all quadruples of \(K\) are present.

For a general shifted ONE family in the stated domain, Lemma
\ref{an:lem:crossing} gives
\[
 n\le a_s-1\le N_s=\left\lfloor\frac{9s+5}{2}\right\rfloor.
\]
Add isolated vertices up to \(N_s\), then enlarge to a saturated
shifted family \(\mathcal G\supseteq\F\) with the same matching
number, as in Section \ref{sec:fulltrace}. The matching avoiding
vertex 1 persists, so \(\mathcal G\) is ONE. At this new parameter,
\(q_*=\lfloor(s-1)/2\rfloor\ge2\), and Theorem \ref{an:thm:clique}
gives \(|\mathcal G|\le A_4(s)=|\F|\).
Thus no edges were added and the preceding argument identifies
\(\F\) with the clique. This also treats \(q=1\) without applying
the incidence inequalities at that boundary.
\end{proof}
This equality statement uses the strict anchor, while the constants
\(71,143\) retain the stronger hypotheses of
Theorem \ref{thm:cliquestability}.

\begin{lemma}[Inverting a shift at a complete clique]\label{lem:undo-clique}
Let \(s\ge2\), \(|T|=4s+3\), and \(\nu(\mathcal H)\le s\).
If \(S_{ij}(\mathcal H)=\binom T4\), then \(\mathcal H\)
is a complete clique on \(4s+3\) vertices.
\end{lemma}
\begin{proof}
A shift preserves the number of edges in each \(i/j\)-exchange orbit.
If \(i,j\) are both in \(T\) or both outside, all orbits are forced.
The case \(j\in T,i\notin T\) is impossible because the image of
\(S_{ij}\) is fixed by that shift.
Suppose \(i\in T,j\notin T\), and put
\(R=T\setminus\{i\}\), so \(|R|=4s+2\ge10\).
Every quadruple of \(R\) is forced present. For each triple
\(U\subset R\), precisely one of \(\{i\}\cup U,\{j\}\cup U\)
is present; all other types of edges are forced absent.
If both resulting classes are nonempty, they have disjoint
representatives: for intersecting representatives \(U,V\), a triple
outside \(U\cup V\) exists, and its class supplies a disjoint pair
of opposite classes. The corresponding two edges, together with
a partition of the \(4s-4\) remaining vertices of \(R\) into
\(s-1\) quadruples, give a forbidden matching.
Thus one class is empty, identifying one of the two complete cliques.
\end{proof}

\begin{corollary}[Arbitrary extremizers strictly below the crossing]
\label{cor:cliqueextremizers}
For \(s\ge25\), \(4s+4\le n<a_s\), and \(\nu(\F)\le s\),
equality \(|\F|=A_4(s)\) holds if and only if \(\F\)
is a complete clique on \(4s+3\) vertices.
\end{corollary}
\begin{proof}
Shift an extremal family to \(\F'\).
Its matching number is exactly \(s\): otherwise adding a missing
edge keeps matching at most \(s\), contradicting
Theorem \ref{thm:global}. A missing edge exists since \(n\ge4s+4\).
If ONE fails, delete vertex 1; the global theorem bounds the
remainder by \(M(n-1,s-1)\).
In the cover case, restoring all possible incident edges gives
\(B_4(n,s)<A_4(s)\).
In the clique case, Lemma \ref{an:lem:crossing} gives
\(n-1\le(9s+3)/2\le5s-2\). The positive polynomial in the proof
of Lemma \ref{lem:direct-deletion} therefore gives
\(A_4(s-1)+\binom{n-1}3<A_4(s)\).
Both contradict extremality, so \(\F'\) is ONE.
Proposition \ref{prop:cliquerigidity25} identifies it with
\(\binom{[4s+3]}4\).
Invert the shifts one at a time by Lemma \ref{lem:undo-clique};
every intermediate family has matching number at most \(s\).
The converse is immediate.
\end{proof}

\subsection{Cover uniqueness near the crossing}
\begin{lemma}[ONE cannot attain the upper cover]\label{lem:oneexclusion}
A shifted ONE family with matching number \(s\) has size strictly
less than \(B_4(n,s)\) if \(5\le s\le121,\ n\ge a_s\),
or if \(s\ge122,\ n\ge a_s+1\).
\end{lemma}
\begin{proof}
The first range is Proposition \ref{prop:allonegaps}.
For \(s\ge122\), suppose equality occurs at \(n>a_s\).
The deficit monotonicity proved there and the global bound force
equality with the cover on \([a_s]\).
Proposition \ref{thm:range92}, after saturation, bounds this ONE
restriction by \(A_4(s)\).
If \(B_4(a_s,s)>A_4(s)\), this is impossible.
In the remaining tie, Theorem \ref{thm:cliquestability} identifies
the restriction as the complete clique on \(K=[4s+3]\).
An edge using a vertex outside \(K\) leaves at least \(4s\)
vertices of \(K\) free, and together with a partition of those
vertices gives a forbidden matching. There are no such edges,
contradicting the strict increase of \(B_4(n,s)\) in \(n\).
\end{proof}

\begin{lemma}[Inverting a shift at a complete cover]\label{lem:undo-shift}
Let \(t\ge2\), \(n\ge4t+4\), and \(\nu(\F)\le t\).
If one usual shift \(S_{ij}\), from \(j\) to \(i<j\), sends \(\F\)
to the complete cover \(\mathcal C_T\) of a \(t\)-set \(T\),
then \(\F\) is a complete cover of some \(t\)-set.
\end{lemma}
\begin{proof}
A shift preserves the number of edges in each \(i/j\)-exchange orbit.
Every fixed orbit and every orbit having zero or two cover edges is
therefore forced. If \(i,j\) are both in \(T\) or both outside it,
this already gives \(\F=\mathcal C_T\).
The case \(j\in T,i\notin T\) is impossible, because the image of
\(S_{ij}\) is fixed by that shift and this cover is not.

Suppose \(i\in T,j\notin T\). Put \(K=T\setminus\{i\}\) and
\(W=[n]\setminus(K\cup\{i,j\})\), so \(m=|W|=n-t-1\ge3t+3\ge9\).
Every edge meeting \(K\) is forced in \(\F\).
For each \(U\in\binom W3\), exactly one of \(\{i\}\cup U\) and
\(\{j\}\cup U\) lies in \(\F\), partitioning the triples into two classes.
If both classes are nonempty, they have disjoint representatives:
start with one of each; if they intersect, a triple outside their
union exists since \(m\ge9\), and its class supplies the required pair.
The resulting two four-edges, together with \(t-1\) edges using
distinct vertices of \(K\) and \(3(t-1)\) vertices of \(W\) outside
those representatives, form a forbidden matching.
The latter vertices exist because \(m-6\ge3(t-1)\).
Thus one class is empty. The forced orbits now identify \(\F\)
as \(\mathcal C_{K\cup\{i\}}\) or \(\mathcal C_{K\cup\{j\}}\).
\end{proof}

\begin{theorem}[Complete covers in an explicit finite domain]
\label{thm:coveruniqueness}
Let \(\nu(\F)\le s\). In each of the following domains,
\(|\F|=B_4(n,s)\) holds if and only if \(\F\) is the complete
cover of an \(s\)-set:
\[
\begin{array}{ll}
 s=5, & n\ge33,\\
 s=6, & n\ge34,\\
 7\le s\le121, & n\ge a_s,\\
 s\ge122, & n\ge a_s+1.
\end{array}
\]
This conclusion additionally uses Frankl's cover-uniqueness theorem
\cite[Theorem 1.1]{Frankl13} to start at \(s=4,\ n\ge32\).
\end{theorem}
\begin{proof}
First \(a_s\ge a_{s-1}+1\) for \(s\ge2\).
By \eqref{eq:coarse-crossing}, \(a_s\le5s+4\).
Writing \(u=s-2\ge0\), direct subtraction gives
\[
 24\left[A_4(s)-A_4(s-1)-\binom{5s+3}3\right]
 =216+2356u+2160u^2+524u^3>0.
\]
Consequently Pascal's identity implies
\[
 B_4(a_s-1,s-1)
 =B_4(a_s,s)-\binom{a_s-1}3>A_4(s-1).
\]
This parameter is admissible, so the crossing claim follows.

Frankl's theorem states cover uniqueness for exact matching \(u\)
when \(n\ge7u+4\). At \(s=4,n\ge32\), apply it to the actual
matching number \(u\le4\). If \(u<4\), the bound
\(B_4(n,u)<B_4(n,4)\) excludes equality (the empty case is immediate).
Set \(e_4=32\), and recursively
\[
 e_s=\begin{cases}
 \max\{e_{s-1}+1,a_s\},&5\le s\le121,\\
 \max\{e_{s-1}+1,a_s+1\},&s\ge122.
 \end{cases}
\]
The crossings \(a_5=26,a_6=31,a_7=35\) give
\(e_5=33,e_6=34,e_7=a_7\).
The crossing increment gives precisely the displayed domains.

Induct on \(s\), and shift an extremal family with \(n\ge e_s\).
Its matching is exactly \(s\), by the missing-edge argument above.
Lemma \ref{lem:oneexclusion} rules out ONE, so deleting vertex 1
leaves a family \(\F_0\) with matching exactly \(s-1\).
Since \(n-1\ge e_{s-1}\), both brackets below are nonnegative:
\[
 B_4(n,s)-|\F|
 =\bigl[B_4(n-1,s-1)-|\F_0|\bigr]
  +\bigl[\binom{n-1}3-\deg_{\F}(1)\bigr].
\]
Equality forces a complete \((s-1)\)-cover on the remaining vertices
by induction, and every four-edge through 1 is present.
This gives a complete \(s\)-cover.
Lemma \ref{lem:undo-shift} inverts each shift in the original family;
its domain \(s\ge2,n\ge4s+4\) is satisfied.
The converse follows from the cover construction.
\end{proof}
These exact-equality conclusions do not imply quantitative stability
for arbitrary families. The crossing itself for \(s\ge122\) and the
remaining small-parameter equality cases are not classified here.

\section{Two elementary applications}\label{sec:applications}
These consequences illustrate the cardinality theorem.
The probabilistic limit already follows from HHL's large-\(s\)
theorem and the classical matching--probability connection
\cite[Conjecture 1.1 and Lemma 3.2]{LMS}.
It is not a new consequence made possible by the small cases.

\begin{corollary}[Finite weights and four i.i.d.\ variables]\label{cor:iid4}
For nonnegative weights \(w_1,\ldots,w_n\), set
\(s=\floor{\sum_iw_i}\). If \(s\ge1\) and \(n\ge4s+4\), at most
\(M(n,s)\) four-subsets have weight sum at least 1.
If \(s=0\), none do.

For independent, identically distributed nonnegative \(X_1,\ldots,X_4\)
with common mean at most \(x\), the supremum over common laws is
\[
 \sup\Pr(X_1+X_2+X_3+X_4\ge1)
 =\begin{cases}
 \max\{1-(1-x)^4,(4x)^4\},&0\le x\le1/4,\\
 1,&x\ge1/4.
 \end{cases}
\]
No classification of all optimizing laws is asserted.
\end{corollary}
\begin{proof}
The weighted four-subsets form a family in which every matching
has size at most the total weight, proving the finite assertion.

For the limit, truncating a variable at 1 preserves the event and
can only lower its mean. Fix \(0<x<1/4\) and
\(0<\varepsilon<1/4-x\), and sample \(N\) truncated variables.
When their empirical mean is at most \(x+\varepsilon\), apply
Theorem \ref{thm:global} with \(s_N=\floor{N(x+\varepsilon)}\);
\(N\ge4s_N+4\) and \(s_N\ge1\) hold for sufficiently large \(N\).
The expected density of the resulting four-graph is the probability
in question. Chebyshev's inequality, using variance at most \(1/4\),
gives
\[
 \Pr(X_1+\cdots+X_4\ge1)
 \le\frac{M(N,s_N)}{\binom N4}+\frac1{4N\varepsilon^2}.
\]
Let \(N\to\infty\), then \(\varepsilon\downarrow0\).
The ratios converge to the two displayed terms.
The laws \((1-x)\delta_0+x\delta_1\) and
\((1-4x)\delta_0+4x\delta_{1/4}\) attain them.
The boundary values and \(x>1/4\) follow directly.
Since \(s_N\to\infty\), HHL's threshold \(s_N\ge6961\) would
also suffice throughout this limit argument.
\end{proof}

\begin{corollary}[An explicit supersaturation bound]\label{cor:supersaturation}
Let \(s\ge1\), \(n\ge m\ge4(s+1)\), and let \(L_{s+1}(\F)\)
count unordered matchings of \(s+1\) edges in \(\F\subseteq\binom{[n]}4\).
Then
\[
 L_{s+1}(\F)\ge
 \max\left\{0,\left\lceil
 \frac{|\F|\binom{n-4}{m-4}-M(m,s)\binom nm}
 {\binom{n-4(s+1)}{m-4(s+1)}}
 \right\rceil\right\}.
\]
One may maximize over the integer choices of \(m\).
\end{corollary}
\begin{proof}
For each \(m\)-set \(V\), choose one edge from every forbidden
matching in \(\F[V]\), and remove the union of these chosen edges.
At most \(L_{s+1}(\F[V])\) edges are removed; the remaining family
has matching number at most \(s\).
Theorem \ref{thm:global} gives
\(L_{s+1}(\F[V])\ge|\F[V]|-M(m,s)\).
Summing over \(V\), each edge is counted \(\binom{n-4}{m-4}\) times
and each unordered matching is counted
\(\binom{n-4(s+1)}{m-4(s+1)}\) times. Divide and round upward.
\end{proof}
For example, \(n=30,s=2,|\F|=15000,m=13\) gives at least
42261542 unordered three-edge matchings.
This is the usual deletion and double-counting argument; no
optimality or new general supersaturation principle is claimed.

\section{Comparison with earlier results}\label{sec:literature}
\subsection{Cardinality and the finite-board method}
Table \ref{tab:antecedents} separates the ranges of the principal
antecedents. The theorem locators refer to the identified preprint
versions where the published text has not been checked in full.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.24\linewidth}>{\raggedright\arraybackslash}p{.29\linewidth}>{\raggedright\arraybackslash}p{.41\linewidth}@{}}
\toprule
Source & Domain & Relation to this paper\\
\midrule
Frankl \cite{Frankl17}, Thm.~1.1 &
Uniformity three, all parameters &
Complete earlier uniformity; Prop.~5.1 gives the deletion principle\\[2pt]
FRR \cite{FRR}, Thm.~1 &
Uniformity three, \(s\ge33\) &
Short proof; the restricted triple bound is used only in Appendix~\ref{app:local}\\[2pt]
HHL \cite{HHL}, Thm.~1.1 &
Uniformity four, \(s\ge6961\), all admissible \(n\) &
Board framework and exact computations developed here for all \(s\)\\[2pt]
FLMW \cite{FLMW}, Thm.~1.2;
CLZ \cite{CLZ}, Thm.~1.2 &
Uniformity four, sufficiently large parameters, \(n\ge5s\) &
Cover-side range; does not cover every crossing parameter\\[2pt]
Guo--Lu \cite{GuoLu}, Thm.~1.3, Cor.~1.5 &
\(s>s_0(k)\), \(ks+k\le n\le(1+\beta)ks+k-2\) &
Arbitrary-family clique-side containment above their density threshold\\[2pt]
SciNet \cite{SciNet} &
Four finite critical points &
Earlier reports of \(385,1379,3876,4255\); their solvers are not imported\\
\bottomrule
\end{tabular}
\caption{Statement-level comparison. Asymptotic constants and
restricted family classes are not interchangeable with explicit finite
thresholds. The table does not establish an exhaustive priority claim.}
\label{tab:antecedents}
\end{table}

Frankl's later author copy \cite[Section 13, Theorem 13.2]{Frankl17}
also announces the four-uniform conjecture for sufficiently large
matching number, with a proof deferred to future work.
That announcement is an antecedent distinct from a proof supplied in
that text and from the all-parameter conclusion here.
The direct-deletion and ONE reductions are attributed at their use;
the polynomial proof in Lemma \ref{lem:direct-deletion} is retained
for its explicit strict inequality.
The withdrawn complete-solution claim \cite{Mishra} is not a theorem
input; its withdrawal does not determine another work's priority.

Our finite certificates couple the selected-residual constraints with
actual local order, integer orbit counts, support costs and rectangle
persistence. The exact-trace and selected-residual mechanisms follow
\cite[Sections 2 and 4]{HHL}. The support census, support maxima and
residual-row method likewise have HHL antecedents.
HHL's C3 gives the rectangle cap \(96/4\) through 66 missing points;
Lemma \ref{lem:persistence92} extends it to 75 under its displayed
premises. Neither averaging nor orbit-count integrality is proposed
as a new general principle.

\subsection{Clique-side structure}
Guo--Lu \cite[Theorem 1.3 and Corollary 1.5, arXiv v1]{GuoLu}
work for \(k\ge3\), sufficiently large \(s\), and
\(ks+k\le n\le(1+\beta)ks+k-2\), with \(\beta>0\) depending on \(k\).
Their non-trivial families have no isolated vertices. Above the maximum
sizes of their two explicit non-trivial constructions, an arbitrary
family with \(\nu\le s\) is contained in a clique on \(ks+k-1\) vertices.
This is a directly relevant, stronger conclusion in its density regime.
Theorem \ref{thm:cliquestability} instead gives a linear deficit bound
with constants \(71,143\) and cutoff \(s\ge122\), under shifted ONE
and throughout its stated crossing interval. It does not transfer
that quantitative estimate to arbitrary families.
The results have different hypotheses and types of control;
neither an automatic absorption nor overall novelty follows from
this comparison.

\subsection{Local stability and weighted graphs}
The section and shadow decomposition follows Frankl
\cite[Sections 3--5]{Frankl13}. Nested weighted section estimates and
canonical diversity have established antecedents
\cite[Section 8]{FK}. The finite variance is imported from that paper;
its Theorem 32 already gives the asymptotic coefficient \(5.74\) in
uniformity four. Proposition \ref{prop:uniform} supplies an explicit
cutoff using the inequalities displayed here.
Wang \cite[Lemmas 2.1--2.2, 3.2 and proof of Theorem 1.2]{Wang}
provides the graph compression and the container/convexity antecedent.
For the signed functional \(K_3-\lambda e\), completing a graph to a
container need not increase its value; the weighted count in
Lemma \ref{lem:graphs} is therefore retained.

A direct stability comparison is Frankl--Lu--Ma--Wu
\cite[Definition 1.4 and Theorem 1.5]{FLMW}.
For fixed \(c_0\in(0,1/5)\), sufficiently small
\(\varepsilon>0\) depending on \(c_0\), and
\(n\ge n_0(\varepsilon,c_0)\), their theorem applies when
\(c_0n\le t\le n/5\) and gives, for shifted families with \(\nu(\F)\le t\),
\[
 d_t(\F)\le\varepsilon n^4
 \quad\Longrightarrow\quad
 |\mathcal C_t\setminus\F|<400\varepsilon^{1/4}n^4.
\]
Their distance is asymmetric. Our conclusions instead give
\(|\mathcal C_t\setminus\F|\le(K+1)d_t(\F)\), with explicit \(K\)
and bases. The asymptotic theorem has a wider ground-set domain;
its stated cutoff does not certify each finite base here, and its
quantifiers do not justify sending \(\varepsilon\) to zero at fixed \(n\).
Their cardinality Theorem 1.2 does have an explicit threshold:
the end of their Section 4 gives \(n_0=10^{10^7}\), together with
\(n\ge5t\). This does not certify our finite bases; the stability theorem
retains its separate dependence on \(\varepsilon\) and \(c_0\).

Cao--Liu--Zhang \cite[Theorem 1.4]{CLZ} prove stability for arbitrary
families in every compact subinterval of \(0<t/n\le1/5\):
given a distance tolerance, a sufficiently small density deficit and a
sufficiently large \(n\) force small symmetric difference from some cover.
Their Theorem 1.2 also classifies exact extremizers for all
\(t\ge t_0(4)\), \(n\ge5t\). Thus the qualitative form of
Corollary \ref{cor:extremizers} is already available in a wider asymptotic
range. Their revised version of 7 September 2026 retains these
four-uniform statements; the displayed coefficient \(k+0.6\) is stated
for uniformity \(k\ge5\). Its parameterized conclusions still require
sufficiently large matching number. The contribution here is its explicit finite domain together with
the linear shifted estimates; no all-domain improvement is asserted.

Frankl's uniqueness statement at \(n\ge7t+4\)
\cite[Theorem 1.1]{Frankl13} and the finite hypothesis of
Frankl--Kupavskii \cite[Theorem 3]{FKStability}, which here requires
\(n\ge12t+8\), do not include our bases.
Their diversity theorem \cite[Section 7, Theorem 28]{FKDiversity}
has a sufficiently-large-\(n\) hypothesis.
The displayed estimates do not resolve the general diversity problem,
and no novelty is attributed to shifted completion, reverse shifting,
or the classical clique-cap theorem.

The compatibility argument in Section \ref{sec:ht} averages constraints
from all submatchings of one matching, then uses the same deficit to
bound every later link. The density-adapted centre in
Lemma \ref{lem:adapted} preserves the two-endpoint proof while sharpening
the bound. These two ingredients account for the smaller finite bases, including
the additional points \((2904,15676)\), \((888,4798)\), \((360,1950)\),
\((72,395)\), and, with the one-sided variance and all-weight graph bound,
\((49,269)\).
The first-deficit example has a nonempty tail of nonpositive
weight; it does not establish sharpness for a positive tail.
The constants and cutoffs are sufficient, not optimal.
Proposition \ref{prop:quantprop} extends shifted stability above a base
with a growing coefficient by monotonicity of the deficit and double counting.
It is an elementary consequence of the base theorem; no priority is claimed
for this propagation principle. Quantitative transfer through arbitrary
shifts would require additional arguments.
\section{Computational specifications and reproducibility}\label{sec:reproduce}
\subsection{Verification command and scope}
The computational supplement has one verification entry point:
\begin{verbatim}
python -X utf8 -S -B scripts/verify.py
    --hhl-bundle EMC_certificate.zip --zig PATH_TO_ZIG
    --node PATH_TO_NODE --output build/check
\end{verbatim}
The displayed lines form one command, run from the repository root.
It uses standard-library Python 3.12 or later, Zig 0.16.0 and Node 24.
The dependencies and hash-pinned HHL archive are supplied before the
offline verification. No optimization solver is needed to check the
certificates.

The default command verifies every computational component of this
article. It recompiles and executes C1 and all seven consumed C2 cases,
checks the support and layer inequalities, verifies the four small
points, the 51 endpoint records and two fixed inequalities used for
cardinality, and checks their polynomial propagation. It also verifies
all 88 endpoint records retained for the structural results and the
stronger stability weights. It extracts the 68 strict upper margins and
then verifies the seven computational components of Appendix \ref{app:local},
including their stability normalizations. Complete success emits
\begin{center}\small\ttfamily
PASS\_ALL\_ARTICLE\_COMPUTATIONS.
\end{center}
Missing or changed inputs, failed processes, incomplete coverage,
malformed output and timeouts prevent this marker.
The new output directory contains a receipt, complete process logs
and the exact endpoint bounds. Failure controls are supplied in
\texttt{tests/}.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.22\linewidth}>{\raggedright\arraybackslash}p{.35\linewidth}>{\raggedright\arraybackslash}p{.37\linewidth}@{}}
\toprule
Obligation & Mathematical specification & Computational evidence\\
\midrule
C1 and seven C2 cases &
Lemma \ref{lem:no-topstar-finite} &
Exhaustive C++ searches; thresholds and complete transcripts\\[2pt]
Support facets and layer costs &
Lemmas \ref{lem:support-semantic}--\ref{lem:integer-topstar};
Proposition \ref{prop:wide-layer} &
Finite support census, 21 signed facets and integer-orbit tree\\[2pt]
Residual inequalities &
Lemma \ref{lem:lower} &
31 primitive rows, 54528 labelled transports\\[2pt]
Small critical inputs &
Proposition \ref{prop:small} &
Four labelled trees, 94 exact dual leaves\\[2pt]
Intermediate inputs &
Section \ref{app:global} &
15 ordinary and 3 minimum-preserving records; 33 order trees\\[2pt]
Analytic propagation &
Section \ref{sec:assembly92} &
Two fixed inequalities; four-column anchor checks and exact polynomial identities\\
\bottomrule
\end{tabular}
\caption{Computations needed by the global cardinality proof.
Exact row arithmetic is separated from the mathematical proof that
every actual configuration satisfies those rows.}
\label{tab:computations}
\end{table}

The rational checkers reconstruct the labelled universes, transports
and row bounds. Multiplier rounding occurs only after the full global
multiplicity is applied. Certificates are compressed JSON files grouped
by cases and lemmas in \texttt{certificates/}; their mathematical formats
are documented there. Verification code is in \texttt{emc4/}.
The 37 other ordinary upper records remain distributed to check the structural
gap claims, including all 68 upper gaps for $5\le s\le72$.
The replay also checks the 49 gap subtractions for $73\le s\le121$
and the stronger coefficient bounds used by Lemma \ref{lem:weightsmall}.
Thus the 53-obligation count describes the intermediate cardinality
argument, not the number of computations in the complete article.

The root \texttt{REPRODUCE.md} gives dependencies, commands, expected
results and instructions for rebuilding the paper.

The option \texttt{--scope global} restricts verification to
Table \ref{tab:computations} and these structural gap and weight checks, and reports
\texttt{PASS\_\allowbreak GLOBAL\_\allowbreak COMPUTATIONS}.
The option \texttt{--scope appendices} runs the additional computations
below using Python alone and reports
\texttt{PASS\_\allowbreak APPENDIX\_\allowbreak COMPUTATIONS}.
Both restricted modes explicitly report that the whole article has
not been checked.

\subsection{Additional computations in the appendices}
The local estimates do not serve as inputs to Theorem \ref{thm:global}.
Their computational groups are:
\begin{center}\small
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{.69\linewidth}>{\raggedright\arraybackslash}p{.25\linewidth}@{}}
\toprule
Local assertion & Verification group\\
\midrule
252 bases, 504 moment endpoints; factor 4692 & \texttt{local252}\\[2pt]
Uniform base \(\lceil5.74t\rceil,\ t\ge2200\); factor 2285 &
\texttt{uniform}\\[2pt]
Bases \((2904,15676)\), \((888,4798)\), \((360,1950)\);
factors 1427, 601, 319 &
\texttt{local2904}, \texttt{local888}, \texttt{local360}\\[2pt]
Base \((72,395)\); factor 148 & \texttt{local72}\\[2pt]
Base \((49,269)\); factor 160 & \texttt{local49}\\
\bottomrule
\end{tabular}
\end{center}
The moment checks reconstruct all specified cuts and intervals,
then substitute the strict margins into the stability formula.
The uniform result is checked through coefficient signs rather than
a sample of parameter values.

Replaying C1/C2 relies on the correctness of the credited implementations.
The trace reductions, necessity of the constraints, graph inequalities,
shifting arguments and induction are proved in this paper. Their
mathematical validity is not a conclusion of a software success marker.

\subsection{Authorship, assistance and materials}
The author directed the research programme and selected its scope.
AI systems were used extensively to explore proof approaches,
propose lemmas and counterchecks, generate certificate and verification
code, draft and revise text, and conduct adversarial reviews.
Additional AI-assisted calculations supplied by the author were checked
against the proofs and exact computations. They include the common-board
polynomial propagation, the two fixed inequalities, and the direct dense
support constructions incorporated here.
This assistance includes scientific and computational work, not only
language editing. Agent reviews are not independent specialist
acceptance; the proofs and identified computations carry the justification.

The computational supplement consists of verification programs,
exact certificates, documented expected results and file hashes.
HHL methods and programs retain their attribution; the pinned external
archive and its applicable terms are specified separately in the supplement.
The supplement contains the source and PDF of this article together with
instructions for rebuilding the paper and reproducing the computations.

\appendix
\section{Effective shifted stability and weighted graph bounds}\label{app:local}
This appendix preserves the local results and their proofs as a
complement to Theorem \ref{thm:global}. They do not use finite HHL board
certificates, and the global proof does not use their estimates.
Here \(t\) denotes the allowed matching number.
The additional quantitative inputs appear in
Section \ref{sec:localimports}.

\subsection{Statements and proof route}\label{sec:localresults}
For a family \(\F\subseteq\binom{[n]}4\), define its deficit and \(t\)-diversity by
\[
 d_t(\F)=B_4(n,t)-|\F|,\qquad
 \gamma_t(\F)=\min_{\substack{S\subseteq[n]\\|S|=t}}
       |\{E\in\F:E\cap S=\varnothing\}|.
\]
For shifted families, \([t]\) attains this minimum.
The first local result gives a finite, linear relation between these quantities.

\begin{theorem}[Effective shifted stability]\label{thm:uniform}
Let \(t\ge2200\), \(n=\ceil{287t/50}\), and let
\(\F\subseteq\binom{[n]}4\) be shifted with \(\nu(\F)\le t\).
Then \(d=d_t(\F)\ge0\) and
\[
 \gamma_t(\F)=|\F\setminus\mathcal C_t|\le2285d,\qquad
 |\F\mathbin{\triangle}\mathcal C_t|\le4571d.
\]
\end{theorem}

A more detailed estimate is useful when the number of vertices is reduced.
A matching in a tail link forces missing head triples on every residual
set obtained by selecting some of its pairs. Averaging these constraints
and adapting the moment centre produces the next finite refinement.

\begin{theorem}[Smaller finite bases]\label{thm:finite}
Let \((t,n,K)\) be one of the following choices:
\[
 \begin{aligned}
 (t,n,K)&\in\{(49,269,160),(72,395,148),(360,1950,319),\\
         &\qquad (888,4798,601),(2904,15676,1427)\},\\
 (n,K)&=(t+15301,4692)\qquad(3229\le t\le3480).
 \end{aligned}
\]
Every shifted \(\F\subseteq\binom{[n]}4\) with \(\nu(\F)\le t\)
satisfies \(d=d_t(\F)\ge0\) and
\[
 \gamma_t(\F)=|\F\setminus\mathcal C_t|\le Kd,\qquad
 |\F\mathbin{\triangle}\mathcal C_t|\le(1+2K)d.
\]
\end{theorem}

The 252 bases in the interval have between 5 and 1195 fewer vertices
than \(\ceil{287t/50}\). The additional base at \(t=2904\) has 993 fewer
vertices than the uniform base 16669, and symmetric-difference factor 2855.
The bases at \(t=888\), \(t=360\), \(t=72\) and \(t=49\) give
symmetric-difference factors 1203, 639, 297 and 321, respectively. The uniform theorem is not invoked
at these smaller matching parameters. The five isolated bases have
different values of \(t\); factor 148 does not replace another factor
at a fixed matching parameter; neither does the factor 160 at \(t=49\).
The constants apply to their stated ground sets and are not asserted optimal. Taking \(d=0\) gives shifted uniqueness
at the bases. This qualitative conclusion extends as follows.

\begin{corollary}[Exact extremizers above the bases]\label{cor:extremizers}
Suppose \(t\ge2200,\ n\ge\ceil{287t/50}\), or
\(3229\le t\le3480,\ n\ge t+15301\), or \(t=2904,\ n\ge15676\),
or \(t=888,\ n\ge4798\), or \(t=360,\ n\ge1950\),
or \(t=72,\ n\ge395\), or \(t=49,\ n\ge269\).
Every \(\F\subseteq\binom{[n]}4\) with \(\nu(\F)\le t\) satisfies
\(|\F|\le B_4(n,t)\), with equality if and only if
\(\F=\mathcal C_T(n)\) for some \(t\)-set \(T\).
\end{corollary}

\begin{corollary}[Shifted stability above a base]\label{cor:alln}
Let \((a,K)\) be any of the following base pairs:
\[
 \begin{aligned}
 (a,K)&=\bigl(\ceil{287t/50},2285\bigr) &&(t\ge2200),\\
 (a,K)&=(t+15301,4692) &&(3229\le t\le3480),\\
 (a,K)&=(15676,1427) &&(t=2904),\\
 (a,K)&=(4798,601) &&(t=888),\\
 (a,K)&=(1950,319) &&(t=360),\\
 (a,K)&=(395,148) &&(t=72),\\
 (a,K)&=(269,160) &&(t=49).
 \end{aligned}
\]
For every \(n\ge a\) and shifted \(\F\subseteq\binom{[n]}4\) with
\(\nu(\F)\le t\), put \(R=\binom{n-t}4/\binom{a-t}4\). Then
\[
 d_t(\F)\ge0,\qquad
 \gamma_t(\F)\le KR\,d_t(\F),\qquad
 |\F\mathbin{\triangle}\mathcal C_t|\le(1+2KR)d_t(\F).
\]
Where several base pairs are available, their smallest applicable coefficient
may be used.
\end{corollary}

The loss is explicit: at fixed \(t\) it grows as \((n-t)^4\).
For example, \(t=3480\), \(a=18781\) and \(n=19000\) give
\(\gamma_t(\F)\le4967d_t(\F)\), before the uniform base \(19976\).
The constants 2285, 4692, 1427, 601, 319, 148 and 160 are asserted at their bases;
the quantitative result still requires shiftedness.


The proof starts with the section and shadow method of Frankl
\cite{Frankl13} and the finite variance estimate of Frankl--Kupavskii
\cite{FK}. Sections \ref{sec:moments}--\ref{sec:graphs} prove the uniform
estimate. Sections \ref{sec:ht}--\ref{sec:certificate} give the finite
refinement and quantitative propagation; Section \ref{sec:equality}
handles exact equality and inversion of shifts.
The weighted graph Lemma \ref{lem:graphs} determines an exact maximum
for \(K_3(G)-\lambda e(G)\) on its displayed interval, and is also useful
as a separate technical result. Section \ref{sec:literature} distinguishes
these finite linear estimates from the broader asymptotic literature.

\subsection{Additional inputs for the local results}\label{sec:localimports}
The shadow theorem was stated in Section \ref{sec:imports}.
The following inputs are used only in this appendix.

\paragraph{Triple systems.}
Frankl--R\"odl--Ruci\'nski \cite[Theorem 1]{FRR} gives, for
\(u\ge33\), \(N\ge3u+3\) and matching number exactly \(u\),
\[
 |\A|\le\max\left\{\binom{3u+2}3,B_3(N,u)\right\}.
\]
To extend it to matching number at most \(u\), add edges until the first
family with matching number \(u\). A single added edge increases the
matching number by at most one, and the complete family has sufficient
matching capacity. Further,
\[
 B_3(4u-1,u)-\binom{3u+2}3=\frac{u(10u^2-69u+5)}6>0\quad(u\ge33).
\]
Indeed the numerator at \(u=33+x\) is
\(10x^3+921x^2+28121x+284394\).
Monotonicity in \(N\) therefore yields
\begin{equation}\label{eq:triple}
 \nu(\A)\le u,\quad u\ge33,\quad N\ge4u-1
 \quad\Longrightarrow\quad |\A|\le B_3(N,u).
\end{equation}
For smaller residual ground sets we retain the full maximum in FRR.

\paragraph{Finite variance.}
For a uniformly random matching \(\BB\) of \(v\) triples on \([m]\),
where \(m\ge3v\), let \(Z=|\A\cap\BB|\) and
\(\mu=v|\A|/\binom m3\). The finite estimate in
\cite[Lemma 10, Proposition 11 and equation (20)]{FK} is
\begin{equation}\label{eq:variance}
 \Var Z\le2\mu(1-\mu/v).
\end{equation}
No asymptotic threshold from that paper is used in the proof.

\paragraph{Clique cap.}
The Lov\'asz form of Kruskal--Katona, stated in
\cite[Theorem 1]{Keevash}, says that if
\(|\A_0|=\binom x3>0\), \(x\ge3\), then
\begin{equation}\label{eq:kk}
 K_4(\A_0)\le\binom x4=\frac{x-3}{4}|\A_0|.
\end{equation}

\paragraph{Graph compression.}
For graphs, compression preserves the number of edges, does not increase
the matching number and does not decrease the number of triangles
\cite[Lemmas 2.1--2.2]{Wang}. Thus it does not decrease
\(K_3(G)-\lambda e(G)\). This permits the weighted proof in
Section \ref{sec:graphs} to be carried out on stable graphs.

\begin{lemma}[One-sided Kneser variance]\label{lem:variance-one-sided}
Let \(m\ge6\), \(v\ge1\) and \(3v\le m\). For any triple family
\(\A\subseteq\binom{[m]}3\) and a uniformly random matching \(\BB\)
of \(v\) triples, put \(Z=|\A\cap\BB|\) and
\(\mu=v|\A|/\binom m3\). Then
\begin{equation}\label{eq:variance-one-sided}
 \Var Z\le\rho_{m,v}\mu(1-\mu/v),\qquad
 \rho_{m,v}=1+\frac{6(v-1)}{(m-3)(m-4)}.
\end{equation}
\end{lemma}
\begin{proof}
Give functions on \(\binom{[m]}3\) the uniform inner product.
Let \(K\) be the adjacency operator for disjoint triples, of degree
\(d=\binom{m-3}3\), and put \(g_J(T)=1_{J\subseteq T}\).
Let \(V_j\) be the span of these indicators for \(|J|=j\).
The spaces are nested, \(V_0\) consists of constants, and \(V_3\)
is the whole function space. Direct counting and inclusion--exclusion give
\[
 (Kg_J)(T)=\binom{m-3-j}{3-j}1_{J\cap T=\varnothing}
 =\binom{m-3-j}{3-j}\sum_{I\subseteq J}(-1)^{|I|}g_I(T).
\]
Thus \(K\) acts on \(V_j/V_{j-1}\) by
\((-1)^j\binom{m-3-j}{3-j}\). Since \(K\) is self-adjoint,
the orthogonal differences give an eigenspace decomposition.
The nonconstant eigenvalues are
\(-\binom{m-4}2,\ m-5,\ -1\); their largest algebraic value is \(m-5\).
For \(f=1_\A-\alpha\), \(\alpha=|\A|/\binom m3\), this yields
\[
 \frac{\langle f,Kf\rangle}{d}
 \le\frac{m-5}{d}\alpha(1-\alpha).
\]
Two distinct positions of a random matching are uniform disjoint triples.
Adding the \(v\) variances and \(v(v-1)\) covariances gives
\[
 \Var Z\le v\alpha(1-\alpha)
       \left(1+(v-1)\frac{m-5}{d}\right),
\]
which is \eqref{eq:variance-one-sided}. The case \(v=1\) is immediate.
\end{proof}
This uses the Kneser spectral method underlying \cite{FK}.
For this upper bound the largest algebraic eigenvalue suffices;
the larger absolute value of a negative eigenvalue need not be used.
We retain \eqref{eq:variance} for the other numerical arguments
and use \eqref{eq:variance-one-sided} only where specified.

\subsection{Sections and shifted completion}\label{sec:sections}
Recall the elementary shifted-completion Lemma \ref{lem:completion}.

Fix \(t\ge1\), \(n\ge4t+4\), and a stable family \(\F\) with \(\nu(\F)=t\).
A stable family of exact matching number \(t\) contains the complete
four-graph on \([t+3]\). Indeed an edge of a maximum matching avoids
\([t-1]\), hence dominates \(\{t,t+1,t+2,t+3\}\).
Define
\[
 X=[t+1],\quad Y=[t+2,n],\quad m=|Y|,\quad
 c=t-\floor{(t+1)/4},
\]
\[
 \HH=\F\cap\binom Y4,\qquad
 \A_i=\{T\in\binom Y3:T\cup\{i\}\in\F\},\quad
 \A=\A_{t+1}.
\]
These sections meet \(X\) in exactly one vertex. They are nested:
\(\A_1\supseteq\cdots\supseteq\A_{t+1}\), and cross-dependent, since
disjoint representatives would complete to \(t+1\) disjoint four-edges.
In particular \(\nu(\A)\le t\).
The packing inside \(X\) gives \(\nu(\HH)\le c\); stability gives
\(\partial\HH\subseteq\A\). Thus
\begin{equation}\label{eq:twoH}
 |\HH|\le c|\A|,\qquad |\HH|\le K_4(\A).
\end{equation}
All sections with at least two vertices in \(X\) already meet \([t]\).
It therefore suffices to prove
\begin{equation}\label{eq:sectiongoal}
 |\HH|+\sum_{i=1}^{t+1}|\A_i|\le t\binom m3.
\end{equation}

\begin{lemma}[Deficit and canonical diversity]\label{lem:accounting}
For the sections above, put \(C=\binom m3\) and \(d=B_4(n,t)-|\F|\).
Then
\[
 d\ge tC-|\HH|-\sum_{i=1}^{t+1}|\A_i|,\qquad
 \gamma_t(\F)=|\F\setminus\mathcal C_t|=|\HH|+|\A|
 \le(c+1)|\A|.
\]
Moreover, for every shifted family,
\[
 |\mathcal C_t\setminus\F|=d+|\F\setminus\mathcal C_t|,\qquad
 |\F\mathbin{\triangle}\mathcal C_t|=d+2|\F\setminus\mathcal C_t|.
\]
\end{lemma}
\begin{proof}
The cover has all \(tC\) sections meeting \(X\) exactly once through
\([t]\); every section with at least two vertices in \(X\) already meets
\([t]\). Its deficit on these latter sections is nonnegative, proving
the first inequality. The edges avoiding \([t]\) are exactly \(\HH\)
and the section \(\A=\A_{t+1}\).
To see that \([t]\) minimizes diversity, write
\([n]\setminus S=\{u_1<\cdots<u_{n-t}\}\); then \(u_i\le t+i\).
Coordinatewise lowering \(t+i\mapsto u_i\) injects the edges avoiding
\([t]\) into those avoiding \(S\).
The last two identities follow by subtracting cardinalities and hold
without any matching assumption.
\end{proof}

\begin{lemma}[Nested incidence]\label{lem:nested}
On a matching of \(v\) triples, let
\(d_1\ge\cdots\ge d_{t+1}=z\) count membership in the sections.
For every real \(w\), some \(j\in[z,t]\) satisfies
\begin{equation}\label{eq:nested}
 W-tv\le j(j-v)+wz,\qquad W=\sum_{i=1}^t d_i+wz .
\end{equation}
\end{lemma}
\begin{proof}
Nested neighbourhoods have distinct representatives if
\(d_i\ge t+2-i\) for every \(i\), by assignment starting with the last row.
Cross-dependence therefore gives \(d_{t+1-j}\le j\) for some
\(0\le j\le t\). Nesting implies \(z\le j\).
The first \(t-j\) rows have size at most \(v\), and the remaining \(j\)
of the first \(t\) rows have size at most \(j\). This proves the bound.
\end{proof}

\subsection{A centered moment inequality}\label{sec:moments}
Suppose
\[
 m\ge3v,\qquad t+1\le v\le2t,\qquad y=v-t,\qquad
 0<b\le v,\qquad bv\ge2ty .
\]
Convexity in \(j\) in \eqref{eq:nested} yields
\[
 W-tv\le G_w(z):=\max\{z(z+w-v),-ty+wz\},\qquad 0\le z\le t.
\]
Put \(\kappa=ty/b^2\). The quadratic
\[
 Q_w(z)=wz-ty+\kappa(z-b)^2
       =\kappa z^2+(w-2ty/b)z
\]
dominates both branches. Its difference from the linear branch is a
square; its difference from the other branch is
\(z[(\kappa-1)z+v-2ty/b]\).
The bracket is affine in \(z\), nonnegative at zero by hypothesis, and
equals \(y(t/b-1)^2\) at \(t\).

Using \eqref{eq:variance}, with \(C=\binom m3\) and
\(\mu=v|\A|/C\), we get
\begin{equation}\label{eq:Phi}
 \E(W-tv)\le\Phi_w(\mu)
 :=\kappa(1-2/v)\mu^2+(w-2ty/b+2\kappa)\mu .
\end{equation}
This is convex, including the limiting case \(v=2\).
If \(\mu\le b\), \(\Phi_w(0)=0\), and
\begin{equation}\label{eq:M}
 M_w:=ty-wb-\frac{2ty}{b}(1-b/v)\ge0,
\end{equation}
then \(\Phi_w(\mu)\le0\), since \(\Phi_w(b)=-M_w\).
Together with \(|\HH|\le(w-1)|\A|\), this proves \eqref{eq:sectiongoal}.

Section \ref{sec:certificate} adapts the centre to the actual mean
for the finite refinement, while retaining a two-endpoint reduction.

\subsection{Weighted triangle bounds and a uniform cover range}\label{sec:graphs}
\begin{lemma}\label{lem:graphs}
For an integer \(t\ge1\) and any graph \(G\) with \(\nu(G)\le t\),
\begin{equation}\label{eq:half}
 K_3(G)-\frac{t-1}{2}e(G)\le
 g_{1/2}:=\frac{t(t+1)(2t+1)}6 .
\end{equation}
If its ground set has size \(N\ge2t+1\), then for
\(0\le\lambda\le(t-1)/3\),
\begin{equation}\label{eq:weightedgraph}
\begin{split}
 K_3(G)-\lambda e(G)&\le g_\lambda(t,N)
 :=\max\{C_\lambda(t),J_\lambda(N,t)\},\\
 C_\lambda(t)&=\binom{2t+1}3-\lambda\binom{2t+1}2,\\
 J_\lambda(N,t)&=\binom t3+(N-t)\binom t2
              -\lambda\left[\binom t2+t(N-t)\right].
\end{split}
\end{equation}
In particular,
\begin{equation}\label{eq:third}
 K_3(G)-\frac{t-1}{3}e(G)\le
 \max\left\{\frac{t^2(2t+1)}3,\frac{t(t-1)(N-t-1)}6\right\}.
\end{equation}
\end{lemma}
\begin{proof}
By graph compression, we may assume that \(G\) is stable:
the matching constraint is retained and the functional cannot decrease.
Let \(h_b\) be the number of lower neighbours of vertex \(b\).
They form an initial clique. The left side of \eqref{eq:half} is
\(\frac12\sum_b h_b(h_b-t)\).
For \(b\ge2t+2\), \(h_b\le t\); otherwise the edge \((t+1,b)\)
forces the matching \((i,t+1+i)\), \(1\le i\le t+1\).
If some \(h_b>t\), the initial clique on \(t+1\) vertices contributes
\(-t(t^2-1)/12\). Positive contributions are possible only for
\(t+2\le b\le2t+1\), bounded individually by
\((b-1)(b-1-t)/2\). Their sum is \(t(5t^2+6t+1)/12\).
Adding proves \eqref{eq:half}; if no \(h_b>t\), the sum is nonpositive.

For \eqref{eq:weightedgraph}, the case \(N=2t+1\) follows from
\(3K_3\le(N-2)e\), since \((N-2)/3-\lambda\ge0\).
If \(N\ge2t+2\), one of the disjoint pairs
\((a+1,2t+2-a)\), \(0\le a\le t\), is missing.
Set \(b_0=2t+1-a\). Stability makes the vertices beyond \([b_0]\)
independent, with neighbours contained in \([a]\).
The head contribution is at most
\(\binom{b_0}3-\lambda\binom{b_0}2\): count each head triangle
three times and use \((b_0-2)/3-\lambda\ge0\).
An outside vertex of degree \(h\le a\) contributes at most
\(\binom h2-\lambda h\), whose maximum is
\(\max\{0,\binom a2-\lambda a\}\).
For \(a\le2\lambda+1\) this is zero; the head expression is at most
\(C_\lambda(t)\), since it increases with \(b_0\ge t+1\).
Above the breakpoint the bound becomes
\[
 T(a)=\binom{2t+1-a}3-\lambda\binom{2t+1-a}2
       +(N-2t-1+a)\left(\binom a2-\lambda a\right).
\]
Here \(T''(a)=N+2a-3\lambda-2>0\).
At the joining point the value is at most \(C_\lambda(t)\);
at \(a=t\) it is \(J_\lambda(N,t)\). Convexity proves the assertion,
with an empty second interval omitted. Substitution of
\(\lambda=(t-1)/3\) gives \eqref{eq:third}.
\end{proof}
Both bounds are sharp when \(N\ge2t+1\).
The graph \(K_{2t+1}\) with isolated remaining vertices has matching
number \(t\), \(\binom{2t+1}2\) edges and \(\binom{2t+1}3\) triangles.
It attains \eqref{eq:half} and the first term of \eqref{eq:third}.
The join \(K_t\vee\overline K_{N-t}\) has matching number \(t\) and
\[
 e=\binom t2+t(N-t),\qquad
 K_3=\binom t3+(N-t)\binom t2.
\]
It attains the second term of \eqref{eq:third}.
For every admissible weight, the same two graphs realize the two
terms in \eqref{eq:weightedgraph}. Thus all the displayed bounds are
exact maxima.

\begin{lemma}[A graph bound for all nonnegative weights]\label{lem:graph-all}
For an integer \(u\ge1\), let \(G\) be a graph on \(N\ge2u+1\)
vertices, with \(\lambda\ge0\) and \(\nu(G)\le u\).
Writing \(x_+=\max\{0,x\}\), we have
\begin{equation}\label{eq:graph-all}
\begin{split}
 K_3(G)-\lambda e(G)&\le\widehat g_\lambda(u,N)\\
 &:=\max_{0\le a\le u}\biggl\{
 \left(\binom{2u+1-a}3-\lambda\binom{2u+1-a}2\right)_+\\
 &\qquad +(N-2u-1+a)\left(\binom a2-\lambda a\right)_+
 \biggr\},
\end{split}
\end{equation}
where \(a\) is integral. Set \(\widehat g_\lambda(0,N)=0\).
This is an upper bound; exactness for all weights is not asserted.
\end{lemma}
\begin{proof}
Compress \(G\). If \(N=2u+1\), the triangle incidence bound
\(3K_3\le(N-2)e\) gives the first term with \(a=0\), or zero
when its coefficient is negative.
For \(N\ge2u+2\), the missing pair used in the proof of
Lemma \ref{lem:graphs} gives a head of size \(b=2u+1-a\)
and an independent exterior whose neighbours lie in \([a]\).
On the head, \(3K_3\le(b-2)e\) gives
\(K_3-\lambda e\le(\binom b3-\lambda\binom b2)_+\):
use \(e\le\binom b2\) when the coefficient is nonnegative and zero otherwise.
An exterior vertex of degree \(h\le a\) contributes at most
\(\binom h2-\lambda h\). Convexity in \(h\) bounds it by the
larger endpoint value \(0\) or \(\binom a2-\lambda a\).
Summing and maximizing over \(a\) proves the result.
\end{proof}

For a stable triple family \(\A\) on \([m]\), put \(q=3t+2\) and
\[
 G_j=\{P\in\binom{[j-1]}2:P\cup\{j\}\in\A\}.
\]
For \(j>q\), \(\nu(G_j)\le t\): \(t+1\) disjoint pairs could be
completed to triples using \(t\) free vertices below \(j\), and \(j\)
itself, contradicting \(\nu(\A)\le t\).
Moreover the four-cliques with largest vertex \(j\) are counted
\emph{exactly} by \(K_3(G_j)\). The triple omitting \(j\) is forced by
stability. If \(\A_0=\A\cap\binom{[q]}3\), the elementary head bound
\(4K_4(\A_0)\le(q-3)|\A_0|\) and \eqref{eq:half} give
\begin{equation}\label{eq:Ehalf}
 K_4(\A)\le\frac{t-1}{2}|\A|+E_{1/2}(t,m),\qquad
 E_{1/2}(t,m)=\frac{t+1}{4}\binom{3t+2}3+(m-3t-2)g_{1/2}.
\end{equation}

\begin{proposition}\label{prop:uniform}
For \(t\ge2200\), the cover bound holds for every
\(n\ge\ceil{287t/50}\).
\end{proposition}
\begin{proof}
At \(a=\ceil{287t/50}\), let \(m=a-t-1\),
\(m_0=237t/50-1\), \(m_+=237t/50\).
Then
\[
 m_0\le m<m_+,\quad 79t/50-1\le v=\floor{m/3}\le79t/50,
 \quad 29t/50-1\le y\le29t/50.
\]
For the lower bound on \(v\), use
\(v=\floor{(\ceil{237t/50}-1)/3}\).
All the domains of Section \ref{sec:moments} hold at \(t\ge2200\);
also \(m\ge4t-1\).

Write \(\alpha=|\A|/\binom m3\).
Equation \eqref{eq:triple} implies \(\alpha\le161/316\).
To check this, the ratio
\(\binom{m-t}3/\binom m3=\prod_{i=0}^2(1-t/(m-i))\)
increases with \(m\), and
\[
 316\binom{m_0-t}3-155\binom{m_0}3=P_A(t)/750000,
\]
\[
 P_A(t)=3019933t^3-703202700t^2+614817500t-120750000.
\]
Its coefficients after \(t=2200+x\) are positive
(Appendix \ref{app:polys}).

If \(\alpha>12/25\), \eqref{eq:Ehalf} gives
\(|\HH|\le(23t/32)|\A|\), since
\[
 (7t/32+1/2)(12/25)\binom{m_0}3-E_{1/2}(t,m_+)
 =P_J(t)/150000000>0,
\]
\[
 P_J(t)=23803113t^4-82886156t^3-771716100t^2+309590000t-36000000.
\]
Again the translated coefficients are positive. Use the following
weights and centers in \eqref{eq:M}:
\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
Density range & Upper weight \(w\) & Center \(b\)\\
\midrule
\(0\le\alpha\le12/25\) & \(3t/4+3/2\) & \(474t/625\)\\
\(12/25<\alpha\le161/316\) & \(23t/32+1\) & \(161t/200\)\\
\bottomrule
\end{tabular}
\end{center}
The first weight bounds \(c+1\), by the four residues of \(t+1\)
modulo four. Both centers satisfy \(\mu\le b\le v\).
In the order of the two rows, direct lower bounds are
\begin{align*}
 bv-2ty&\ge\frac{598t^2}{15625},
 & M_w&\ge\frac{7t(474t-124127)}{296250},\\
 bv-2ty&\ge\frac{1119t^2}{10000},
 & M_w&\ge\frac{9t(12719t-22718432)}{81401600}.
\end{align*}
For the first column, write \(bv-2ty=bt+(b-2t)y\) and use the upper
bound on \(y\). For the second, use the lower bound on \(y\) in \(ty\),
the upper bound in the subtracted correction, and respectively
\(1-b/v\le13/25\) or \(155/316\).
All margins are positive for \(t\ge2200\).
Equations \eqref{eq:twoH}, \eqref{eq:Ehalf} and
\eqref{eq:Phi}--\eqref{eq:M} prove the base case.
Shifting and Lemma \ref{lem:completion} cover matching number at most \(t\).
Propagation in \(n\) is proved in Lemma \ref{lem:propagation}.
\end{proof}

\begin{proof}[Proof of Theorem \ref{thm:uniform}]
First assume \(\nu(\F)=t\). Use the sections of Section \ref{sec:sections}; exact matching number
again suffices. In either density range of Proposition \ref{prop:uniform},
the corresponding \(w,b\) give
\[
 \frac vC\left(|\HH|+\sum_i|\A_i|-tC\right)\le\Phi_w(\mu).
\]
For \(0<\mu\le b\), the ratio \(\Phi_w(\mu)/\mu\) is nondecreasing,
because the quadratic coefficient is nonnegative.
Since \(\Phi_w(b)=-M_w\), the section deficit is at least
\((M_w/b)|\A|\).
Dividing the two explicit lower margins in that proposition by their
centers gives, respectively,
\[
 \eta_1(t)=\frac{7(474t-124127)}{224676},\qquad
 \eta_2(t)=\frac{9(12719t-22718432)}{65528288}.
\]
For \(t\ge2200\), we have \(\eta_1>\eta_2>0\) and
\(2285\eta_2\ge3t/4+3/2\ge c+1\).
Here is a direct all-parameter check: after \(t=2200+x\), the
coefficients of these affine expressions are
\[
\begin{array}{c|cc}
 & \text{coefficient of }x & \text{constant}\\ \hline
 \eta_2 & 9/5152 & 5921289/8191036\\
 \eta_1-\eta_2 & 15899/1221024 & 40620105838/1455956649\\
 2285\eta_2-3t/4-3/2 & 16701/5152 & 2649411/8191036
\end{array}
\]
and every entry is positive.
The section accounting and canonical diversity argument of
Lemma \ref{lem:accounting} yield
\(d\ge\eta_2|\A|\) and
\(\gamma_t(\F)\le(c+1)|\A|\le2285d\).
If \(\mu=0\), then \(\A=\HH=\varnothing\), so the same conclusion is
immediate. Lemma \ref{lem:completion} extends the first bound to \(\nu(\F)\le t\); Lemma \ref{lem:accounting} gives the symmetric-difference bound.
\end{proof}

\subsection{Averaged matching deficits and a common tail bound}\label{sec:ht}
Let \(\A\subseteq\binom{[m]}3\) be stable with \(\nu(\A)\le t\), and put
\[
 q=3t+2\le m,\qquad \A_0=\A\cap\binom{[q]}3,\qquad
 \Delta=\binom q3-|\A_0|,\qquad M=m-q .
\]
Use the link graphs \(G_j\) from Section \ref{sec:graphs}.
Recall that \(\nu(G_j)\le t\) for \(j>q\).

A nonempty tail forces \(\{1,2,j\}\) for some \(j>q\).
Every partition of \([3,q]\) into \(t\) triples must then contain
a missing triple. Averaging over uniform partitions gives
\begin{equation}\label{eq:d0}
 \Delta\ge d_0:=\binom{3t-1}2.
\end{equation}

\paragraph{A sharp first deficit.}
On \([q+1]\), define
\[
 \A^*=\left(\binom{[q]}3\setminus
       \{\{a,b,q\}:3\le a<b\le q-1\}\right)
       \cup\{\{1,2,q+1\}\}.
\]
This family is stable and its head deficit is exactly \(d_0\).
A matching avoiding the tail has at most \(t\) edges. If it uses
the tail triple, all remaining triples avoid \(1,2,q\), leaving
\(3t-1\) vertices and at most \(t-1\) further edges.
The complete head on \([q-1]\) contains a \(t\)-matching, so
\(\nu(\A^*)=t\). The sole tail link has one edge and no triangle:
its contribution to \(K_3-\lambda e\) is \(-\lambda\le0\).
Thus \eqref{eq:d0} is sharp for a nonempty tail, without asserting
sharpness of a deficit forced by positive tail weight.

\begin{lemma}[Averaging over submatchings]\label{lem:averaged}
Suppose \(G_{q+L}\) contains a matching of size \(u\), where
\(3\le u\le t\). Let \(1\le r\le\min\{u,L\}\) and \(t-r\ge33\).
Set \(h=q-2u\) and
\[
 V_t(r)=\min\left\{\binom{q-2r}3-\binom{3(t-r)+2}3,
                            \binom{2t+2-r}3\right\}.
\]
\begin{align*}
 n_0&=\binom h3,&
 n_1&=u\left(2\binom h2+h\right),\\
 n_2&=\binom u2(4h+4),&
 n_3&=8\binom u3.
\end{align*}
Put \(p_k=\binom{u-k}r/\binom ur\) for \(0\le k\le3\).
Then
\begin{equation}\label{eq:dualcut}
 \Delta\ge D_t(u,r):=
 \max\left\{0,\ \max_{\substack{0\le k\le3\\p_k>0}}
 \ceil{\frac{V_t(r)-\sum_{i<k}(p_i-p_k)n_i}{p_k}}\right\}.
\end{equation}
\end{lemma}
\begin{proof}
By replacing occupied vertices with smaller unused vertices, shiftedness
places a \(u\)-matching inside \([2u]\).
Fix its \(u\) disjoint pairs. Any \(r\) of them can be completed with
distinct vertices \(q+1,\ldots,q+r\) to disjoint triples of \(\A\).
After deleting their \(2r\) head vertices, the residual triple family
has matching at most \(t-r\) on \(q-2r\) vertices.
The full FRR bound applies, since
\[
 (q-2r)-3(t-r)-3=r-1\ge0,
\]
and forces at least \(V_t(r)\) missing residual triples.
Both FRR branches are retained.

Classify head triples by the number \(k\) of matching pairs they meet.
Their capacities are \(n_k\): for \(k=1\), either one vertex of a
pair or the whole pair is used; for \(k=2\), either two single pair
vertices and one outside vertex, or a whole pair and one other pair
vertex are used. The other two counts are immediate.
Let \(x_k\) be the number of missing triples in class \(k\).
Then \(0\le x_k\le n_k\), \(\Delta=\sum_kx_k\), and a class-\(k\)
triple survives a uniformly chosen \(r\)-submatching with probability
\(p_k\). Averaging gives \(\sum_kp_kx_k\ge V_t(r)\).
Since \(p_0\ge p_1\ge p_2\ge p_3\), for \(p_k>0\),
\[
 V_t(r)\le p_k\Delta+\sum_{i<k}(p_i-p_k)x_i
                    +\sum_{i>k}(p_i-p_k)x_i
 \le p_k\Delta+\sum_{i<k}(p_i-p_k)n_i .
\]
Taking ceilings proves \eqref{eq:dualcut}.
\end{proof}

The bound is necessary; it does not claim that every feasible
four-class profile can be realized by a stable family.
Its useful feature is that the same \(\Delta\) controls every link.

Choose a finite set \(\mathcal T\) of triples \((u,r,D_t(u,r))\)
satisfying Lemma \ref{lem:averaged}, and include the additional
nonempty-tail cut \((1,1,d_0)\).
If \(\Delta<D\), any cut \((u,r,D)\) implies
\(\nu(G_{q+j})\le u-1\) for every \(j\ge r\).
For \(0\le\delta\le\binom q3\), define
\[
 u_\delta(j)=
 \min\bigl(\{t\}\cup\{u-1:(u,r,D)\in\mathcal T,\ r\le j,\ D>\delta\}\bigr).
\]
These are upper bounds for the link matchings, not a realizability claim.

For \(0\le a\le\binom q3\), let \(z(a)\ge3\) be the least integer
with \(\binom{z(a)}3\ge a\), taking \(z(0)=3\), and put
\begin{equation}\label{eq:beta}
 \beta_\lambda(a)=\max\{0,((z(a)-3)/4-\lambda)a\}.
\end{equation}
Equation \eqref{eq:kk} implies
\(K_4(\A_0)-\lambda|\A_0|\le\beta_\lambda(a)\) when
\(|\A_0|\le a\). For a nonnegative coefficient use this cardinality
bound; for a negative coefficient use zero. The function
\(\beta_\lambda\) is nondecreasing.

\begin{proposition}[A common deficit for the tail]\label{prop:paired}
Assume all cut values lie in \([0,\binom q3]\).
Take \(0\le\lambda\le(t-1)/3\) such that every positive cap
\(u_\delta(j)\) below satisfies
\(\lambda\le(u_\delta(j)-1)/3\). Define \(g_\lambda(0,N)=0\) and
\begin{equation}\label{eq:Epaired}
\begin{split}
 \mathcal D&=\{0\}\cup\{D:(u,r,D)\in\mathcal T\},\\
 E_{\mathcal T}
 &=\max_{\delta\in\mathcal D}
 \left\{\beta_\lambda\left(\binom q3-\delta\right)
             +\sum_{j=1}^{M}g_\lambda(u_\delta(j),q+j-1)\right\}.
\end{split}
\end{equation}
Then \(K_4(\A)\le\lambda|\A|+E_{\mathcal T}\).
\end{proposition}
\begin{proof}
Decomposition by largest vertex gives exactly
\[
 K_4(\A)-\lambda|\A|
 =K_4(\A_0)-\lambda|\A_0|
   +\sum_{j=1}^{M}\bigl(K_3(G_{q+j})-\lambda e(G_{q+j})\bigr).
\]
Apply \eqref{eq:beta} to the head and
\eqref{eq:weightedgraph} to each positive-cap link; a zero cap
makes that link empty. Between consecutive cut values the caps are
constant and the head term is nonincreasing. The left endpoint of
each interval therefore suffices, proving \eqref{eq:Epaired}.
The state \(\delta=0\) is included; the nonempty-tail cut makes
all its links empty. Thus the bound also covers empty tails.
\end{proof}
The finite reduction covers every deficit interval. It does not sample
selected hypergraphs or assume that the relaxed maximizing state is attained.

The same proposition holds for every \(\lambda\ge0\), with
\(g_\lambda\) replaced throughout by \(\widehat g_\lambda\) from
Lemma \ref{lem:graph-all}; no positive-cap weight restriction is then
needed. The proof is identical, using \eqref{eq:graph-all} on the links.
The carrier condition holds because \(q+j-1\ge3t+2\ge2u_\delta(j)+1\).
Denote this envelope by \(\widehat E_{\mathcal T}\).
The cut hypotheses, head cap and exhaustive deficit intervals are unchanged.

\subsection{Adapted moments and the finite certificate}\label{sec:certificate}
The centre used in Section \ref{sec:moments} can depend on the mean
density while remaining deterministic.

\begin{lemma}[Density-adapted centre]\label{lem:adapted}
Suppose \(m\ge3v\), \(t+1\le v\le2t\), \(v>2\), and
\(\Var Z\le\rho\mu(1-\mu/v)\) for some \(0<\rho<v\).
Put \(y=v-t\), \(a_v=1-\rho/v\), \(\xi_0=2ty/v\), and
\[
 \xi(\mu)=\max\{\xi_0,a_v\mu+\rho\},\qquad 0\le\mu\le v .
\]
For the nested incidence variable of Lemma \ref{lem:nested},
\begin{equation}\label{eq:Psi}
 \E(W-tv)\le\Psi_w(\mu):=
 w\mu-\frac{2ty\mu}{\xi(\mu)}
      +\frac{ty(a_v\mu^2+\rho\mu)}{\xi(\mu)^2}.
\end{equation}
The function \(\Psi_w\) is convex and \(\Psi_w(0)=0\).
\end{lemma}
\begin{proof}
For every \(\xi\in[\xi_0,v]\), the quadratic
\(wz-ty+ty(z-\xi)^2/\xi^2\) dominates both incidence branches:
use the calculation in Section \ref{sec:moments} with \(b=\xi\).
Taking expectations and using the stated variance bound gives the expression
on the right of \eqref{eq:Psi} with this fixed \(\xi\).
For \(\mu>0\), its derivative with respect to \(\xi\) has the sign
of \(\xi-(a_v\mu+\rho)\); also \(a_v\mu+\rho\le v\).
The displayed \(\xi(\mu)\) therefore minimizes that upper bound.

On the free branch the expression is
\[
 w\mu-\frac{ty\mu}{a_v\mu+\rho},
 \qquad
 \frac{d^2}{d\mu^2}
 \left(w\mu-\frac{ty\mu}{a_v\mu+\rho}\right)
 =\frac{2ty\rho a_v}{(a_v\mu+\rho)^3}>0 .
\]
The clamped branch is a convex quadratic with second derivative
\(2tya_v/\xi_0^2\). Values and slopes agree at the join.
If \(\xi_0\le\rho\), only the free branch occurs.
The centre depends on the mean, not the sampled matching, so the
expectation step is valid. The case \(\mu=0\) is immediate.
\end{proof}

In the formulas below, \(\rho=2\) unless explicitly specified.
Lemma \ref{lem:variance-one-sided} permits a smaller value in the last base.
The preceding estimates specialize to \(\rho=2\).

Set \(C=\binom m3\), \(B=B_3(m,t)\), and \(b=vB/C\).
Whenever \(t\ge33\) and \(m\ge4t-1\), \eqref{eq:triple} gives
\(\mu\le b\). If \(K_4(\A)\le\lambda|\A|+E\) with
\(0\le\lambda<c\), equations \eqref{eq:twoH} and \eqref{eq:Psi} imply
\begin{equation}\label{eq:F}
 \frac vC\left(|\HH|+\sum_i|\A_i|-tC\right)
 \le F(\mu):=\Psi_{\lambda+1}(\mu)
                  +\min\{(c-\lambda)\mu,Ev/C\}.
\end{equation}
If \(0<\mu_*:=Ev/[C(c-\lambda)]<b\le v\), \(F\) is convex
separately on \([0,\mu_*]\) and \([\mu_*,b]\), with \(F(0)=0\).
Thus two nonpositive endpoint values suffice for the cover bound.
Global convexity across the corner of the minimum is not asserted.

For each \(3229\le t\le3480\), use
\[
 n=t+15301,\quad m=15300,\quad v=5100,\quad
 \lambda=\frac{3(t-1)}{100},\quad E=E_{\mathcal T}.
\]
The finite cut set consists of \((1,1,d_0)\) and the cuts
\[
 u=\floor{it/1000},\quad i=250,300,\ldots,1000,\qquad
 r=\floor{jt/1000},\quad j=25,75,\ldots,\quad j\le i,
\]
subject to \(1\le r\le u\) and \(t-r\ge33\).
This is a sufficient fixed selection, not optimization over all cut sets.
The certificate checks every residual FRR domain, positive-cap weight
domain, cut value and moment interval. It gives
\begin{center}
\begin{tabular}{@{}lr@{}}
\toprule
Check & Result\\
\midrule
Finite bases & 252\\
Averaged cuts & 50400\\
Deficit states, including zero & 25956\\
Strictly negative rational endpoints & 504\\
\bottomrule
\end{tabular}
\end{center}
The cuts encode a fractional capacity calculation; the distributed
verifier checks them using the dual inequalities \eqref{eq:dualcut}.
It reconstructs every deficit interval and sums the tail envelopes
exactly, using arithmetic progressions between their breakpoints.
In particular, this covers all 103 states at the critical base.

Both endpoint maxima occur at \(t=3480\). There
\[
 q=10442,\quad c=2610,\quad 100E=62543109568930107,\quad
 b=\frac{321648884360}{117022051},
\]
\[
 \mu_*=\frac{20847703189643369}{9773798721571},
\]
and
\begin{align*}
 F(b)&=-\frac{734432834661303950523791651}
                 {480071155938247978303700}<0,\\
 F(\mu_*)&=-\frac{12342446404786844238991062728486983}
                    {211193652014625943473584177232}<0.
\end{align*}
The maximizing envelope state is \(\Delta=45051066360\);
its caps are 3480 through tail position 1130 and 3479 thereafter.
It is an upper-bound profile, not a constructed extremizer.

\paragraph{The additional base at \(t=2904\).}
Use the same cut selection and envelope with
\[
 n=15676,\quad m=12771,\quad v=4257,\quad y=1353,\quad
 q=8714,\quad c=2178,\quad\lambda=\frac{8709}{100}.
\]
There are 200 averaged cuts and 103 deficit states, including zero.
The certificate checks all the domains used above and gives
\[
 100E=30345188802828751,\quad
 b=\frac{37403488540}{16306013},\quad
 \mu_*=\frac{30345188802828751}{17047202820915}.
\]
In particular, \(0<\mu_*<b\le v\), and the two exact signs are
\begin{align*}
 F(b)&=-\frac{206897019088563628476145569}
                  {59031722428985718476500}<0,\\
 F(\mu_*)&=-\frac{396285397094368554542026979822553289}
                    {9226892430402448555509056468640}<0.
\end{align*}
At each of the 103 states the verifier sums the envelope over all
4057 tail positions using exact arithmetic progressions.
These are fixed certificate checks, with no additional hypothesis on
\(\F\). The local proof and the new constant below do not use HHL.

\paragraph{The further base at \(t=888\).}
The general lemmas above also apply at
\[
 n=4798,\quad m=3909,\quad v=1303,\quad y=415,\quad
 q=2666,\quad c=666,\quad\lambda=\frac{2661}{100}.
\]
Here \(t\ge33\), \(m\ge4t-1\), \(q\le m\), \(n\ge4t+4\), and
\(t+1\le v\le2t\). Retaining only the admissible cuts in the same grid
leaves 199 averaged cuts, together with \((1,1,d_0)\), where
\(d_0=3544453\). They produce 102 deficit states. In particular, the
FRR condition \(t-r\ge33\) excludes one grid cut that was available at
the preceding bases. Every residual ground-set and positive graph-cap
domain is checked separately. The exact values are
\[
 100E=265583224513928,\qquad
 b=\frac{2678431702}{3817139},\qquad
 \mu_* =\frac{132791612256964}{244064050521},
\]
and
\begin{align*}
 F(b)&=-\frac{21670567755141894005923}{27790259876854163550}<0,\\
 F(\mu_*)&=-\frac{9548351932641510714925649296621}
                    {2195172693406543742168343732}<0.
\end{align*}
We have \(0<\mu_*<b\le v\). At each of the 102 states the verifier
sums the envelope over all 1243 tail positions using exact arithmetic
progressions between breakpoints.
This is a new application of the general section, cut and moment lemmas,
not an application of the uniform theorem outside \(t\ge2200\).

\paragraph{The base at \(t=360\).}
The same cut grid and moment lemmas apply with
\[
 n=1950,\quad m=1589,\quad v=529,\quad y=169,\quad
 q=1082,\quad c=270,\quad\lambda=\frac{1077}{100}.
\]
Here \(m=3v+2\). The variance input \eqref{eq:variance} permits
\(m\ge3v\), so the two unused vertices require no change of normalization.
We have \(t\ge33\), \(m\ge4t-1\), \(q\le m\), \(n\ge4t+4\)
and \(t+1\le v\le2t\). Filtering the grid by the stated FRR domain
leaves 197 averaged cuts, plus the nonempty-tail cut, and 100 deficit
states. The smallest actual residual matching parameter is 45.
Every cut, positive link cap and adapted centre is checked in its own
domain. The exact values are
\[
 100E=7198243043040,\qquad b=\frac{179393730}{630833},\qquad
 \mu_*=\frac{171386739120}{778718279},
\]
with \(0<\mu_*<b\le v\), and
\begin{align*}
 F(b)&=-\frac{2272864566320194107}{9384421237500155}<0,\\
 F(\mu_*)&=-\frac{241993520128384136905733}
                    {307445894130701973387}<0.
\end{align*}
Exact arithmetic progressions sum all 507 tail positions at each of the
100 states. As at the other bases, the two endpoint signs use
convexity separately on the two sides of \(\mu_*\), including the zero
state; they assert neither global convexity across the corner nor
realizability of the maximizing relaxed profile.

\paragraph{The base at \(t=72\).}
The same parametric lemmas, rather than the uniform theorem, apply with
\[
 n=395,\quad m=322,\quad v=107,\quad y=35,\quad
 q=218,\quad c=54,\quad\lambda=\frac{213}{100}.
\]
The ground set satisfies \(q\le m\le5t+8\), \(m\ge4t-1\),
\(n\ge4t+4\), \(t+1\le v\le2t\). Here \(m=3v+1\), permitted
by \eqref{eq:variance}. Filtering the same cut grid leaves 155 averaged
cuts, plus the nonempty-tail cut; the smallest residual FRR matching
parameter is 35. Every positive link cap satisfies the weight domain
of Lemma \ref{lem:graphs}. The cuts give 67 deficit states, and
\[
 100E=11744277120,\qquad b=\frac{73491}{1288},\qquad
 \mu_*=\frac{12233622}{278369}.
\]
The maximizing envelope state is \(\Delta=400200\), with cap 72 on
each of the 104 tail positions; it is not asserted realizable. Exact
arithmetic progressions sum the envelope at all 67 deficit states.

At this smaller base, the two endpoints use different centre branches:
\[
 \xi_0=\frac{5040}{107},\qquad
 \theta:=\frac{\xi_0-2}{1-2/v}=\frac{4826}{105},\qquad
 0<\mu_*<\theta<b\le v.
\]
Thus \(\xi(\mu_*)=\xi_0\) is clamped and \(\xi(b)=(1-2/v)b+2\)
is free. Using the corresponding formulas in \eqref{eq:Psi} gives
\begin{align*}
 F(b)&=-\frac{3130309743249}{147056240800}<0,\\
 F(\mu_*)&=-\frac{152269162897357}{4649358009660}<0.
\end{align*}
The centre join preserves values and slopes, as proved in
Lemma \ref{lem:adapted}; hence its passage inside \([\mu_*,b]\) does
not spoil convexity there. Convexity across the separate corner at
\(\mu_*\) is not assumed. In particular, the free-branch simplification
must not be used at both endpoints.

\paragraph{The base at \(t=49\).}
Use the all-weight envelope \(\widehat E_{\mathcal T}\), with
\[
 n=269,\quad m=219,\quad v=73,\quad y=24,\quad
 q=149,\quad c=37,\quad \lambda=1.
\]
Choose every cut of Lemma \ref{lem:averaged} with
\(3\le u\le49\), \(1\le r\le\min\{u,16\}\), together with
\((1,1,d_0)\). There are 661 averaged cuts, and the minimum residual
FRR matching parameter is 33. The 190 deficit states include zero.
Equation \eqref{eq:graph-all} checks every cap, including \(u=0,1,2,3\);
the restricted formula \eqref{eq:weightedgraph} is not used outside
its weight domain. Exact summation over 70 tail positions in every state
checks 13300 positions and yields
\[
 E=\widehat E_{\mathcal T}=\frac{50841725}{2},\qquad
 \rho=\rho_{219,73}=\frac{217}{215}.
\]
The remaining domains are \(q\le m\), \(m\ge4t-1\),
\(n\ge4t+4\), \(t+1\le v\le2t\), and \(0<\rho<v\).
With this \(\rho\) in Lemma \ref{lem:adapted},
\[
 b=\frac{131747}{3379},\qquad
 \mu_*=\frac{50841725}{1703016},\qquad 0<\mu_*<b\le v,
\]
and the two certified values of \eqref{eq:F} are
\[
 F(\mu_*)=-\frac{941079953521235}{62581832506368}<0,\qquad
 F(b)=-\frac{80139181023}{8649854794}<0.
\]
The centre is evaluated as the displayed maximum at each endpoint.
The proof uses convexity on each side of \(\mu_*\), including any centre
join; it does not assert convexity across the minimum in \eqref{eq:F}.
Neither this base nor its stability and equality consequences use HHL.

\begin{proof}[Proof of Theorem \ref{thm:finite}]
First suppose \(\nu(\F)=t\).
Use the sections of Section \ref{sec:sections} and the certified
parameters above. Define
\[
 \eta_t=\min\left\{-F(\mu_*)/\mu_*,-F(b)/b\right\}>0.
\]
On each of the two intervals, \(F(\mu)+\eta_t\mu\) is convex
and nonpositive at its endpoints, hence nonpositive throughout.
Equation \eqref{eq:F} and Lemma \ref{lem:accounting} give
\[
 d_t(\F)\ge\eta_t|\A|,\qquad
 \gamma_t(\F)\le(c+1)|\A|
       \le\frac{c+1}{\eta_t}d_t(\F).
\]
The case \(\A=\varnothing\) has \(\gamma_t(\F)=0\).
The exact calculation of all 252 ratios gives its maximum at
\(t=3480\):
\[
 \max_t\frac{c+1}{\eta_t}
 =\frac{3445298291203325575600158052000}
        {734432834661303950523791651}<4692.
\]
For the additional base \(t=2904\), the same normalization gives
\begin{align*}
 \eta_{2904}&=\frac{206897019088563628476145569}
                    {135409701523544000906870000},\\
 \frac{2179}{\eta_{2904}}
 &=\frac{295057739619802377976069730000}
         {206897019088563628476145569}<1427.
\end{align*}
At \(t=888\), the same endpoint normalization gives
\begin{align*}
 \eta_{888}&=\frac{21670567755141894005923}
                   {19500026868548619183900},\\
 \frac{667}{\eta_{888}}
 &=\frac{13006517921321928995661300}{21670567755141894005923}<601.
\end{align*}
At \(t=360\), the endpoint normalization gives
\begin{align*}
 \eta_{360}&=\frac{757621522106731369}{889567883357596850},\\
 \frac{271}{\eta_{360}}
 &=\frac{241072896389908746350}{757621522106731369}<319.
\end{align*}
At \(t=72\), the two centre branches give
\begin{align*}
 \eta_{72}&=\frac{1043436581083}{2796922927700},\\
 \frac{55}{\eta_{72}}
 &=\frac{153830761023500}{1043436581083}<148.
\end{align*}
At \(t=49\), the one-sided variance and all-weight envelope give
\[
 \eta_{49}=\frac{7285380093}{30659754622},\qquad
 \frac{38}{\eta_{49}}
 =\frac{1165070675636}{7285380093}<160.
\]
Lemma \ref{lem:completion} extends each estimate to \(\nu(\F)\le t\);
the identity in Lemma \ref{lem:accounting} gives the corresponding
symmetric-difference factor \(1+2K\).
\end{proof}

\begin{lemma}[Propagation from a cover base]\label{lem:propagation}
Let \(t\ge33\), \(a\ge4t+4\), and suppose the cover bound holds at
\(n=a\) for every four-graph of matching number at most \(t\).
Then it holds for all \(n\ge a\).
\end{lemma}
\begin{proof}
Shift a family on \(n\ge a+1\) vertices and delete its last vertex.
Its triple link has matching number at most \(t\): \(t+1\) disjoint
triples would leave at least
\(n-1-3(t+1)\ge t+1\) unused vertices below \(n\).
Replacing the last vertex in the corresponding four-edges by these
distinct unused vertices, using stability, gives a forbidden matching.
Induction on \(n\) and \eqref{eq:triple} now give
\[
 |\F|\le B_4(n-1,t)+B_3(n-1,t)=B_4(n,t).
\]
\end{proof}
\begin{proposition}[Quantitative propagation]\label{prop:quantprop}
Let \(t\ge33\), \(a\ge4t+4\), and \(K\ge0\). Suppose every shifted
four-uniform family on \([a]\) with matching number at most \(t\)
satisfies the cover bound and \(\gamma_t\le Kd_t\).
Then for every \(n\ge a\), each such family \(\F\) on \([n]\) satisfies
\[
 \gamma_t(\F)\le
 K\frac{\binom{n-t}4}{\binom{a-t}4}\,d_t(\F).
\]
\end{proposition}
\begin{proof}
For \(a\le j\le n\), let \(\F_j=\F\cap\binom{[j]}4\), and write
\(d_j=B_4(j,t)-|\F_j|\) and
\(\gamma_j=|\F_j\setminus\mathcal C_{[t]}(j)|\).
Each restriction is shifted with matching number at most \(t\).
Lemma \ref{lem:propagation} supplies its cover bound.

For \(j>a\), the triple link \(L_j\) of \(j\) has matching number
at most \(t\). Otherwise its \(t+1\) disjoint triples could be completed
with \(t+1\) unused vertices below \(j\), since
\(j-1-3(t+1)\ge t+1\). Shiftedness would give a forbidden matching.
By \eqref{eq:triple} and Pascal's identity,
\[
 d_j-d_{j-1}=B_3(j-1,t)-|L_j|\ge0.
\]
Let \(\ell_j\) count the triples of \(L_j\) avoiding \([t]\).
For each such triple \(T\), every \(x\in[j-1]\setminus([t]\cup T)\)
gives \(T\cup\{x\}\in\F_{j-1}\), again by shiftedness.
There are \(j-t-4\) choices of \(x\), while each four-edge outside
the cover is counted at most four times. Therefore
\[
 (j-t-4)\ell_j\le4\gamma_{j-1},\qquad
 \gamma_j=\gamma_{j-1}+\ell_j
 \le\frac{j-t}{j-t-4}\gamma_{j-1}.
\]
Multiplication from \(j=a+1\) to \(n\) telescopes:
\[
 \gamma_n\le
 \frac{\binom{n-t}4}{\binom{a-t}4}\gamma_a
 \le K\frac{\binom{n-t}4}{\binom{a-t}4}d_a
 \le K\frac{\binom{n-t}4}{\binom{a-t}4}d_n.
\]
The case \(n=a\) uses the empty product. The base hypothesis already
allows matching number smaller than \(t\), so it applies to \(\F_a\).
\end{proof}

Applying Proposition \ref{prop:quantprop} to
Theorems \ref{thm:uniform}--\ref{thm:finite} proves
Corollary \ref{cor:alln}; the symmetric-difference identity is
Lemma \ref{lem:accounting}. No new certificate is needed for this step.

\subsection{Exact extremizers above the bases}\label{sec:equality}
\begin{lemma}[Propagation of shifted equality]\label{lem:equality-propagation}
Let \(t\ge33\), \(a\ge4t+4\), and suppose the cover bound holds for
matching number at most \(t\) at every \(n\ge a\).
If \(\mathcal C_t\) is the unique stable family of exact matching number
\(t\) attaining \(B_4(a,t)\), the same uniqueness holds at every \(n\ge a\).
\end{lemma}
\begin{proof}
Induct on \(n>a\). Let \(\F\) be stable with
\(\nu(\F)=t\) and \(|\F|=B_4(n,t)\).
Put \(\F_0=\F\cap\binom{[n-1]}4\) and let \(L\) be the triple link of \(n\).
We have \(\nu(\F_0)=t\): if a \(t\)-matching uses \(n\), replace that
vertex by an unused smaller vertex, available since \(n>4t\), and
apply stability. Lemma \ref{lem:propagation} gives \(\nu(L)\le t\);
the triple bound therefore gives
\[
 |\F_0|+|L|\le B_4(n-1,t)+B_3(n-1,t)=B_4(n,t).
\]
Both inequalities must be equalities, so induction identifies
\(\F_0\) with the complete cover of \([t]\).
An edge \(E\in\F\) avoiding \([t]\) would contain \(n\).
There are at least \(3t\) vertices in
\([n-1]\setminus([t]\cup(E\setminus\{n\}))\), since \(n\ge4t+4\).
Partition \(3t\) of them into triples and add a different vertex of
\([t]\) to each. This gives a \(t\)-matching of \(\F_0\) disjoint from
\(E\), a contradiction. Thus \(\F\subseteq\mathcal C_t\);
equal cardinalities finish the proof.
\end{proof}

\begin{proof}[Proof of Corollary \ref{cor:extremizers}]
The cover bound holds at all the stated bases by Theorems \ref{thm:uniform}--\ref{thm:finite}, using shifting for arbitrary families. Lemma \ref{lem:propagation} gives it at every larger ground set.
At its maximum cardinality, matching number below \(t\) is impossible:
adding a missing edge would contradict that bound.
The same observation applies after shifting.
Theorems \ref{thm:uniform}--\ref{thm:finite} and
Lemma \ref{lem:equality-propagation} identify the fully shifted family.
Invert the shifts one at a time using Lemma \ref{lem:undo-shift};
each preceding family still has matching number at most \(t\).
\end{proof}
Only exact equality is transferred through arbitrary shifts.
Quantitative stability for shifted families above a base is supplied by
Proposition \ref{prop:quantprop}, with its explicit binomial loss.
The constants 2285, 4692, 1427, 601, 319, 148 and 160 remain estimates at their specified bases.
These equality arguments use classical shifting and the local cover bounds.
\section{Polynomial details for the uniform range}\label{app:polys}
The two polynomial positivity checks in Proposition \ref{prop:uniform}
are transparent after translation:
\begin{align*}
 P_A(2200+x)={}&3019933x^3+19228355100x^2\\
               &+40755950097500x+28754097993750000,\\
 P_J(2200+x)={}&23803113x^4+209384508244x^3\\
               &+690694581174300x^2+1012615286669630000x\\
               &+556715897678850000000.
\end{align*}
Every coefficient is positive. These are identities in the product
extension of binomial coefficients. The moment-margin derivation can
be checked without a symbolic system. For example in the low-density
row, \(y_-=29t/50-1\), \(y_+=29t/50\), \(b=474t/625\), and
\(w=3t/4+3/2\) give
\[
 M_w\ge ty_- -wb-\frac{2ty_+}{b}\frac{13}{25}
       =\frac{7t(474t-124127)}{296250}.
\]
The high-density row uses \(b=161t/200\), \(w=23t/32+1\) and
\(155/316\) in the last factor. The remaining margins follow from
\(bt+(b-2t)y_+\). These algebraic identities are displayed for direct inspection.

\begin{thebibliography}{99}
\raggedright
\setlength{\itemsep}{2pt plus 1pt}
\bibitem{Erdos65}
P.~Erd\H{o}s, \emph{A problem on independent \(r\)-tuples},
Ann. Univ. Sci. Budapest. E\"otv\"os Sect. Math. \textbf{8} (1965), 93--95.
\href{https://www.renyi.hu/~p_erdos/1965-01.pdf}{Original paper},
equation (9).

\bibitem{GuoLu}
M.~Guo and H.~Lu, \emph{A stability result for almost perfect matchings},
J. Graph Theory \textbf{112} (2026), 5--14.
\href{https://doi.org/10.1002/jgt.70007}{doi:10.1002/jgt.70007}.
Theorem locators follow
\href{https://arxiv.org/abs/2404.09720v1}{arXiv:2404.09720v1}.

\bibitem{Frankl13}
P.~Frankl, \emph{Improved bounds for Erd\H{o}s' Matching Conjecture},
J. Combin. Theory Ser. A \textbf{120} (2013), 1068--1072.
\href{https://doi.org/10.1016/j.jcta.2013.01.008}{doi:10.1016/j.jcta.2013.01.008}.
Theorems 1.1--1.2 and Sections 3--5.

\bibitem{FRR}
P.~Frankl, V.~R\"odl and A.~Ruci\'nski,
\emph{Short Proof of Erd\H{o}s' Conjecture for Triple Systems},
Acta Math. Hungar. \textbf{151} (2017), 495--509.
\href{https://doi.org/10.1007/s10474-017-0692-8}{doi:10.1007/s10474-017-0692-8}.
Theorem 1 in \href{https://arxiv.org/abs/1609.00530v1}{arXiv:1609.00530v1}.

\bibitem{FK}
P.~Frankl and A.~Kupavskii,
\emph{The Erd\H{o}s matching conjecture and concentration inequalities},
J. Combin. Theory Ser. B \textbf{157} (2022), 366--400.
\href{https://doi.org/10.1016/j.jctb.2022.08.002}{doi:10.1016/j.jctb.2022.08.002}.
Locators follow \href{https://arxiv.org/abs/1806.08855v3}{arXiv:1806.08855v3}.
Lemma 10, Proposition 11, equation (20), Theorem 32 and Section 8, Problem 1.

\bibitem{Keevash}
P.~Keevash, \emph{Shadows and intersections: stability and new proofs},
Adv. Math. \textbf{218} (2008), 1685--1703.
\href{https://doi.org/10.1016/j.aim.2008.03.023}{doi:10.1016/j.aim.2008.03.023}.
Theorem 1, p.~1686.

\bibitem{Wang}
J.~Wang, \emph{The shifting method and generalized Tur\'an number of matchings},
\href{https://arxiv.org/abs/1812.01832v5}{arXiv:1812.01832v5}.
Lemmas 2.1--2.2, Lemma 3.2 and proof of Theorem 1.2.

\bibitem{FKStability}
P.~Frankl and A.~Kupavskii,
\emph{Two problems on matchings in set families---in the footsteps of
Erd\H{o}s and Kleitman},
J. Combin. Theory Ser. B \textbf{138} (2019), 286--313.
\href{https://doi.org/10.1016/j.jctb.2019.02.004}{doi:10.1016/j.jctb.2019.02.004}.
Locators follow \href{https://arxiv.org/abs/1607.06126v3}{arXiv:1607.06126v3}.
Theorem 3 and Lemma 4.

\bibitem{FKDiversity}
P.~Frankl and A.~Kupavskii, \emph{Diversity},
\href{https://arxiv.org/abs/1811.01111v1}{arXiv:1811.01111v1}.
Theorem 28.

\bibitem{FLMW}
P.~Frankl, H.~Lu, J.~Ma and Y.~Wu,
\emph{Towards the Erd\H{o}s matching conjecture for 4-uniform hypergraphs:
stability and applications},
\href{https://arxiv.org/abs/2602.19230v2}{arXiv:2602.19230v2}.
Theorems 1.2 and 1.5; Definition 1.4.

\bibitem{CLZ}
M.~Cao, H.~Liu and H.~Zhang,
\emph{A Near-Optimal Linear Range for the Erd\H{o}s Matching Conjecture},
\href{https://arxiv.org/abs/2608.19118v2}{arXiv:2608.19118v2}.
Theorems 1.2 and 1.4; Remark 1.3 and Section 6.1.

\bibitem{HHL}
J.~Hou, C.~Hu and X.~Liu,
\emph{A finite-board reduction for the Erd\H{o}s Matching Conjecture
and the 4-uniform case via exact certificates},
\href{https://arxiv.org/abs/2605.26060v1}{arXiv:2605.26060v1}.
Sections 2 and 4 for the attributed trace and selection mechanisms;
Lemmas 5.1--5.3, specified C1/C2 parts of Theorem 9.2 and
Appendix A.1 for the finite ingredients reconstructed in Sections
\ref{app:global}--\ref{app:range92}. Lemma 3.1 is not an input
to the present global proof.

\bibitem{Frankl17}
P.~Frankl, \emph{On the maximum number of edges in a hypergraph with
 given matching number}, Discrete Appl. Math. \textbf{216} (2017), 562--581.
\href{https://doi.org/10.1016/j.dam.2016.08.003}{doi:10.1016/j.dam.2016.08.003}.
Theorem locators for the deletion inequality and the historical
announcement follow the \href{https://www.renyi.hu/~pfrankl/2016-2.pdf}{later author copy},
Proposition 5.1 and Theorem 13.2; they are distinct from the first
arXiv version \href{https://arxiv.org/abs/1205.6847v1}{1205.6847v1}.

\bibitem{LMS}
T.~{\L}uczak, K.~Mieczkowska and M.~{\v S}ileikis,
\emph{On maximal tail probability of sums of nonnegative, independent
and identically distributed random variables},
Statistics \& Probability Letters \textbf{129} (2017), 12--16,
\href{https://doi.org/10.1016/j.spl.2017.04.024}{doi:10.1016/j.spl.2017.04.024};
consulted version \href{https://arxiv.org/abs/1602.03547v1}{arXiv:1602.03547v1}.
Conjecture 1.1 and Lemma 3.2.

\bibitem{SciNet}
SciNet, \emph{Erd\H{o}s matching conjecture (\#1020) confirmed by exact
computation in five complete open windows}, public dossier,
27 July 2026.
\href{https://api.scinet.pub/f/aec4527d-0276-45b3-82ab-98aa3f965d75}{Finding and finite-value table};
\href{https://github.com/scinet-ai/math-number-theory/blob/e36280d1d511422e9447ae98f8c49bcb644fd678/erdos-1020/README.md}{repository at commit e36280d1}.
Compared as prior computational work; its solvers are not proof inputs.

\bibitem{Mishra}
T.~K.~Mishra, \emph{Erd\H{o}s Matching (Conjecture) Theorem},
\href{https://arxiv.org/abs/2602.01471v6}{arXiv:2602.01471v6},
withdrawn 1 June 2026. Cited only for the withdrawal status of the
earlier complete-solution claim, not as a theorem input.

\end{thebibliography}
\end{document}