Tau-Identity Theorem

THE CROWN JEWEL: if two tau-holomorphic functions agree at stage d0 for all inputs, they agree at all stages <= d0. Hallmark of holomorphic rigidity. Proof uses tower coherence for vertical propagation (not classical sideways analytic continuation).

Tau-Identity Theorem

Summary

THE CROWN JEWEL: if two tau-holomorphic functions agree at stage d0 for all inputs, they agree at all stages <= d0. Hallmark of holomorphic rigidity. Proof uses tower coherence for vertical propagation (not classical sideways analytic continuation).

Statement

%
\label{thm:tau-identity}
Let $T, S \in \mathrm{HolFun}$
(Definition~\ref{def:holfun}, I.D47).
If there exists $d_0 \geq 1$ such that
$T$ and $S$ agree at depth $d_0$
(Definition~\ref{def:tail-agreement}),
then $T = S$ as functions on $\mathrm{OmegaTail}$
(Definition~\ref{def:omega-tail}, I.D25).
\[
    \boxed{%
    \exists\, d_0 \geq 1:\;
    T \sim_{d_0} S
    \;\;\Longrightarrow\;\;
    T = S.}
\]

Proof / Justification

By Lemma~\ref{lem:tail-agreement-propagation},
$T$ and $S$ agree at every depth $d \geq d_0$.
But agreement at all depths means:
for every omega-tail $t$
and every primorial stage $k$,
the $k$-th components
of $T(t)$ and $S(t)$ coincide.

An omega-tail \emph{is} its sequence of components ---
it is a compatible tower
$(x_1, x_2, x_3, \ldots)$
with $x_k \in \mathbb{Z}/M_k\mathbb{Z}$
(Definition~\ref{def:omega-tail}).
If $\bigl(T(t)\bigr)_k = \bigl(S(t)\bigr)_k$
for all $k \geq 1$,
then $T(t)$ and $S(t)$ are the same omega-tail.
Therefore $T(t) = S(t)$ for all $t$,
i.e., $T = S$.

Source Context

• Registry source: book-01.jsonl line 120
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part13/ch52-identity-theorem.tex lines 325-342

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.IdentityTheorem
• Name: Tau.Holomorphy.tau_identity_nat

Dependencies

• Canonical: I.D46, I.D47, I.T18, I.L07

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.