Tau-Holomorphic Function

A tau-holomorphic function (HolFun) = D-holomorphic + tower-coherent germ transformer. The D-holomorphic condition is structural (SectorFun); tower coherence is the additional rigidity constraint.

Tau-Holomorphic Function

Summary

A tau-holomorphic function (HolFun) = D-holomorphic + tower-coherent germ transformer. The D-holomorphic condition is structural (SectorFun); tower coherence is the additional rigidity constraint.

Statement

%
\label{def:holfun}
A \textbf{$\tau$-holomorphic function} is an $\omega$-germ transformer
$T : \mathrm{OmegaTail} \to \hat{\mathbb{Z}}_\tau[j]$
(Definition~\ref{def:omega-germ-transformer}, I.D45)
that satisfies both:
\begin{enumerate}
    \item \textbf{D-holomorphy in sector coordinates}
          (Chapter~\ref{ch:d-holomorphy}):
          $T$ respects the idempotent decomposition,
          acting as independent sector functions
          $T_+ = e_+ \circ T$ and $T_- = e_- \circ T$
          on the $B$-sector and $C$-sector respectively.
    \item \textbf{Tower coherence}
          (Definition~\ref{def:tower-coherence}, I.D46):
          for all $k \leq \ell$,
          $\pi_{\ell \to k}(T_\ell(t))
          = T_k(\pi_{\ell \to k}(t))$.
\end{enumerate}
The type of all $\tau$-holomorphic functions is denoted:
\[
    \boxed{%
    \mathrm{HolFun}
    \;:=\;
    \bigl\{
        T : \mathrm{OmegaTail} \to \hat{\mathbb{Z}}_\tau[j]
        \;\big|\;
        T \text{ is D-holomorphic and tower-coherent}
    \bigr\}.}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 112
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part13/ch50-tau-holomorphic.tex lines 283-314

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.TauHolomorphic
• Name: Tau.Holomorphy.HolFun

Dependencies

• Canonical: I.D45, I.D46

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.