PRP0024canonicalv1No Simultaneous Projection
No Simultaneous Projection: the diagonal-free discipline prevents any omega-tail from projecting nontrivially onto BOTH idempotent sectors e_plus and e_minus simultaneously.
Payload
No Simultaneous Projection
No Simultaneous Projection: the diagonal-free discipline prevents any omega-tail from projecting nontrivially onto BOTH idempotent sectors e_plus and e_minus simultaneously.
No Simultaneous Projection
Summary
No Simultaneous Projection: the diagonal-free discipline prevents any omega-tail from projecting nontrivially onto BOTH idempotent sectors e_plus and e_minus simultaneously.
Statement
%
\label{prop:no-simul-projection}
Let $t = (x_k)_{k \geq 1}$ be a compatible omega-tail
(satisfying the reduction conditions of the primorial tower),
and let $T \in \mathrm{HolFun}$ be a $\tau$-holomorphic function.
Then the canonical sector projections
$\chi_+(T(t))$ and $\chi_-(T(t))$
cannot \emph{both} be nontrivial at every stage
of the primorial ladder.
More precisely:
at each primorial stage $M_k$,
the CRT decomposition
\[
\mathbb{Z}/M_k\mathbb{Z}
\;\cong\;
\prod_{i=1}^{k} \mathbb{Z}/p_i\mathbb{Z}
\]
assigns each CRT factor $\mathbb{Z}/p_i\mathbb{Z}$
to exactly one sector via the Prime Polarity Theorem (I.T05):
to the $B$-sector if $\mathrm{pol}(p_i) = +$,
or to the $C$-sector if $\mathrm{pol}(p_i) = -$.
The diagonal-discipline axiom (K5, I.D03)
forbids any program from simultaneously accessing
generators from both sectors in the same application step.
Therefore, $T$'s output in the $B$-sector
depends only on $B$-sector inputs,
and $T$'s output in the $C$-sector
depends only on $C$-sector inputs.
An omega-germ cannot project nontrivially onto both sectors
simultaneously through a $\tau$-holomorphic function.
Proof / Justification
Consider a compatible omega-tail $t = (x_k)_{k \geq 1}$.
At stage $M_k$, the CRT decomposition
assigns each prime $p_i$ ($1 \leq i \leq k$)
to the $B$-sector (if $\mathrm{pol}(p_i) = +$)
or to the $C$-sector (if $\mathrm{pol}(p_i) = -$).
The $B$-sector projection at stage $k$
acts only on the $B$-sector CRT factors;
the $C$-sector projection acts only on the $C$-sector factors.
For a $\tau$-holomorphic function $T \in \mathrm{HolFun}$,
tower coherence (I.D46)
and D-holomorphy --- specifically,
sector independence (I.P22) ---
together ensure that
$T$'s $B$-sector output depends only on $B$-sector inputs
and $T$'s $C$-sector output depends only on $C$-sector inputs.
The diagonal discipline (I.D03) is the axiom-level guarantee
that programs cannot mix these sectors:
no single denotational step simultaneously applies generators
from both the $B$-sector and the $C$-sector.
This is precisely the content of axiom K5 ---
the no-diagonals constraint introduced in
Chapter~\ref{ch:diagonal-discipline}.
Combining these three ingredients:
\begin{enumerate}
\item \emph{CRT partition}: each prime belongs to exactly one sector
(I.T05);
\item \emph{Sector independence}: $T$ decomposes as
$T(u, v) = (g(u), h(v))$ in sector coordinates (I.P22);
\item \emph{Diagonal discipline}: no program step
can access generators from both sectors simultaneously
(I.D03).
\end{enumerate}
It follows that an omega-germ cannot
``project nontrivially onto both sectors simultaneously''
through $T$.
If $t$ is purely $B$-sector at every stage,
then $\chi_-(T(t))$ is determined
entirely by the trivial $C$-sector input.
If $t$ has nontrivial $C$-sector content,
then the $B$-sector output is independent
of that $C$-sector content.
The two projections are structurally decoupled.
Source Context
- Registry source:
book-01.jsonlline 115 - Manuscript source:
2nd-edition/book-i-categorical-foundations/02_mainmatter/part13/ch51-diagonal-free-protection.texlines 149-181
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookI.Holomorphy.DiagonalProtection - Name:
Tau.Holomorphy.no_simul_projection_b
Dependencies
- Canonical: I.D03, I.T05, I.D47
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
I.P23no-simultaneous-projectionprop:no-simul-projectionRelease lines
corpus_v3_workingcorpus_v2Relations
Formalized by (1)
Appears in (1)
Downstream uses (computed) (2)
Items in the corpus that reference this one via load-bearing relations. Computed from the full corpus-v3 graph at build time.
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.