Registry · Proposition I.P14 established formalized

I.P14 — Omega Unique Fixed Seed

rho(x) = x iff seed(x) = omega. Omega is the unique fixed seed of rho among ALL objects (not just generators). Non-omega seeds always advance depth by 1.

Book I Part 1 Ch. 2

Dependency Graph

Depends on (4)

I.D02 I.K2 I.K3 I.K4

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.omega_unique_fixed_seed