Index Exponentiation

n^m = n * n * … * n (m times): exponentiation earned by structural recursion on multiplication.

Index Exponentiation

Summary

n^m = n * n * … * n (m times): exponentiation earned by structural recursion on multiplication.

Statement

%
\label{def:idx-exp}
For $\underline{n}, \underline{m} \in \tau\text{-Idx}$,
\textbf{index exponentiation} is defined by
structural recursion on $m$:
\begin{align*}
    \underline{n}^{\underline{0}} &:= \underline{1}, \\
    \underline{n}^{\rho(\underline{m})}
    &:= \underline{n}^{\underline{m}} \times \underline{n}.
\end{align*}
That is, $\underline{n}^{\underline{m}}
= \underbrace{\underline{n} \times \cdots \times \underline{n}}_{m \text{ times}}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D11, I.D06

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.