Bipolar Idempotents Interior

Bipolar Idempotents Interior

Bipolar Idempotents Interior

Summary

Bipolar Idempotents Interior

Statement

%
\label{def:bipolar-idempotents-interior}
The \textbf{bipolar idempotents} are
\[
    \boxed{%
    e_+
    \;:=\;
    \frac{1 + \jj}{2},
    \qquad\qquad
    e_-
    \;:=\;
    \frac{1 - \jj}{2}.}
\]
These satisfy:
\begin{enumerate}
    \item[\textup{(i)}]
          $e_+^2 = e_+$, \quad $e_-^2 = e_-$
          \quad (idempotent),
    \item[\textup{(ii)}]
          $e_+ \cdot e_- = 0$
          \quad (orthogonal),
    \item[\textup{(iii)}]
          $e_+ + e_- = 1$
          \quad (complete),
    \item[\textup{(iv)}]
          $\jj = e_+ - e_-$
          \quad (recovery of~$\jj$).
\end{enumerate}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 73
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part05/ch27-j-replaces-i.tex lines 260-289

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Transcendentals.JReplacesI
• Name: j_exponential

Dependencies

• Canonical: II.D32, I.D20

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.