NF Address Encoding

Every object x in Obj(tau) has a normal form X = ((A^^C)^B)*D via greedy peel-off of tetration, exponentiation, multiplication, and radial index.

NF Address Encoding

Summary

Every object x in Obj(tau) has a normal form X = ((A^^C)^B)*D via greedy peel-off of tetration, exponentiation, multiplication, and radial index.

Statement

%
\label{def:nf-encoding}
The \textbf{normal-form address encoding}
of $X \in \tau\text{-Idx}$ is the expression
\[
    \boxed{X
    \;=\;
    ((\underline{A} \uparrow\uparrow \underline{C})^{\underline{B}})
    \cdot \underline{D}}
\]
where $(\underline{A}, \underline{B}, \underline{C}, \underline{D})
= \Phi(X)$ is the output of the greedy peel-off algorithm
(Definition~\ref{def:greedy-peel}).
For $X = \underline{1}$, the NF is the trivial encoding
$\underline{1} = \underline{1} \cdot \underline{1}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 32
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch18-nf-encoding.tex lines 40-56

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.NormalForm
• Name: Tau.Coordinates.spine

Dependencies

• Canonical: I.D19c, I.D19d, I.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.