% TARGET_CORRECTNESS_AXIOMS.tex

\providecommand{\CST}{\ensuremath{\mathrm{CST}}}

\paragraph{Target correctness axiom block (CTP/CHT).}
SFT treats \emph{target correctness} as part of the meaning of any certificate-or-obstruction claim.
A declared claim must state (i) the \emph{target type} (circle / full torus / coupled target) and (ii) the \emph{baseline measure} used for any comparison, stability, or convergence upgrade.

\begin{itemize}[leftmargin=*]
\item \textbf{Circle or full torus targets.}
When the correct target is a compact group target $\mathbb{T}_P$ or $\mathbb{T}_{\mathbf P}$, the baseline is the (unique) Haar probability measure on that target.
\item \textbf{Coupled targets (CST).}
When coupling constraints restrict the image to a coupled subtorus coset,
\[
\CST_s\;:=\;\{y\in \mathbb{T}_{\mathbf P}: Ay=\Psi(s)\},\qquad A\in\mathbb{Z}^{r\times d},
\]
then the correct target is $\CST_s$ (not the ambient torus) and the baseline is the (unique) translation-invariant probability measure on $\CST_s$.
Equivalently, for any parameterization $\eta_s:\mathbb{T}_{P_*}^m\to \CST_s$, the baseline is the pushforward of Haar:
\[
\mu^{\CST}_{\mathrm H,s}:=(\eta_s)_\#\mu_{\mathrm H}^{(m)}.
\]
\end{itemize}

\paragraph{CTP (Coupled Target Principle).}
If the declared context includes coupling constraints yielding a coupled target $\CST_s$, then all coverage statements, stability margins, and upgrades are to be interpreted \emph{relative to $\CST_s$}.
Using the ambient torus as the target in this regime is not a weaker claim; it is a \emph{different} claim.

\paragraph{CHT (Coupled Haar Theorem, as baseline convention).}
In the coupled regime, the baseline for comparisons is $\mu^{\CST}_{\mathrm H,s}$.
Any convergence or mixing claim must specify this baseline when the target is $\CST_s$.

\paragraph{Corollary (wrong target/baseline forces a boundary obstruction).}
If a declared claim uses a target/baseline pair incompatible with the declared coupling structure
(e.g., it uses full-torus Haar when the correct target is $\CST_s$), then the claim is \emph{ill-posed in SFT}.
The correct engine output in that case is the coupling-mismatch obstruction \texttt{WOB-06-coupling-mismatch}.
