CRT Decomposition Theorem

τ-native Chinese Remainder Theorem: ℤ/Prim(k)ℤ ≅ ∏ᵢ₌₁ᵏ ℤ/pᵢℤ proved constructively without signed arithmetic. Uses modular Bézout via K3 divisibility. CRT = algebraic Euler product: End(F) ≅ ∏ End(ℤ/pᵢℤ).

CRT Decomposition Theorem

Summary

τ-native Chinese Remainder Theorem: ℤ/Prim(k)ℤ ≅ ∏ᵢ₌₁ᵏ ℤ/pᵢℤ proved constructively without signed arithmetic. Uses modular Bézout via K3 divisibility. CRT = algebraic Euler product: End(F) ≅ ∏ End(ℤ/pᵢℤ).

Statement

%
\label{thm:crt-decomposition}
For each $k \geq 1$, the canonical ring homomorphism
\begin{equation}\label{eq:ch15-crt-iso}
    \Phi_k \;:\;
    \Z / \mathrm{Prim}(k)\Z
    \;\longrightarrow\;
    \prod_{i=1}^{k} \Z / p_i \Z,
    \qquad
    \Phi_k(x) \;=\; (x \bmod p_1,\, \ldots,\, x \bmod p_k),
\end{equation}
is an isomorphism of rings.
Its inverse is the idempotent assembly:
\begin{equation}\label{eq:ch15-crt-inverse}
    \Phi_k^{-1}(a_1, \ldots, a_k)
    \;=\;
    \sum_{i=1}^{k} a_i \cdot e_i
    \;\bmod\; \mathrm{Prim}(k).
\end{equation}
The construction is purely $\tau$-internal:
multiplication ($\KAxiom{2}$),
divisibility ($\KAxiom{3}$),
and finite enumeration.
No subtraction, no signed arithmetic,
no extended Euclidean algorithm.

Proof / Justification

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

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: III.D19, III.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.