Earned Stage-Determined Point

An earned interior point: a value obtained by extending boundary data via Hartogs extension. Carries a tower-coherent StageFun and produces interior values that are self-consistent (reduced).

Earned Stage-Determined Point

Summary

An earned interior point: a value obtained by extending boundary data via Hartogs extension. Carries a tower-coherent StageFun and produces interior values that are self-consistent (reduced).

Statement

%
\label{def:earned-interior-point}
A point $p \in \tau^3$ is an
\textbf{earned stage-determined point}
(or \emph{earned interior point}
in the geometric language of Book~II)
if its $\tau$-holomorphic data
is completely determined by omega-tail data on~$\mathbb{L}$:
\[
    \boxed{%
    p \in \mathrm{Int}_{\mathrm{earned}}(\tau^3)
    \quad:\Longleftrightarrow\quad
    \forall\, T \in \mathrm{Hol}(\mathbb{L}),\;
    T(p) \text{ is determined by }
    T|_{\mathbb{L}}.}
\]
Here $\mathrm{Hol}(\mathbb{L})$
is the space of $\tau$-holomorphic functions
(Definition~\ref{def:hol-L}, I.D49)
and the determination is via
Global Hartogs extension
(Theorem~\ref{thm:global-hartogs}, I.T06).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.T31, I.D47

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.