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.

Omega Unique Fixed Seed

Summary

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.

Statement

%
\label{prop:omega-unique-fixed}
An object $x \in \Obj(\tau)$ satisfies $\rho(x) = x$
if and only if the seed of $x$ is $\omega$.
That is, $\omega$ is the \emph{unique fixed seed} of~$\rho$:
no non-$\omega$ generator produces a fixed point,
regardless of depth.

Proof / Justification

If $x = \langle\omega, d\rangle$ for any depth~$d$,
then $\rho(x) = \langle\omega, d\rangle = x$ by $\KAxiom{2}$.
Conversely, if $x = \langle g, d\rangle$ for a non-$\omega$ generator
$g \in \{\alpha, \pi, \gamma, \eta\}$,
then $\rho(x) = \langle g, d+1\rangle \neq \langle g, d\rangle = x$
(since $d + 1 \neq d$).

Source Context

• Registry source: book-01.jsonl line 95
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part01/ch02-rho-omega.tex lines 113-120

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Structural
• Name: Tau.Denotation.omega_unique_fixed_seed

Dependencies

• Canonical: I.D02, I.K2, I.K3, I.K4

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.