Tau-Admissible Point

Tau-Admissible Point

Tau-Admissible Point

Summary

Tau-Admissible Point

Statement

%
\label{def:tau-admissible-point}
A \textbf{$\tau$-admissible point} is a quadruple
$(A, B, C, D) \in \tau\text{-Idx}^4$
satisfying all five constraints of the
constraint lattice (Definition~\ref{def:constraint-lattice}).
Write
\[
    \boxed{\tau^3_{\mathrm{fin}}
    \;:=\;
    \bigl\{\, (A, B, C, D) \in \tau\text{-Idx}^4
    \;\big|\;
    (A, B, C, D) \text{ is } \tau\text{-admissible} \,\bigr\}}
\]
for the set of all $\tau$-admissible points
with finite coordinates.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 5
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part01/ch04-tau-admissible-points.tex lines 205-222

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Interior.TauAdmissible
• Name: Tau.BookII.Interior.TauAdmissiblePoint

Dependencies

• Canonical: I.D17, I.T04

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.