Tower Atom

T(a,b,c) = (a^^c)^b for prime a, b >= 1, c >= 1. The nesting ((a^^c)^b) is forced by diagonal discipline; only binding from which all three parameters are uniquely recoverable.

Tower Atom

Summary

T(a,b,c) = (a^^c)^b for prime a, b >= 1, c >= 1. The nesting ((a^^c)^b) is forced by diagonal discipline; only binding from which all three parameters are uniquely recoverable.

Statement

%
\label{def:tower-atom}
A \textbf{tower atom} is a triple
$(\underline{a}, \underline{b}, \underline{c})$
with $\underline{a} \in \mathbb{P}_\tau$,
$\underline{b} \geq \underline{1}$,
$\underline{c} \geq \underline{1}$,
whose \textbf{value} is
\[
    \boxed{T(\underline{a}, \underline{b}, \underline{c})
    \;=\;
    (\underline{a} \uparrow\uparrow \underline{c})^{\underline{b}}.}
\]
Here $\underline{a} \uparrow\uparrow \underline{c}$
is the internal tetration of Chapter~\ref{ch:exp-tetration},
and the exponentiation is internal
(Chapter~\ref{ch:swap-add-mul}).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 54
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch17-tower-atoms-peel.tex lines 40-58

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.TowerAtoms
• Name: Tau.Coordinates.tower_atom

Dependencies

• Canonical: I.D19b, I.D12, I.D13

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.