Positive Regularity Theorem

For τ-admissible initial data, every ω-germ stabilizes under H_flow. 3-condition proof: (i) clopen locality, (ii) ω-germ determinacy via Local Hartogs, (iii) defect-horizon contractivity. Structural mechanism, not a PDE estimate.

Positive Regularity Theorem

Summary

For τ-admissible initial data, every ω-germ stabilizes under H_flow. 3-condition proof: (i) clopen locality, (ii) ω-germ determinacy via Local Hartogs, (iii) defect-horizon contractivity. Structural mechanism, not a PDE estimate.

Statement

\label{thm:positive-regularity}
For every $\tau$-admissible fluid datum $f$ (Definition~\ref{def:tau-admissible-fluid-data}, Ch.~34) on every clopen cylinder domain $U \subset \tau^3$, the Hartogs flow operator $H_{\mathrm{flow}}$ (Definition~\ref{def:hartogs-flow-operator}, Ch.~36) produces a stabilized $\omega$-germ at every point of $U$:
\begin{equation}
\forall\, x \in U, \quad \exists\, N_x \in \mathbb{N} : \quad
\forall\, n \geq N_x, \quad
H_{\mathrm{flow}}(f)\big|_{\operatorname{Prim}(n)}(x)
= \omega\text{-}\mathrm{germ}(f, x).
\label{eq:ch37-positive-regularity}
\end{equation}
Regularity is \emph{positive}: it is the existence of a stabilized germ, not the absence of a singularity.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 97
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch37-positive-regularity.tex lines 87-99

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Physics.PositiveRegularity
• Name: positive_regularity_check

Dependencies

• Canonical: III.D36, III.D39, III.D40, III.T24, III.P14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.