PRP0082canonicalv13-Condition Sufficiency
The three conditions (clopen locality + ω-germ determinacy + defect contractivity) are individually necessary and jointly sufficient for positive regularity. Removing any one permits non-stabilizing ω-germs.
Payload
3-Condition Sufficiency
The three conditions (clopen locality + ω-germ determinacy + defect contractivity) are individually necessary and jointly sufficient for positive regularity. Removing any one permits non-stabilizing ω-germs.
3-Condition Sufficiency
Summary
The three conditions (clopen locality + ω-germ determinacy + defect contractivity) are individually necessary and jointly sufficient for positive regularity. Removing any one permits non-stabilizing ω-germs.
Statement
\label{prop:three-condition-sufficiency}
Let $f$ be $\tau$-admissible fluid data on a clopen cylinder domain $U \subset \tau^3$. Suppose the following three conditions hold:
\begin{enumerate}
\item[\emph{(C1)}] \textbf{Clopen locality.} The domain $U$ is a finite union of clopen cylinders at each primorial depth (Definition~\ref{def:clopen-cylinder-domain}, Ch.~34), and the Boolean cylinder algebra is closed under intersection, union, and complement.
\item[\emph{(C2)}] \textbf{$\omega$-Germ determinacy.} At each primorial level $\operatorname{Prim}(n)$, the Local Hartogs continuation $\operatorname{Ext}_n$ produces a unique extension of the boundary data into the interior of~$U_n$ (Theorem~\ref{thm:hartogs-flow-theorem}(i), Ch.~36). There is no freedom in the evolved data: it is \emph{forced} by the boundary assignment.
\item[\emph{(C3)}] \textbf{Defect-horizon contractivity.} The defect functional $\Delta(f, n)$ (Definition~\ref{def:defect-functional}, Ch.~35) satisfies $\Delta(f, n{+}1) \leq \kappa \cdot \Delta(f, n)$ for all $n$ sufficiently large, with $\kappa < 1$ (Proposition~\ref{prop:defect-contractivity}, Ch.~35).
\end{enumerate}
Then $H_{\mathrm{flow}}(f)$ admits a stabilized $\omega$-germ at every point $x \in U$.
Proof / Justification
No immediate manuscript proof block was extracted in this pilot run.
Source Context
- Registry source:
book-03.jsonlline 99 - Manuscript source:
2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch37-positive-regularity.texlines 56-68
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookIII.Physics.PositiveRegularity - Name:
stability_criterion_check
Dependencies
- Canonical: III.T25
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
III.P153-condition-sufficiencyprop:three-condition-sufficiencyRelease lines
corpus_v3_workingcorpus_v2Relations
Formalized by (1)
Appears in (1)
Downstream uses (computed) (2)
Items in the corpus that reference this one via load-bearing relations. Computed from the full corpus-v3 graph at build time.
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.