Tau-Regularity

A point p is tau-regular for f if the omega-germ sequence stabilizes at a finite primorial stage. A constructive, positive criterion: existence of stabilization, not absence of pathology.

Tau-Regularity

Summary

A point p is tau-regular for f if the omega-germ sequence stabilizes at a finite primorial stage. A constructive, positive criterion: existence of stabilization, not absence of pathology.

Statement

%
\label{def:tau-regularity}
Let $f : \tau^3 \to H_\tau$ be $\tau$-holomorphic
(equivalently, by II.T33:
idempotent-supported via the decomposition
$f = e_+ \cdot f_+ + e_- \cdot f_-$
of the Idempotent Decomposition Lemma, II.L07).
A point $p \in \tau^3$ is
\textbf{$\tau$-regular for $f$}
if there exists a primorial stage $N \geq 1$
such that the $\omega$-germ sequence of $f$ at $p$
stabilizes at stage $N$:
\[
    \boxed{%
    p \text{ is $\tau$-regular for } f
    \quad:\Longleftrightarrow\quad
    \exists\, N \geq 1,\;
    \forall\, k \geq N:\;
    \rho_{k,N}\bigl(G_f\bigr)
    = G_f \big|_{C_N(p)}.}
\]
The minimal such $N$ is called the
\textbf{regularity depth} of $f$ at $p$,
denoted $\mathrm{rd}_f(p)$.

A function $f$ is \textbf{everywhere $\tau$-regular}
if every point $p \in \tau^3$
is $\tau$-regular for $f$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 115
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part07/ch39-regularity-positive.tex lines 286-315

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Regularity.PositiveRegularity
• Name: is_regular

Dependencies

• Canonical: II.D37, II.D10, II.L07, II.T33, I.T31

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.