\subsection*{Predicate exhaustion: minimal completeness skeleton}

SFT treats \emph{validator predicates} as the formal boundary between certificate-claims and obstruction-claims.

The audit-facing specification of the predicate suite and its canonical mapping appears in \texttt{VALIDATOR\_PREDICATE\_SPEC.tex} (and in the runnable contract files under \codeid{engine/contracts}).
Inside the declared regime, a witness stability certificate (WSC) is permitted only when the listed predicates hold on the declared target.
When a predicate fails, the correct output is a witness obstruction (WOB) with a canonical code and a finite evidence checklist.

\subsection*{Validator predicates and canonical WOB codes}

Write $\mathrm{V}_{\mathrm{XX}}$ for the validator predicate associated to obstruction code \codeid{WOB-XX}.
The intended reading is:

\begin{itemize}[leftmargin=*]
\item if $\mathrm{V}_{\mathrm{XX}}$ holds, then \codeid{WOB-XX} is \emph{not} triggered by that failure mode,
\item if $\mathrm{V}_{\mathrm{XX}}$ fails, then \codeid{WOB-XX} is the correct obstruction code to report (with evidence).
\end{itemize}

The predicates are:

\begin{itemize}[leftmargin=*]
\item \textbf{$\mathrm{V}_{01}$ (subsystem/observable present).}
There exists an admissible subsystem (slice, orbit-domain, or embedded loop/defect domain) and a phase observable to a declared target $\mathbb{T}_P$ or $\mathbb{T}_{\mathbf P}$.
If this fails, report \codeid{WOB-01-no-subsystem}.

\item \textbf{$\mathrm{V}_{02}$ (nontrivial winding/holonomy).}
In an embedded mechanism, some certified loop carries a nonzero integer witness (degree or holonomy multiple).
If this fails, report \codeid{WOB-02-trivial-winding}.

\item \textbf{$\mathrm{V}_{03}$ (no pinch on the declared target).}
On the declared target, the observable image does not miss a positive-length arc neighborhood required for SCL.
If this fails, report \codeid{WOB-03-pinch}.

\item \textbf{$\mathrm{V}_{04}$ (no tear: definability/regularity).}
The hypotheses needed to define degree/holonomy in the adopted model class hold on the evidence domain (liftability/atlas consistency/continuity at the declared tolerance).
If this fails, report \codeid{WOB-04-tear}.

\item \textbf{$\mathrm{V}_{05}$ (holonomy consistency).}
In holonomy-based mechanisms, the lift/connection interface is consistent at the declared tolerance so the holonomy integer is well-defined.
If this fails, report \codeid{WOB-05-holonomy-defect}.

\item \textbf{$\mathrm{V}_{06}$ (coupled target correctness).}
In coupled settings, the selected target is the coupled subtorus coset $\mathrm{CST}_s$ and the baseline is coupled Haar on $\mathrm{CST}_s$.
If this fails, report \codeid{WOB-06-coupling-mismatch}.

\item \textbf{$\mathrm{V}_{07}$ (mixing claim justified).}
Any statistical convergence claim is accompanied by an admissible certificate hypothesis (RNF or NDB+MXC, with declared parameters).
If this fails, report \codeid{WOB-07-mixing-not-justified}.

\item \textbf{$\mathrm{V}_{08}$ (orbit realized on the evidence domain).}
In action-equivariant mechanisms, the evidence domain contains a $\chi$-active circle-type orbit segment needed for the forcing template.
If this fails, report \codeid{WOB-08-orbit-collapse}.

\item \textbf{$\mathrm{V}_{09}$ (equivariance within tolerance).}
The equivariance defect is within the declared admissible tolerance on the evidence domain.
If this fails, report \codeid{WOB-09-equivariance-defect}.

\item \textbf{$\mathrm{V}_{10}$ (no resonant locking for the intended target).}
The response rank and the inferred constraint structure do not collapse the intended target (full torus versus subtorus coset).
If this fails, report \codeid{WOB-10-resonant-locking}.

\item \textbf{$\mathrm{V}_{11}$ (connected slice/component availability).}
The declared measurement domain intersects the orbit-bearing/loop-bearing component required by the chosen mechanism.
If this fails, report \codeid{WOB-11-disconnected-slice}.

\item \textbf{$\mathrm{V}_{12}$ (slope-zero quotient surjectivity when needed).}
When the induced homomorphism $\chi$ is trivial, the factor map through the quotient is surjective onto the declared target.
If this fails, report \codeid{WOB-12-slope-zero-quotient-nonsurjective}.
\item  \textbf{$\mathrm{V}_{13}$ (constraint hypothesis uniqueness).}
In constraint/target inference, the declared data and tolerance determine a unique small-integer constraint hypothesis within the declared finite search.
If this fails, report  exttt{WOB-13-ambiguity}.

\item  \textbf{$\mathrm{V}_{14}$ (sufficient excitation for inference).}
The sample count and excitation are sufficient to support stable inference of constraint rank and target rank at the declared tolerance.
If this fails, report  exttt{WOB-14-insufficient-excitation}.

\item  \textbf{$\mathrm{V}_{15}$ (stability margin away from resonance).}
The best constraint candidates are separated from the declared tolerance by a positive stability margin; near-relations do not make the decision unstable.
If this fails, report  exttt{WOB-15-resonance-masking}.
\end{itemize}

\subsection*{Lemma suite (each predicate failure forces its WOB code)}

\begin{lemma}[\codeid{WOB-01} is forced by $\neg\mathrm{V}_{01}$]
If no admissible subsystem/observable exists in the declared regime, then no WSC exists in that regime.
\end{lemma}
\begin{proof}
Every WSC is defined on a declared evidence domain and records a target and observable.
If such data do not exist in the declared regime, then no WSC object satisfying the regime validators can exist.
\end{proof}

\begin{lemma}[\codeid{WOB-02} is forced by $\neg\mathrm{V}_{02}$]
If every admissible loop mechanism in the evidence domain has zero degree and zero holonomy multiple, then no embedded-loop WSC with nonzero witness integer exists.
\end{lemma}
\begin{proof}
Embedded-loop WSCs require an integer witness invariant that persists under the LCM/HMR margins.
If all admissible loops have witness integer $0$, then the mechanism cannot certify forced coverage by winding/holonomy and the obstruction is the trivial-winding class.
\end{proof}

\begin{lemma}[\codeid{WOB-03} is forced by $\neg\mathrm{V}_{03}$]
If the observable image misses a required arc neighborhood on the declared target, then SCL on that target cannot hold, hence no target-correct WSC exists.
\end{lemma}
\begin{proof}
SCL asserts surjectivity onto the declared target.
Missing an arc neighborhood contradicts surjectivity, so no WSC proving SCL on that target can exist.
\end{proof}

\begin{lemma}[\codeid{WOB-04} is forced by $\neg\mathrm{V}_{04}$]
If the adopted model class does not provide the regularity needed to define the witness invariant (degree/holonomy) robustly at the declared tolerance, then no WSC with certified margins exists.
\end{lemma}
\begin{proof}
The WSC format requires a well-defined integer witness together with margins certifying its stability.
If the witness cannot be defined in the adopted model class on the evidence domain, the certificate interface cannot be satisfied.
\end{proof}

\begin{lemma}[\codeid{WOB-05} is forced by $\neg\mathrm{V}_{05}$]
If holonomy consistency fails at the declared tolerance, then holonomy-based certification is ill-posed in that regime and no holonomy WSC exists.
\end{lemma}
\begin{proof}
Holonomy WSCs require a connection/lift interface whose loop integral is well-defined modulo the period.
If the interface is inconsistent, the holonomy integer is not stable or not defined, and the holonomy-defect obstruction is the correct output.
\end{proof}

\begin{lemma}[\codeid{WOB-06} is forced by $\neg\mathrm{V}_{06}$]
In a coupled setting, if the target is not declared as $\mathrm{CST}_s$ with coupled Haar baseline, then any claimed certificate is target-incorrect and no target-correct WSC exists without repairing the target.
\end{lemma}
\begin{proof}
Coupling changes the maximal invariant set and the correct baseline measure.
A certificate that uses the wrong target/baseline is not a WSC in the declared target-correct regime.
\end{proof}

\begin{lemma}[\codeid{WOB-07} is forced by $\neg\mathrm{V}_{07}$]
If a statistical convergence claim is asserted without an admissible hypothesis certificate (RNF or NDB+MXC), then the claim is outside the permitted regime and the correct output is the mixing-not-justified obstruction.
\end{lemma}
\begin{proof}
SFT treats convergence as an additional artifact class whose hypotheses must be declared and auditable.
Without an admissible hypothesis certificate, no convergence certificate can be issued, so the regime boundary is triggered.
\end{proof}

\begin{lemma}[\codeid{WOB-08} is forced by $\neg\mathrm{V}_{08}$]
If the $\chi$-active orbit needed by the equivariant forcing template is absent from the evidence domain, then action-equivariant forcing cannot be invoked there and no forcing-based WSC exists on that domain.
\end{lemma}
\begin{proof}
The forcing template certifies coverage by transporting phases along a realized orbit.
If no such orbit occurs on the evidence domain, the mechanism is unavailable and the orbit-collapse class is the correct obstruction.
\end{proof}

\begin{lemma}[\codeid{WOB-09} is forced by $\neg\mathrm{V}_{09}$]
If equivariance defect exceeds the declared tolerance, then equivariance is not valid in the adopted model class at that tolerance and no equivariance-based WSC exists.
\end{lemma}
\begin{proof}
Equivariance-based WSCs require the defect to be within tolerance so that the induced homomorphism controls orbit images.
If the defect is too large, the required mechanism hypotheses fail.
\end{proof}

\begin{lemma}[\codeid{WOB-10} is forced by $\neg\mathrm{V}_{10}$]
If rank deficiency or resonant locking collapses the intended target, then no certificate can truthfully assert coverage of the larger target; the correct output is the resonant-locking obstruction (and the target must be revised).
\end{lemma}
\begin{proof}
The correct target is determined by the response rank and by any valid integer constraints.
If the intended target is larger than the reachable coset/subtorus, coverage of the larger target is impossible.
\end{proof}

\begin{lemma}[\codeid{WOB-11} is forced by $\neg\mathrm{V}_{11}$]
If the declared measurement domain does not meet the required orbit-bearing/loop-bearing component, then no certificate for that mechanism can be produced from that domain.
\end{lemma}
\begin{proof}
All certificate mechanisms require evidence on a domain supporting the relevant orbit or loop.
If the domain misses that component, the mechanism is inapplicable there.
\end{proof}

\begin{lemma}[\codeid{WOB-12} is forced by $\neg\mathrm{V}_{12}$]
If $\chi$ is trivial and the quotient factor map is not surjective onto the declared target, then SCL on that target is impossible and no target-correct WSC exists.
\end{lemma}
\begin{proof}
When $\chi$ is trivial, equivariance forces the observable to factor through the quotient.
If the induced factor is not surjective, the declared target cannot be covered.
\end{proof}

\begin{lemma}[ exttt{WOB-13} is forced by $
eg\mathrm{V}_{13}$]
If multiple incompatible small-integer constraint hypotheses fit within the declared tolerance and search, then the target is not uniquely determined in the declared regime and no target-correct certificate can be issued without additional excitation or a refined target declaration.
\end{lemma}
\begin{proof}
A target-correct certificate requires a declared target type and, when constraints are part of the target selection, a determinate constraint hypothesis.
If the declared data/tolerance admit more than one incompatible constraint hypothesis within the search, any choice is non-auditable without additional information, so the declared regime treats this as an explicit inference obstruction.
\end{proof}

\begin{lemma}[ exttt{WOB-14} is forced by $
eg\mathrm{V}_{14}$]
If the sample count or excitation is insufficient to support stable constraint inference at the declared tolerance, then inference is ill-posed in the declared regime and the correct output is  exttt{WOB-14-insufficient-excitation}.
\end{lemma}
\begin{proof}
Stable inference requires enough samples and enough motion to distinguish candidate constraint hypotheses.
When these are absent, any inferred constraints can change under small perturbations of the data, so no target-correct certificate can be issued in the declared regime.
\end{proof}

\begin{lemma}[ exttt{WOB-15} is forced by $
eg\mathrm{V}_{15}$]
If the best candidate constraints are within the declared tolerance by too small a margin, or if a near-relation lies just above tolerance, then the constraint decision is unstable at the declared tolerance and the correct output is  exttt{WOB-15-resonance-masking}.
\end{lemma}
\begin{proof}
A positive stability margin is needed so that the inferred constraints persist under admissible perturbations.
When the margin is too small or a near-relation is present, small perturbations can change the inferred target rank or constraint set, so the declared regime treats the situation as a resonance-masking obstruction.
\end{proof}
