Index Addition

n + m = rho^m(n): addition on tau-Idx earned by iterating rho m times starting from n. No Peano axioms imported.

Index Addition

Summary

n + m = rho^m(n): addition on tau-Idx earned by iterating rho m times starting from n. No Peano axioms imported.

Statement

%
\label{def:idx-add}
For $\underline{n}, \underline{m} \in \tau\text{-Idx}$,
\textbf{index addition} is defined by
\[
    \boxed{\underline{n} + \underline{m}
    := \rho^m(\underline{n}) = \rho^m(\rho^n(\alpha))
    = \rho^{n+m}(\alpha) = \underline{n+m}.}
\]
Equivalently, by structural recursion on $m$:
\begin{align*}
    \underline{n} + \underline{0} &:= \underline{n}, \\
    \underline{n} + \rho(\underline{m})
    &:= \rho(\underline{n} + \underline{m}).
\end{align*}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 24
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch11-swap-add-mul.tex lines 94-110

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D07, I.D06, I.D02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.