% COC_multicycle_proof.tex
% including the correct target when the response has deficient rank and when coupling forces a CST.
%
% This file is intended to be \input{} into SFT I/II/III and the global universality pack.

\providecommand{\TorusVecP}{\ensuremath{\mathbb{T}_{\mathbf P}}}
\providecommand{\COC}{\ensuremath{\mathrm{COC}}}
\providecommand{\CST}{\ensuremath{\mathrm{CST}}}

\subsection*{Canonical proof template: multi-cycle forcing and correct coupled targets}

\begin{theorem}[\texorpdfstring{$\mathbb{T}^k$}{Tk}-action forcing template: image subtorus and effective target rank]
\label{thm:torus-action-template}
Let $\Sigma$ be a slice and let $A:\mathbb{T}^k\times\Sigma\to\Sigma$ be a continuous $\mathbb{T}^k$-action.
Let $\Phi:\Sigma\to\TorusVecP$ be continuous.
Assume there exists a continuous homomorphism $\chi:\mathbb{T}^k\to\TorusVecP$ such that on a declared domain $D\subseteq\Sigma$,
\begin{equation}
\label{eq:Tk-equivariance}
\Phi(A(u,x))=\Phi(x)\oplus\chi(u)\qquad \forall(u,x)\in\mathbb{T}^k\times D.
\end{equation}
Define the (possibly lower-dimensional) response subtorus
\[
\mathrm{Im}(\chi):=\chi(\mathbb{T}^k)\subseteq\TorusVecP.
\]
Then for every $x\in D$,
\[
\Phi\big(A(\mathbb{T}^k,x)\big)=\Phi(x)\oplus\mathrm{Im}(\chi).
\]
In particular, the action-forcing mechanism forces coverage on the \emph{coset target} $\Phi(x)\oplus\mathrm{Im}(\chi)$.
A universality claim in this setting is therefore well-posed only when its declared target agrees with this coset (or an explicitly declared coupled target contained in it).

Moreover, after choosing standard identifications
$\mathbb{T}^k\cong\mathbb{R}^k/2\pi\mathbb{Z}^k$ and
$\TorusVecP\cong\prod_{j=1}^m \mathbb{R}/P_j\mathbb{Z}$,
there exists an integer matrix $M\in\mathbb{Z}^{m\times k}$ such that $\chi$ lifts to the linear map $t\mapsto \mathrm{diag}(P_1/2\pi,\dots,P_m/2\pi)\,M t$ on universal covers.
The \emph{effective target rank} is
\[
 r:=\mathrm{rank}(M)=\dim\big(\mathrm{Im}(\chi)\big),
\]
so the response rank determines the target rank: the correct target cannot have dimension larger than $r$.
\end{theorem}

\begin{proof}
Fix $x\in D$.
For any $u\in\mathbb{T}^k$, \eqref{eq:Tk-equivariance} gives $\Phi(A(u,x))=\Phi(x)\oplus\chi(u)$.
Thus
\[
\Phi\big(A(\mathbb{T}^k,x)\big)=\{\Phi(x)\oplus\chi(u):u\in\mathbb{T}^k\}=\Phi(x)\oplus\chi(\mathbb{T}^k)=\Phi(x)\oplus\mathrm{Im}(\chi).
\]
This is exactly the coset identity.

For the rank statement, observe that continuous homomorphisms between tori are induced by integer matrices on fundamental groups.
Under the standard coordinate identifications, a homomorphism $\chi:\mathbb{T}^k\to\TorusVecP$ admits a lift to a linear map on universal covers whose matrix has integer entries up to the fixed diagonal period scaling.
The image $\mathrm{Im}(\chi)$ is a closed connected subgroup of $\TorusVecP$, hence a subtorus, and its dimension equals the rank of the inducing integer matrix $M$.
\end{proof}

\begin{theorem}[Coupling forces a coupled target (CST) and a coupled Haar baseline]
\label{thm:coupling-forces-cst}
Let $\Phi:\Sigma\to\TorusVecP$ be a multi-cycle phase observable and suppose the declaration includes a coupling law on the same domain $D$ that restricts the image to a coset of a subtorus.
In the integer-matrix atlas class this has the form
\begin{equation}
\label{eq:cst-constraint}
A\,\Phi(x)=\Psi(s)\qquad \forall x\in D\cap\Sigma_s,
\end{equation}
for a fixed small-integer matrix $A$ (declared or inferred) and a slice-dependent offset $\Psi(s)$.
Define the coupled target on slice $s$ by
\[
\CST_s:=\{y\in\TorusVecP: A y=\Psi(s)\}.
\]
Then any coverage, stability, or baseline statement is meaningful only on $\CST_s$.
In particular:
\begin{itemize}[leftmargin=*]
\item If a claim uses the full torus as its target when \eqref{eq:cst-constraint} holds, the claim is ill-posed and the correct engine output is the coupling-mismatch obstruction (WOB-06).
\item The correct uniform baseline in coupled settings is Haar on $\CST_s$ (equivalently, the pushforward of Haar on the free-coordinate parameterization of $\CST_s$).
\item In the presence of a $\mathbb{T}^k$-action equivariance \eqref{eq:Tk-equivariance}, the forced target is the intersection of the response coset from Theorem~\ref{thm:torus-action-template} with the coupled target; in the target-correct regime these coincide because the declaration chooses $\CST_s$ as the target.
\end{itemize}
\end{theorem}

\begin{proof}
The set $\CST_s$ defined by \eqref{eq:cst-constraint} is, by construction, a coset of the subtorus $\ker(A)$.
Thus it is a legitimate torus-type target equipped with its intrinsic Haar measure.
A statement phrased on the full torus while the dynamics and observable are confined to $\CST_s$ changes the meaning of ``coverage'' and ``uniformity'' and therefore is not a well-posed SFT claim.

If, in addition, \eqref{eq:Tk-equivariance} holds, then by Theorem~\ref{thm:torus-action-template} the action-forced image on any orbit is a translate of $\mathrm{Im}(\chi)$.
When the declaration is target-correct, the target selection rule chooses the coupled target coset that actually contains the image; this is exactly the role of $\CST_s$.
\end{proof}

\begin{theorem}[Multi-cycle forcing yields a COC embedding on the correct target]
\label{thm:multicycle-coc}
Assume a declared context provides:
(PO) a multi-cycle phase observable $\Phi$,
(WM) an admissible $\mathbb{T}^k$-action $A$ with equivariance \eqref{eq:Tk-equivariance} on a domain $D$,
and (TR) the target rule selecting the correct coset target (the response image coset, or a coupled target $\CST_s$ when coupling constraints are present).
Then the declared context belongs to \COC\ on $D$.
Consequently, on the correct target (with Haar or coupled Haar baseline as appropriate), the SFT engine posture applies: the correct output is either a WSC with explicit margins, or a finite WOB with evidence.
\end{theorem}

\begin{theorem}[Frame/gauge invariance (FEQ) in the multi-cycle setting]
\label{thm:Tk-feq}
Assume two declared contexts are related by a frame/gauge equivalence (FEQ) that preserves slice identification and conjugates the $\mathbb{T}^k$-action and phase observable on the declared domain $D$:
there is a homeomorphism $F:D\to D'$ such that $F(A(u,x))=A'(u,F(x))$ and $\Phi'\circ F=\Phi$.
Then the coset identity in Theorem~\ref{thm:torus-action-template} and the coupled-target correctness statement in Theorem~\ref{thm:coupling-forces-cst} are invariant under the FEQ change of description.
\end{theorem}
