tau-Idx (Earned Natural Numbers)

tau-Idx := O_alpha = {alpha, rho(alpha), rho^2(alpha), …}. The alpha-orbit IS the internal natural numbers (N is not imported but earned).

tau-Idx (Earned Natural Numbers)

Summary

tau-Idx := O_alpha = {alpha, rho(alpha), rho^2(alpha), …}. The alpha-orbit IS the internal natural numbers (N is not imported but earned).

Statement

%
\label{def:tau-idx}
The \textbf{internal natural numbers} of Category~$\tau$
are defined as the alpha-orbit:
\[
    \boxed{\tau\text{-Idx} := O_\alpha
    = \{\alpha, \rho(\alpha), \rho^2(\alpha), \ldots\}.}
\]
We write $\underline{n}$ for $\rho^n(\alpha) \in \tau\text{-Idx}$,
so that $\underline{0} = \alpha$, $\underline{1} = \rho(\alpha)$,
$\underline{2} = \rho^2(\alpha)$, etc.
The successor operation on $\tau$-Idx is $\rho$ itself:
$S(\underline{n}) = \rho(\underline{n}) = \underline{n+1}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 21
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch10-tau-idx.tex lines 54-68

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.TauIdx
• Name: Tau.Denotation.TauIdx

Dependencies

• Canonical: I.D05, I.T01, I.P03

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.