Central Theorem

The Central Theorem: canonical isomorphism O(tau^3) = A_spec(L), identifying holomorphic functions on the fibered product with spectral characters on the lemniscate boundary. Functorial, bipolar-compatible, tower-graded, iota_tau-calibrated.

Central Theorem

Summary

The Central Theorem: canonical isomorphism O(tau^3) = A_spec(L), identifying holomorphic functions on the fibered product with spectral characters on the lemniscate boundary. Functorial, bipolar-compatible, tower-graded, iota_tau-calibrated.

Statement

%
\label{thm:central-theorem}
%   II.T27, II.T33, II.T35, II.T36, II.T37, II.T38, II.T39,
%   II.D35, II.D59, II.P13, II.L07, II.L12, II.L13, II.L14
There is a canonical isomorphism of calibrated
split-complex algebras:
\begin{equation}
\label{eq:ch51-central-theorem}
    \boxed{\;
    \mathcal{O}(\tau^3)
    \;\cong\;
    A_{\mathrm{spec}}(\mathbb{L})
    \;}
\end{equation}
The isomorphism is:
\begin{enumerate}
    \item[\textup{(a)}] \textbf{canonical}:
          no choices are involved in its construction;
    \item[\textup{(b)}] \textbf{functorial}:
          it commutes with morphisms of $\tau$-spaces;
    \item[\textup{(c)}] \textbf{compatible with the bipolar decomposition}:
          it sends $e_+ \cdot f_+$ to $e_+ \cdot \chi_+$
          and $e_- \cdot f_-$ to $e_- \cdot \chi_-$;
    \item[\textup{(d)}] \textbf{compatible with the tower grading}:
          it respects the stage-by-stage structure
          of the primorial tower;
    \item[\textup{(e)}] \textbf{compatible with $\iota_\tau$-calibration}:
          the numerical values of spectral coefficients
          in $A_{\mathrm{spec}}(\mathbb{L})$
          are the numerical values of
          the corresponding holomorphic function
          in $\mathcal{O}(\tau^3)$.
\end{enumerate}

Proof / Justification

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

Source Context

• Registry source: book-02.jsonl line 148
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part09/ch51-central-theorem.tex lines 377-411

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.CentralTheorem.CentralTheorem
• Name: Tau.BookII.CentralTheorem.central_theorem_check

Dependencies

• Canonical: I.T05, I.T31, I.D18, I.D19, I.D21, I.T41, II.T27, II.T33, II.T35, II.T36, II.T37, II.T38, II.T39, II.D35, II.D59, II.P13, II.L07, II.L12, II.L13, II.L14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.