LEM0019canonicalv1Polarity Symmetry
The j-involution interchanges bipolar sectors: sigma_j(G_+) = G_- and sigma_j(G_-) = G_+, so one sector determines the full transformer.
Payload
Polarity Symmetry
The j-involution interchanges bipolar sectors: sigma_j(G_+) = G_- and sigma_j(G_-) = G_+, so one sector determines the full transformer.
Polarity Symmetry
Summary
The j-involution interchanges bipolar sectors: sigma_j(G_+) = G_- and sigma_j(G_-) = G_+, so one sector determines the full transformer.
Statement
%
\label{lem:polarity-symmetry}
Let $G = G_+ + G_-$
be the Branch Factorization
of an $\omega$-germ transformer \textup{(II.L08)}.
Then the $\jj$-involution interchanges the two sectors:
\begin{enumerate}
\item[\textup{(i)}]
$\sigma_\jj(G_+) = G_-$
and $\sigma_\jj(G_-) = G_+$.
\item[\textup{(ii)}]
The spectral data of $G_+$ at a $\gamma$-orbit prime~$p$
determines the spectral data of $G_-$
at the corresponding $\eta$-orbit prime,
and conversely.
\item[\textup{(iii)}]
Knowing $G_+$ alone
determines $G_-$ \textup{(}and hence $G$\textup{)}
via $G_- = \sigma_\jj(G_+)$
and $G = G_+ + \sigma_\jj(G_+)$.
\end{enumerate}
Proof / Justification
\emph{(i) Channel interchange.}
By the channel-swapping property
of $\sigma_\jj$
(Remark~\ref{rem:ch38-sigma-properties}):
\begin{align*}
\sigma_\jj(G_+)
&= \sigma_\jj(e_+ \cdot G)
= \sigma_\jj(e_+) \cdot \sigma_\jj(G)
= e_- \cdot \sigma_\jj(G).
\end{align*}
We need $\sigma_\jj(G) = G$.
This holds because
$G$ is a $\tau$-holomorphic transformer,
and the $\jj$-involution
is an automorphism of $H_\tau$
that preserves the holomorphic structure.
Concretely:
the Mutual Determination Theorem (II.T27,
Chapter~\ref{ch:mutual-determination})
identifies a holomorphic datum
with a boundary character
$\varphi \colon R_\tau \to H_\tau$.
The boundary ring $R_\tau$ (I.D19, Book~I)
is invariant under $\sigma_\jj$
(it is the profinite completion
of cyclic groups,
which are stable under conjugation).
The holomorphic condition is symmetric
in the B and C channels
(the five-way equivalence of II.T27
treats both channels identically).
Hence $\sigma_\jj$ maps holomorphic transformers
to holomorphic transformers,
and since $G$ is the \emph{total} transformer,
$\sigma_\jj(G) = G$ as a transformation
on the germ algebra.
Therefore:
$\sigma_\jj(G_+) = e_- \cdot \sigma_\jj(G) = e_- \cdot G = G_-$.
Similarly, $\sigma_\jj(G_-) = G_+$.
\emph{(ii) Spectral correspondence.}
By Prime-Split Support (II.L09),
$G_+$ has spectral support in
the $\gamma$-orbit primes
and $G_-$ has spectral support in
the $\eta$-orbit primes.
The $\jj$-involution maps
$\chi_+$ to $\chi_-$ and $\chi_-$ to $\chi_+$
(I.D22--I.D23, Book~I:
$\chi_\pm = e_\pm \cdot \chi$
for any character~$\chi$,
and $\sigma_\jj$ swaps $e_\pm$).
Hence the spectral coefficient of $G_+$
at a $\gamma$-orbit prime~$p$
equals the spectral coefficient of $G_-$
at the partner prime in the $\eta$-orbit.
The correspondence is canonical
(determined by Prime Polarity, I.T05).
\emph{(iii) One channel determines both.}
Since $G_- = \sigma_\jj(G_+)$ by~(i),
and $G = G_+ + G_-$ by Branch Factorization,
we have $G = G_+ + \sigma_\jj(G_+)$.
Knowledge of $G_+$ alone
determines $G$ completely.
Symmetrically, $G = \sigma_\jj(G_-) + G_-$.
Source Context
- Registry source:
book-02.jsonlline 113 - Manuscript source:
2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part07/ch38-three-lemma-chain.texlines 641-663
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookII.Regularity.ThreeLemmaChain - Name:
polarity_symmetry_check
Dependencies
- Canonical: I.T05, I.D21, I.D22, I.D23, II.L08, II.L09
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
II.L10polarity-symmetrylem:polarity-symmetryRelease 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.