Product-Meet Collapse

At E₂, meet (∧ = finding a witness) IS product (× = constructing the composite). Search = construction. This is the computational content of the bi-square pasting. Proof via Interface Width Principle + CRT decomposition.

Product-Meet Collapse

Summary

At E₂, meet (∧ = finding a witness) IS product (× = constructing the composite). Search = construction. This is the computational content of the bi-square pasting. Proof via Interface Width Principle + CRT decomposition.

Statement

\label{thm:product-meet-collapse}
Let $\Pi$ be $\tau$-admissible with verifier width $k_0$, and let $x$
be a ``yes'' instance at depth $k \geq k_0$. Then the pasting of the
execution and witness squares
in~\eqref{eq:ch58-computational-bisquare} yields
\begin{equation}\label{eq:ch58-product-meet}
    \underbrace{w_1 \wedge w_2 \wedge \cdots \wedge w_k}%
      _{\text{meet: satisfy all primes}}
    \;=\;
    \underbrace{w_1 \times w_2 \times \cdots \times w_k}%
      _{\text{product: CRT reassembly}},
\end{equation}
where $w_i \in W(x, p_i)$ is a per-prime witness
(Proposition~\ref{prop:crt-witness-decomposition}).

Proof / Justification

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

Source Context

• Registry source: book-03.jsonl line 156
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part09/ch58-the-computational-bi-square.tex lines 125-140

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Computation.CompBiSquare
• Name: product_meet_collapse_check

Dependencies

• Canonical: III.D56, III.T31, III.P22

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.