Stages from Limit

The interior is determined by the boundary: two tower-coherent functions with the same boundary data (agreement at a reference depth) have the same interior values at all coarser stages.

Stages from Limit

Summary

The interior is determined by the boundary: two tower-coherent functions with the same boundary data (agreement at a reference depth) have the same interior values at all coarser stages.

Statement

%
\label{cor:interior-from-boundary}
Every finite-stage value on $\tau^3 = \tau^1 \times_f T^2$
is uniquely determined by omega-tail data on~$\mathbb{L}$.
Every point of $\tau^3$
is an earned stage-determined point:
\[
    \boxed{%
    \mathrm{Int}_{\mathrm{earned}}(\tau^3)
    \;=\;
    \tau^3.}
\]

Proof / Justification

Let $p \in \tau^3$ be arbitrary.
By Global Hartogs
(Theorem~\ref{thm:global-hartogs}, I.T06),
every $T \in \mathrm{Hol}(\mathbb{L})$
extends uniquely from partial lemniscate data
to all of~$\mathbb{L}$.
Tower coherence
(Definition~\ref{def:tower-coherence}, I.D46)
ensures that the holomorphic data on $\mathbb{L}$
propagates along the primorial tower
to determine values at $p$:
the CRT reconstruction at each primorial stage
propagates limit data to finite stages.
By the $\tau$-Identity Theorem
(Theorem~\ref{thm:tau-identity}, I.T21),
this extension is unique.
Therefore $p \in \mathrm{Int}_{\mathrm{earned}}(\tau^3)$.

Source Context

• Registry source: book-01.jsonl line 156
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part16/ch63-boundary-interior-passage.tex lines 109-122

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.BoundaryInterior
• Name: Tau.Holomorphy.interior_from_boundary

Dependencies

• Canonical: I.T31, I.D68

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.