CRT Witness Decomposition

Witness space at primorial depth k factors: W(x, Prim(k)) ≅ ∏ W(x, p_i). Each prime contributes independent 1D search. CRT guarantees reconstruction. Product of costs becomes sum of costs.

CRT Witness Decomposition

Summary

Witness space at primorial depth k factors: W(x, Prim(k)) ≅ ∏ W(x, p_i). Each prime contributes independent 1D search. CRT guarantees reconstruction. Product of costs becomes sum of costs.

Statement

\label{prop:crt-witness-decomposition}
Let $\Pi$ be $\tau$-admissible, $x$ a ``yes'' instance, and $k$ the
primorial depth of the TTM verifier. Then:
\[
W(x, k) \;\cong\; \prod_{i=1}^{k} W(x, p_i),
\]
where $W(x, p_i) \subseteq \mathbb{Z}/p_i\mathbb{Z}$ is the
\textbf{per-prime witness space}. Moreover:
\begin{enumerate}
\item \textbf{Independence.}
      $w_i$ at $p_i$ does not constrain $w_j$ at $p_j$ for $j \neq i$.
\item \textbf{Unique reassembly.}
      Given $(w_1, \ldots, w_k)$, the CRT produces a unique
      $w \in W(x, k)$ with $w \equiv w_i \pmod{p_i}$ for all $i$.
\item \textbf{Cardinality.}
      $|W(x, k)| = \prod_{i=1}^{k} |W(x, p_i)|$.
\end{enumerate}

Proof / Justification

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

Source Context

• Registry source: book-03.jsonl line 153
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part09/ch57-witness-search-as-address-resolution.tex lines 127-145

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Computation.WitnessSearch
• Name: crt_witness_check

Dependencies

• Canonical: III.D55, III.T10

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.