Registry · Proposition I.P20 established formalized

I.P20 — Ultra Dist Self

d(t, t) = 0 for every omega-tail t. Identity of indiscernibles for the primorial divergence depth.

Book I Part 7 Ch. 28

Dependency Graph

Depends on (1)

I.D25

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.ultra_dist_self