PRP0021canonicalv1Ultra Dist Self
d(t, t) = 0 for every omega-tail t. Identity of indiscernibles for the primorial divergence depth.
Payload
Ultra Dist Self
d(t, t) = 0 for every omega-tail t. Identity of indiscernibles for the primorial divergence depth.
Ultra Dist Self
Summary
d(t, t) = 0 for every omega-tail t. Identity of indiscernibles for the primorial divergence depth.
Statement
%
\label{prop:ultra-dist-self}
For every omega-tail $t$: $d(t, t) = 0$.
Proof / Justification
By definition, $t$ agrees with itself at every stage,
so $t \sim t$ and hence $d(t, t) = 0$.
Source Context
- Registry source:
book-01.jsonlline 105 - Manuscript source:
2nd-edition/book-i-categorical-foundations/02_mainmatter/part07/ch28-omega-germs.texlines 293-296
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookI.Denotation.Structural - Name:
Tau.Denotation.ultra_dist_self
Dependencies
- Canonical: I.D25
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
I.P20ultra-dist-selfprop:ultra-dist-selfRelease lines
corpus_v3_workingcorpus_v2Relations
Appears in (1)
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.