Uniqueness of Category Tau

The moduli space of tau^3-structures is a single point: any two realizations of axioms K0-K5 are canonically isomorphic, preserving the fibered product structure, ABCD chart, holomorphic structure O(tau^3) = A_spec(L), and calibration constants pi, e, j, iota_tau.

Uniqueness of Category Tau

Summary

The moduli space of tau^3-structures is a single point: any two realizations of axioms K0-K5 are canonically isomorphic, preserving the fibered product structure, ABCD chart, holomorphic structure O(tau^3) = A_spec(L), and calibration constants pi, e, j, iota_tau.

Statement

%
\label{cor:uniqueness}
The moduli space of $\tau^3$-structures is a single point:
\[
    \boxed{\mathcal{M}_{\tau^3} \;=\; \{\mathrm{pt}\}.}
\]
There are no free parameters.
Any two realizations of the axioms \textup{K0--K5}
are canonically isomorphic,
and the isomorphism preserves:
\begin{enumerate}
    \item[\textup{(a)}]
          the fibered product structure
          $\tau^3 = \tau^1 \times_f T^2$;
    \item[\textup{(b)}]
          the ABCD chart~$\Phi$;
    \item[\textup{(c)}]
          the holomorphic structure
          $\mathcal{O}(\tau^3) \cong
          A_{\mathrm{spec}}(\Lemniscate)$;
    \item[\textup{(d)}]
          the calibration constants
          $\pi, e, \jj, \iota_\tau$.
\end{enumerate}

Proof / Justification

By the Categoricity Theorem
(Theorem~\ref{thm:categoricity}, II.T42),
every realization $(M, \Phi_M)$
satisfying K0--K5 is canonically isomorphic to~$\tau^3$.
The moduli space therefore contains
exactly one isomorphism class.
The preservation of structure (a)--(d)
was established in the proof
of Theorem~\ref{thm:categoricity}.

Source Context

• Registry source: book-02.jsonl line 153
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part09/ch52-liouville-categoricity.tex lines 740-765

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.CentralTheorem.Categoricity
• Name: Tau.BookII.CentralTheorem.uniqueness_check

Dependencies

• Canonical: II.T42, II.D61

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.