Independence of Prime-Level Actions

Prime-level actions T^(i) on ℤ/pᵢℤ are independent. CRT guarantees unique reassembly into global action on ℤ/Prim(k)ℤ. The τ-incarnation of the local-global principle.

Independence of Prime-Level Actions

Summary

Prime-level actions T^(i) on ℤ/pᵢℤ are independent. CRT guarantees unique reassembly into global action on ℤ/Prim(k)ℤ. The τ-incarnation of the local-global principle.

Statement

%
\label{prop:prime-independence}
Let $T, T'$ be endomorphisms of $\Z / \mathrm{Prim}(k)\Z$
with CRT decompositions
$(T^{(1)}, \ldots, T^{(k)})$
and $(T'^{(1)}, \ldots, T'^{(k)})$.
Then:
\begin{enumerate}
    \item[\textup{(i)}] \textbf{Independence.}
          For any $\tilde{T}^{(i)} \in \mathrm{End}(\Z / p_i \Z)$,
          there exists a unique $\tilde{T}$
          with CRT decomposition
          $(T^{(1)}, \ldots, \tilde{T}^{(i)}, \ldots, T^{(k)})$.
          Modifying one prime does not affect the others.
    \item[\textup{(ii)}] \textbf{Composition.}
          $T \circ T'$ has CRT decomposition
          $(T^{(1)} \circ T'^{(1)}, \ldots,
          T^{(k)} \circ T'^{(k)})$.
    \item[\textup{(iii)}] \textbf{Equality.}
          $T = T'$ if and only if
          $T^{(i)} = T'^{(i)}$
          for all~$i$.
\end{enumerate}

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 43
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch15-the-crt-decomposition-theorem.tex lines 421-445

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.CRT
• Name: prime_independence_check

Dependencies

• Canonical: III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.