The analytic construction leaves the bounded range \(3\le n<10\,000\).
We complete it with two forms of exact certificate.
Small orders are supplied as explicit binary matrices. For the larger
orders, it suffices to give margins and diagonal entries and verify the
following criterion.

\begin{lemma}\label{short:lem:finite_cuts}
Let \(\alpha_i\in\{0,1\}\), with \(\alpha_0=0\), and let the integers \(Q_i\)
satisfy \(\sum_iQ_i=n(n-1)/2\) and \(0\le Q_i-\alpha_i\le n-1\).
Put \(q_i=Q_i-\alpha_i\). For each \(1\le k\le n\), form the weights
\[
 w_i^{(k)}=i-\alpha_i+\ind_{\{q_i\ge k\}},
\]
and write \(w_{(1)}^{(k)}\ge\cdots\ge w_{(n)}^{(k)}\) for their
nonincreasing rearrangement.
A binary matrix with row sums \(i\), column sums \(Q_i\), and diagonal
\(\alpha_i\) exists if and only if
\begin{equation}\label{short:eq:finite_cuts}
 \sum_{i=0}^{n-1}\min(q_i,k)
 \ \ge\ \sum_{j=1}^{k}w_{(j)}^{(k)}
 \qquad(1\le k\le n).
\end{equation}
\end{lemma}
\begin{proof}
Reserve the diagonal entries and apply the forbidden-diagonal flow
criterion in Lemma~\ref{lem:margins}.
For a row subset \(I\) of size \(k\), its right side is
\[
 \sum_j\min(q_j,k-\ind_{\{j\in I\}})
 =\sum_j\min(q_j,k)-\sum_{i\in I}\ind_{\{q_i\ge k\}}.
\]
Thus its cut condition is
\(\sum_{i\in I}w_i^{(k)}\le\sum_j\min(q_j,k)\).
The largest left side is the sum of the \(k\) largest weights.
The empty subset satisfies the condition, and the integer flow criterion
proves the equivalence. Fig.~\ref{fig:finite-cut} shows this conversion
for one cut in the order-five example.
\end{proof}

\begin{figure}[htbp]
\centering\input{figures/finite_cut.tex}
\caption{The cut with \(k=2\) and \(I=\{3,4\}\) for the matrix in
Fig.~\ref{fig:matrix-landmarks}. In (a), crosses mark forbidden diagonal
positions after reserving the diagonal entries. Column capacities are
\(\min(q_j,2-\mathbf1_{j\in I})\), giving \((2,2,0,1,1)\) for total
demand six. In (b), weights \((1,2,1,3,4)\) have two largest values
summing to seven, equal to \(\sum_j\min(q_j,2)\). Moving the one-unit
diagonal loss to the left converts the same inequality from \(6\le6\)
to \(7\le7\). Every other cut size must also be checked.}
\label{fig:finite-cut}
\end{figure}

\FloatBarrier
\Needspace{10\baselineskip}
\begin{proposition}\label{short:prop:finite}
For every integer \(3\le n<10\,000\), the graph \(S_3(K_n)\)
has an edge multiset resolving set of size at most \(n(n-1)/2\).
\end{proposition}
\begin{proof}[Proof by exact finite certificates]
The accompanying data files\footnote{\raggedright CSV files and reading instructions: \url{https://github.com/tashimir/subdivided-complete-edge-multiset-data}.} cover each integer in this range once.
For \(3\le n\le29\), \texttt{small\_matrices.csv} gives all entries
of one binary matrix of each order. Its fields \(n\) and \texttt{row}
identify a row, and fields \texttt{c0},\ldots,\texttt{c28} contain its
entries followed by empty padding. Algorithm~\ref{alg:matrix} decodes the ones
using~\eqref{short:eq:matrix_encoding} and verifies the resolving
property from graph distances. All 27 matrices satisfy the size bound
and have distinct histograms for their \(12\,177\) graph edges in total.

For \(30\le n\le9999\), the file \texttt{degree\_certificates.csv}
contains one record \((n,p,d,X,Y)\) for each order.
Algorithm~\ref{alg:degrees} reconstructs the column sums and diagonal,
then checks every inequality in~\eqref{short:eq:finite_cuts}.
These checks use integer arithmetic. They passed for all 9970 records,
including all \(49\,994\,565\) inequalities indexed by \((n,k)\).
The diagonal-bit identity gives
\(2Q_i-\alpha_i\equiv f(i)+d\pmod p\).
Lemma~\ref{short:lem:finite_cuts} therefore realizes each record, and
Proposition~\ref{short:prop:separation} proves that its matrix encodes a
resolving set of size \(n(n-1)/2\).
Table~\ref{short:tab:coverage} records the coverage.
\end{proof}

\begin{table}[htb]
\centering
\caption{Complete coverage of the length-three case. The finite rows
contain exact certificates for every integer in the indicated interval.}
\label{short:tab:coverage}
\begin{tabular}{@{}lll@{}}
\toprule
Orders & Certificate or construction & Number of orders\\
\midrule
\(3\le n\le29\) & Explicit matrices; graph distances & 27\\
\(30\le n\le9999\) & Margins and all integer cut inequalities & 9970\\
\(n\ge10\,000\) & Corollary~\ref{short:cor:threshold} and Proposition~\ref{short:prop:separation} & All remaining orders\\
\bottomrule
\end{tabular}
\end{table}

Proposition~\ref{short:prop:finite} and the analytic construction prove the
upper bound in Theorem~\ref{short:thm:three} for every \(n\ge3\).
Corollary~\ref{cor:three-lower} supplies its lower bound for \(n\ge10\),
completing the theorem.


The record \((30,37,6,1,6)\) provides a worked reconstruction
(Fig.~\ref{fig:balance-example}). Its low total is \(303\), its deficit
is \(132\), and lifting one entry with odd residue and six with even
residue adds exactly
\(18+6\cdot19=132\). These are finite certificate parameters;
their validity follows from the cuts, independently of the sufficient
analytic hypotheses of Proposition~\ref{short:prop:quadratic_matrix}.
\begin{figure}[htbp]
\centering\input{figures/balance_example.tex}
\caption{Exact balancing in the certificate \((n,p,d,X,Y)=(30,37,6,1,6)\).
Pairs \((L_i,i)\) are ordered lexicographically within each parity class
of the residues \(r_i\). Blue selects the first pair with odd \(r_i\);
orange selects the first six eligible pairs with even \(r_i\).
The following pairs make the tie-breaking rule visible.
Index zero is excluded from the even-residue class. The total rises from
\(303\) to \(303+18+6\cdot19=435=n(n-1)/2\).}
\label{fig:balance-example}
\end{figure}
\FloatBarrier

The two algorithms below check different mathematical objects.
Algorithm~\ref{alg:matrix} builds the graph from a small matrix and
compares the actual distance histograms. Algorithm~\ref{alg:degrees}
reconstructs the larger certificates and checks the necessary and
sufficient inequalities for a matrix to exist. The latter relies on
Proposition~\ref{short:prop:separation} for the resolving property.

The CSV conventions are specified in \texttt{data/README.txt}.
Read the fields by name and verify that every required order and matrix
row occurs exactly once before applying the algorithms.
In Algorithm~\ref{alg:matrix}, \textsc{BreadthFirstDistances}\((G,s)\)
returns the function \(v\mapsto d_G(s,v)\).

\begin{algorithm}[H]
\caption{Check a small matrix by graph distances}\label{alg:matrix}
\begin{algorithmic}[1]
\Require A binary matrix \(M\) of order \(n\), with \(3\le n\le29\).
\Ensure Accept exactly when its selected vertices resolve \(S_3(K_n)\)
using at most \(\binom n2\) landmarks.
\State Create originals \(v_0,\ldots,v_{n-1}\) in an empty graph \(G\).
\For{each pair \(0\le i<j<n\)}
 \State Create fresh vertices \(x_{ij},x_{ji}\).
 \State Add the path \(v_i-x_{ij}-x_{ji}-v_j\) to \(G\).
\EndFor
\State \(W\gets\{v_i:M_{ii}=1\}\cup\{x_{ij}:i\ne j,\ M_{ij}=1\}\).
\State \textbf{if} \(|W|>\binom n2\) \textbf{then return} Reject.
\State \((H_e(0),\ldots,H_e(5))\gets(0,0,0,0,0,0)\) for each edge \(e\).
\For{each \(s\in W\)}
 \State \(d\gets\Call{BreadthFirstDistances}{G,s}\).
 \For{each edge \(e=uv\) of \(G\)}
  \State \(t\gets\min(d(u),d(v))\).
  \State \(H_e(t)\gets H_e(t)+1\).
 \EndFor
\EndFor
\State Sort the six-entry vectors \((H_e)_{e\in E(G)}\) lexicographically.
\State \Return Accept if no consecutive vectors agree; otherwise Reject.
\end{algorithmic}
\end{algorithm}

The standard breadth-first search in Algorithm~\ref{alg:matrix}
returns the distance from \(s\) to every vertex. All edge-to-vertex
distances in \(S_3(K_n)\) are at most five, so six counters record a
complete histogram. Each landmark increments exactly one counter for
each edge. Consequently acceptance is equivalent to the definition of
an edge multiset resolving set. There are \(O(n^2)\) vertices, edges,
and possible landmarks; the algorithm takes \(O(n^4)\) operations and
\(O(n^2)\) storage. It checks distances independently of the algebraic
formulas used to find the matrices.

Algorithm~\ref{alg:degrees} uses the low values and parity bits from
\eqref{short:eq:low}. The initial parity bit is denoted by \(\sigma_i=\alpha_i^0\)
to distinguish it from the final diagonal entry \(\alpha_i\). Ordering by
\((L_i,i)\) makes every selection unambiguous. Primality may be checked
by trial division through \(\lfloor\sqrt p\rfloor\).

\begin{algorithm}[H]
\caption{Check a degree certificate}\label{alg:degrees}
\begin{algorithmic}[1]
\Require Integers \((n,p,d,X,Y)\), with \(30\le n\le9999\).
\Ensure Accept exactly when the reconstruction below satisfies
the prime, diagonal, total, and matrix-cut conditions.
\State \textbf{if} \(p\) is not prime or \(p<n+5\) \textbf{then return} Reject.
\State \textbf{if} \(d\notin\{0,\ldots,p-1\}\) or \(\min(X,Y)<0\) \textbf{then return} Reject.
\State \(m\gets(p-1)/2\); \(N\gets n(n-1)/2\).
\For{\(i=0,\ldots,n-1\)}
 \State \(r_i\gets(i(i+3)/2+d)\bmod p\).
 \State \(L_i\gets\lfloor(r_i+1)/2\rfloor\); \(\sigma_i\gets r_i\bmod2\); \(\epsilon_i\gets0\).
\EndFor
\State \(O\gets\{i:\sigma_i=1\}\), ordered by \((L_i,i)\).
\State \(E\gets\{i:\sigma_i=0,\ i\ne0\}\), ordered by \((L_i,i)\).
\State \textbf{if} \(X>|O|\) or \(Y>|E|\) \textbf{then return} Reject.
\State Set \(\epsilon_i\gets1\) at the first \(X\) indices of \(O\)
and the first \(Y\) indices of \(E\).
\For{\(i=0,\ldots,n-1\)}
 \State \(Q_i\gets L_i+\epsilon_i(m+1-\sigma_i)\).
 \State \(\alpha_i\gets\sigma_i+\epsilon_i(1-2\sigma_i)\); \(q_i\gets Q_i-\alpha_i\).
\EndFor
\State \textbf{if} \(\alpha_0\ne0\), or \(\sum_iQ_i\ne N\), or some \(q_i\notin\{0,\ldots,n-1\}\) \textbf{then return} Reject.
\For{\(k=1,\ldots,n\)}
 \State Form \(w_i\gets i-\alpha_i+\ind_{\{q_i\ge k\}}\) for all \(i\).
 \State Sort these weights as \(w_{(1)}\ge\cdots\ge w_{(n)}\).
 \State \textbf{if} \(\sum_{j=1}^k w_{(j)}>\sum_i\min(q_i,k)\) \textbf{then return} Reject.
\EndFor
\State \Return Accept.
\end{algorithmic}
\end{algorithm}

Every reconstructed pair satisfies
\(2Q_i-\alpha_i=r_i+p\epsilon_i\), so it has the target label
value modulo \(p\). The last loop checks all the inequalities of
Lemma~\ref{short:lem:finite_cuts}; acceptance therefore proves matrix
realizability, and Proposition~\ref{short:prop:separation} proves the
resolving property. No approximate arithmetic is used.
The displayed cut verification takes \(O(n^2\log n)\) arithmetic
operations and \(O(n)\) storage per record.