unique_infinity (theorem)

/-- [I.T36] Unique Infinity Object: omega is the ONLY infinity object in Category tau. Proof: Let x be any infinity object. Since rho(x) = x and x is unreachable from orbit rays, x must have seed = omega (by K6 object closure, the only objects not in orbit rays have seed omega). Then x = (omega, d) for some d. Since rho(omega, d) = (omega, d) (K2), ANY omega-seeded object is rho-fixed. But the uniqueness is stronger: all (omega, d) are rho-equivalent (they all satisfy rho(x) = x), so up to rho-equivalence there is exactly one infinity object. -/