Index Tetration

n ^^m = n^(n^(…^n)) (m times): tetration earned by structural recursion on exponentiation. Terminal operation (ladder saturates here).

Index Tetration

Summary

n ^^m = n^(n^(…^n)) (m times): tetration earned by structural recursion on exponentiation. Terminal operation (ladder saturates here).

Statement

%
\label{def:idx-tetration}
For $\underline{a}, \underline{c} \in \tau\text{-Idx}$
with $\underline{a} \geq \underline{2}$,
\textbf{index tetration} is defined by
structural recursion on $c$:
\begin{align*}
    {}^{\underline{0}}\underline{a} &:= \underline{1}, \\
    {}^{\rho(\underline{c})}\underline{a}
    &:= \underline{a}^{({}^{\underline{c}}\underline{a})}.
\end{align*}
That is, ${}^{\underline{c}}\underline{a}$
is a right-associative tower of exponentials:
\[
    {}^{\underline{c}}\underline{a}
    = \underbrace{\underline{a}^{\underline{a}^{\cdot^{\cdot^{\cdot^{\underline{a}}}}}}}_{c \text{ copies of } \underline{a}}.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 27
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch12-exp-tetration.tex lines 110-128

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Arithmetic
• Name: Tau.Denotation.idx_tetration

Dependencies

• Canonical: I.D12, I.D06, I.T02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.