% COC_rotation_proof.tex
%
% This file is intended to be \input{} into SFT I/II/III and the global universality pack.

\providecommand{\TorusP}{\ensuremath{\mathbb{T}_P}}
\providecommand{\COC}{\ensuremath{\mathrm{COC}}}

\subsection*{Canonical proof template: circle-action forcing (rotation / periodic forcing)}

\begin{theorem}[Circle-action forcing template]
\label{thm:circle-action-template}
Let $\Sigma$ be a slice and let $A:S^1\times \Sigma\to\Sigma$ be a continuous $S^1$-action.
Let $\phi:\Sigma\to \TorusP$ be continuous.
Assume there exists a continuous homomorphism $\chi:S^1\to \TorusP$ such that on a declared domain $D\subseteq\Sigma$,
\begin{equation}
\label{eq:chi-equivariance}
\phi(A(\theta,x))=\phi(x)\oplus \chi(\theta)\qquad \forall(\theta,x)\in S^1\times D .
\end{equation}
Write $\deg(\chi)\in\mathbb{Z}$ for the integer degree of $\chi$.

\begin{itemize}[leftmargin=*]
\item If $\deg(\chi)\neq 0$, then for every $x\in D$ the orbit loop $\gamma_x:S^1\to\Sigma$, $\gamma_x(\theta)=A(\theta,x)$ satisfies
\[
\deg(\phi\circ\gamma_x)=\deg(\chi)\neq 0,
\]
and $\phi(D)=\TorusP$.
In particular, the declaration $(\Sigma,\phi)$ satisfies the COC checklist on $D$ with:
(PO) phase observable $\phi$,
(WM) action forcing and embedded loop witness,
(TR) circle target with Haar baseline.
\item If $\deg(\chi)=0$, then $\phi$ is $S^1$-invariant on $D$ and factors through the orbit quotient $q:D\to D/S^1$:
there exists $\bar\phi:D/S^1\to \TorusP$ with $\phi|_D=\bar\phi\circ q$.
In this case, coverage on $\TorusP$ can occur only through surjectivity of $\bar\phi$.
\end{itemize}
\end{theorem}

\begin{proof}
Every continuous homomorphism $\chi:S^1\to S^1$ has the form \cite{bredon1972,hatcher2002}: $\chi(e^{2\pi i t})=e^{2\pi i m t}$ for a unique $m\in\mathbb{Z}$, and $\deg(\chi)=m$.

Fix $x\in D$.
Define $\gamma_x(\theta)=A(\theta,x)$.
By \eqref{eq:chi-equivariance},
\[
(\phi\circ\gamma_x)(\theta)=\phi(A(\theta,x))=\phi(x)\oplus\chi(\theta).
\]
Translation by the constant $\phi(x)$ does not change degree \cite{hatcher2002}, hence
$\deg(\phi\circ\gamma_x)=\deg(\chi)$.

If $\deg(\chi)\neq 0$, then $\chi$ is surjective onto $\TorusP$.
For any $y\in\TorusP$, choose $\theta\in S^1$ with $\chi(\theta)=y\ominus \phi(x)$.
Then $\phi(A(\theta,x))=\phi(x)\oplus\chi(\theta)=y$, so $\phi(D)=\TorusP$.
The nonzero degree identity above supplies an embedded loop/holonomy witness, and the equivariance identity supplies an admissible action-forcing witness mechanism.

If $\deg(\chi)=0$, then $\chi$ is trivial, so \eqref{eq:chi-equivariance} gives $\phi(A(\theta,x))=\phi(x)$ for all $\theta$ and all $x\in D$.
Thus $\phi$ is constant along orbits in $D$ and therefore factors through the orbit space \cite{bredon1972}: there exists $\bar\phi$ with $\phi|_D=\bar\phi\circ q$.
\end{proof}

\begin{theorem}[Periodic forcing / rotation model as a COC embedding]
\label{cor:periodic-forcing-coc}
Let $\Sigma$ be a slice in a declared model class and assume the declaration includes a continuous $S^1$-action $A$ and a continuous phase observable $\phi:\Sigma\to\TorusP$ satisfying \eqref{eq:chi-equivariance} on a domain $D$ with $\deg(\chi)\neq 0$.
Then the declared context belongs to \COC\ on $D$.
Consequently, on the correct circle target (with Haar baseline), 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)]
\label{cor:circle-action-feq}
Assume two declared contexts are related by a frame/gauge equivalence (FEQ) that preserves slice identification and conjugates the $S^1$-action and phase observable on the declared domain $D$:
there is a homeomorphism $F:D\to D'$ such that $F(A(\theta,x))=A'(\theta,F(x))$ and $\phi' \circ F=\phi$.
Then the degree identity $\deg(\phi\circ\gamma_x)=\deg(\chi)$ and the forcing/quotient dichotomy in Theorem~\ref{thm:circle-action-template} are invariant under the FEQ change of description.
\end{theorem}
