rho Injectivity Per Orbit

rho is injective on each orbit ray (from K4 no-jump/cover property).

rho Injectivity Per Orbit

Summary

rho is injective on each orbit ray (from K4 no-jump/cover property).

Statement

%
\label{prop:rho-injective}
For each generator $g \in \{\alpha, \pi, \gamma, \eta\}$
and all $n, m \geq 0$:
\[
    \rho\bigl(\rho^n(g)\bigr) = \rho\bigl(\rho^m(g)\bigr)
    \quad\Longrightarrow\quad
    n = m.
\]
That is, $\rho$ is injective on each orbit ray~$O_g$.

Proof / Justification

Suppose $\rho(\rho^n(g)) = \rho(\rho^m(g))$.
By $\KAxiom{4}$:
\[
    \rho(\rho^n(g)) = \rho^{n+1}(g),
    \qquad
    \rho(\rho^m(g)) = \rho^{m+1}(g).
\]
So $\rho^{n+1}(g) = \rho^{m+1}(g)$.
The object $\rho^k(g)$ is characterized within $O_g$
by its depth~$k$ (the number of $\rho$-applications from the seed).
Since $\KAxiom{4}$ ensures that each depth is occupied by exactly one element,
$n+1 = m+1$ and hence $n = m$.

Source Context

• Registry source: book-01.jsonl line 13
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part01/ch03-generation-cover.tex lines 279-290

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Kernel.Axioms
• Name: Tau.Kernel.rho_injective

Dependencies

• Canonical: I.K4, I.D02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.