% global_universality_verification.tex

\subsection{Validated global margins from finite sampling}

Theorem~\ref{thm:global_universality_uniform} becomes genuinely global once one has uniform lower bounds
\(\gamma_0,\delta_0\) on the margins across \(\Theta\).
When \(\Theta\) is a parameter family, a standard way to obtain such bounds is to combine a finite net with a conservative Lipschitz envelope.
This subsection records a clean ``verification lemma'' that can be suitable for citation and implemented by a third party.

\begin{definition}[Net mesh]
Let \(\Theta\subset\mathbb{R}^d\) be compact and let \(\|\cdot\|\) be a fixed norm.
A finite set \(\mathcal{N}\subset\Theta\) is an \(h\)-net if for every \(\theta\in\Theta\) there exists \(\theta_i\in\mathcal{N}\) with \(\|\theta-\theta_i\|\le h\).
\end{definition}

\begin{lemma}[Certified minima from a Lipschitz envelope]
\label{lem:lipschitz_min_cert}
Let \(f:\Theta\to\mathbb{R}\) be Lipschitz with constant \(L_f\) with respect to \(\|\cdot\|\).
Let \(\mathcal{N}\) be an \(h\)-net in \(\Theta\).
Then
\[
\min_{\theta\in\Theta} f(\theta) \;\ge\; \min_{\theta_i\in\mathcal{N}} f(\theta_i)\; -\; L_f\,h.
\]
In particular, if the right-hand side is strictly positive then \(f(\theta)>0\) for all \(\theta\in\Theta\).
\end{lemma}

\begin{proof}
Fix \(\theta\in\Theta\) and pick \(\theta_i\in\mathcal{N}\) with \(\|\theta-\theta_i\|\le h\).
Lipschitz continuity gives \(f(\theta)\ge f(\theta_i)-L_f\,h\).
Taking the minimum over \(\theta\in\Theta\) and then the minimum over \(\theta_i\in\mathcal{N}\) yields the claim.
\end{proof}

\begin{proposition}[Uniform margin verification by net + Lipschitz bounds]
\label{prop:uniform_margins_via_lipschitz}
Assume \(\Theta\) is compact.
Fix a candidate tight SCC \(H\) and a candidate witness word \(w\) and assume these are constant on \(\Theta\).
Assume:
\begin{itemize}[leftmargin=2em]
\item the tightness gap function \(\gamma(\theta)\) is Lipschitz with constant \(L_{\gamma}\),
\item the Doeblin margin function \(\delta_w(\theta):=\min(P_w(\theta))\) is Lipschitz with constant \(L_{\delta}\),
\item RC1 holds for \((H,w)\) (equivalently: the avoidance automaton has no directed cycle).
\end{itemize}
Let \(\mathcal{N}\) be an \(h\)-net in \(\Theta\).
Define certified lower bounds
\[
\underline\gamma_0 := \min_{\theta_i\in\mathcal{N}}\gamma(\theta_i) - L_{\gamma}h,\qquad
\underline\delta_0 := \min_{\theta_i\in\mathcal{N}}\delta_w(\theta_i) - L_{\delta}h.
\]
If \(\underline\gamma_0>0\) and \(\underline\delta_0>0\), then \(\Theta\) admits uniform robust margins in the sense of Definition~\ref{def:uniform_margins}, hence Theorem~\ref{thm:global_universality_uniform} applies with \(\gamma_0=\underline\gamma_0\) and \(\delta_0=\underline\delta_0\).
\end{proposition}

\begin{lemma}[RC1 is chamberwise constant]
\label{lem:rc1_chamberwise_constant}
Fix a candidate tight SCC \(H\) and a candidate witness word \(w\).
Let \(\mathcal{A}(H,w)\) denote the tight-language avoidance automaton used to encode RC1.
If \(H\) and \(w\) are fixed on \(\Theta\), then \(\mathcal{A}(H,w)\) is fixed on \(\Theta\).
Consequently, either RC1 holds for all \(\theta\in\Theta\) or RC1 fails for all \(\theta\in\Theta\).
In particular, RC1 can be verified at a single parameter value once the chamber is fixed.
\end{lemma}

\begin{proof}
RC1 is equivalent to the absence of a directed cycle in \(\mathcal{A}(H,w)\).
When \(H\) and \(w\) are fixed, the transition structure of \(\mathcal{A}(H,w)\) does not depend on \(\theta\).
Thus the cycle predicate is independent of \(\theta\), proving the claim.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:uniform_margins_via_lipschitz}]
Lemma~\ref{lem:lipschitz_min_cert} applied to \(f=\gamma\) and \(f=\delta_w\) yields \(\gamma(\theta)\ge\underline\gamma_0\) and \(\delta_w(\theta)\ge\underline\delta_0\) for all \(\theta\in\Theta\).
RC1 supplies the recurrence-forcing item.
Thus Definition~\ref{def:uniform_margins} holds with the certified bounds.
\end{proof}

\begin{remark}[How to obtain conservative Lipschitz constants]
The proposition treats \(L_{\gamma}\) and \(L_{\delta}\) as inputs.
In applications, one bounds these constants from the parameterization.
For example, if each template map \(\theta\mapsto A_k(\theta)\) is Lipschitz in operator \(\|\cdot\|_{\infty}\) with constant \(L_A\) and \(\max_{\theta\in\Theta}\|A_k(\theta)\|_{\infty}\le M\), then for a fixed word \(w\) of length \(L\) one has the conservative envelope
\[
\|P_w(\theta)-P_w(\theta')\|_{\infty} \;\le\; L\,L_A\,M^{L-1}\,\|\theta-\theta'\|,
\]
so one may take \(L_{\delta} \le L\,L_A\,M^{L-1}\).
For \(\gamma\), a corresponding bound can be obtained once the reduced-cost computation is expressed as a finite composition of linear maps and maxima/minima whose coefficients are bounded on \(\Theta\); the pipeline may record a conservative \(L_{\gamma}\) as part of the calibration contract.
At the artifact level, the parameter-family descriptor may declare the needed moduli explicitly via the \texttt{net\_certification\_contract} block in \texttt{theta\_family\_schema.json}.
\end{remark}

\subsection{Explicit Lipschitz constants for the margins on a fixed witness chamber}

On a chamber where the witness data are frozen, one can make the verification inputs
\(L_{\gamma}\) and \(L_{\delta}\) completely explicit.
The purpose of this subsection is to record conservative formulas that can be cited
without invoking any hidden regularity assumptions.

\begin{definition}[Chamberwise frozen witness project]
\label{def:frozen-witness-project}
Let \(\Theta\subset\mathbb{R}^d\) be a compact parameter region.
We say that \(\Theta\) lies in a \emph{frozen witness chamber} if there exist:
\begin{itemize}[leftmargin=2em]
\item a fixed calibrated pair \((u,\lambda_*)\),
\item a fixed tight edge set \(H\subseteq E\) defined by the sign test for \(c_u\) using \((u,\lambda_*)\),
\item a fixed Doeblin witness word \(w\) of length \(L\),
\end{itemize}
such that all certificates on \(\Theta\) are evaluated using this same data.
In particular, the margin functions are
\(
\gamma(\theta)=\min\{c_u(\theta,e): e\in E\setminus H\}\)
and
\(\delta_w(\theta)=\min(P_w(\theta))\)
with \(H\) and \(w\) fixed.
\end{definition}

\begin{lemma}[Lipschitz constant for the tightness gap under cost parameterization]
\label{lem:lipschitz_gamma_explicit}
Assume \(\Theta\) lies in a frozen witness chamber in the sense of Definition~\ref{def:frozen-witness-project}.
Assume the cost map \(\theta\mapsto c(\theta)\in\mathbb{R}^E\) is Lipschitz in \(\|\cdot\|_{\infty}\) with constant \(L_c\), i.e.
\(\|c(\theta)-c(\theta')\|_{\infty}\le L_c\,\|\theta-\theta'\|\) for all \(\theta,\theta'\in\Theta\).
Keep \((u,\lambda_*)\) fixed.
Then every reduced cost \(c_u(\theta,e)\) is Lipschitz with constant \(L_c\), and the tightness gap
\(\gamma(\theta)=\min_{e\in E\setminus H} c_u(\theta,e)\)
is Lipschitz with constant
\[
L_{\gamma}\le L_c.
\]
\end{lemma}

\begin{proof}
For fixed \((u,\lambda_*)\), the map \(c\mapsto c_u(e)=c(e)-\lambda_*+u(\mathrm{tail}(e))-u(\mathrm{head}(e))\) is affine with Lipschitz constant \(1\) in \(\|\cdot\|_{\infty}\).
Hence
\(|c_u(\theta,e)-c_u(\theta',e)|\le \|c(\theta)-c(\theta')\|_{\infty}\le L_c\,\|\theta-\theta'\|\).
The minimum of finitely many \(L_c\)-Lipschitz functions is \(L_c\)-Lipschitz, which yields the claim for \(\gamma\).
\end{proof}

\begin{lemma}[Lipschitz constant for the Doeblin margin under template parameterization]
\label{lem:lipschitz_delta_explicit}
Assume \(\Theta\) lies in a frozen witness chamber.
Fix a witness word \(w=w_1\cdots w_L\).
Assume each template map \(\theta\mapsto A^{(k)}(\theta)\) is Lipschitz in entrywise \(\|\cdot\|_{\infty,\mathrm{ent}}\) with constant \(L_A\), and assume a uniform bound
\(\max_{\theta\in\Theta}\max_{k,i,j} A^{(k)}_{ij}(\theta)\le M\).
Let \(P_w(\theta)=A^{(w_L)}(\theta)\cdots A^{(w_1)}(\theta)\) and \(\delta_w(\theta)=\min_{i,j}(P_w(\theta))_{ij}\).
Then \(\delta_w\) is Lipschitz with constant
\[
L_{\delta}\le L\,L_A\,M^{L-1}.
\]
\end{lemma}

\begin{proof}
The telescoping identity gives
\(
P_w(\theta)-P_w(\theta')=\sum_{t=1}^L
 A^{(w_L)}(\theta)\cdots A^{(w_{t+1})}(\theta)\bigl(A^{(w_t)}(\theta)-A^{(w_t)}(\theta')\bigr)A^{(w_{t-1})}(\theta')\cdots A^{(w_1)}(\theta')
\)
with the obvious conventions at the ends.
Taking entrywise \(\|\cdot\|_{\infty,\mathrm{ent}}\) and using the uniform bound \(M\) yields
\(
\|P_w(\theta)-P_w(\theta')\|_{\infty,\mathrm{ent}}\le \sum_{t=1}^L M^{L-1}\,\|A^{(w_t)}(\theta)-A^{(w_t)}(\theta')\|_{\infty,\mathrm{ent}}
\le L\,M^{L-1}\,L_A\,\|\theta-\theta'\|.
\)
Since \(\delta_w\) is the minimum of the finitely many entries of \(P_w\), it is 1-Lipschitz as a function of the entry vector, hence it inherits the same constant.
\end{proof}

\begin{remark}[Verified bounds without smoothness]
The formulas in Lemmas~\ref{lem:lipschitz_gamma_explicit} and~\ref{lem:lipschitz_delta_explicit} only use
finite-dimensional Lipschitz envelopes and do not require differentiability.
When a parameter map is only piecewise-Lipschitz, one may apply the same verification locally on each piece
and then use the chamberwise cover mechanism (Algorithm~\ref{alg:global-universality}).
\end{remark}
