TTM τ-Nativity

A TTM program IS a τ-address operating ON τ-addresses producing τ-addresses. Program = data type. Self-referential identity makes the TTM an E₂ object: code contains its own decoder.

TTM τ-Nativity

Summary

A TTM program IS a τ-address operating ON τ-addresses producing τ-addresses. Program = data type. Self-referential identity makes the TTM an E₂ object: code contains its own decoder.

Statement

\label{thm:ttm-tau-nativity}
Let $M$ be a $\tau$-Tower Machine.
Then:
\begin{enumerate}
    \item The program $M$ has a canonical NF address
          $\operatorname{addr}(M) \in \hat{\mathbb{Z}}_{\tau}$.
    \item The instruction set $\Sigma$ has a canonical NF address
          $\operatorname{addr}(\Sigma) \in \hat{\mathbb{Z}}_{\tau}$.
    \item For every input tuple
          $(a_1, \ldots, a_{b_0}) \in \hat{\mathbb{Z}}_{\tau}^{\,b_0}$,
          if $M$ halts with output~$a'$,
          then $a' \in \hat{\mathbb{Z}}_{\tau}$.
    \item The triple
          $(\operatorname{addr}(M),\, \operatorname{addr}(\Sigma),\, a')$
          satisfies $\Elayer{2}$ operational closure
          (Definition~\ref{def:operational-closure}):
          the decoder applied to the code
          produces another code of the same type.
\end{enumerate}
In particular, the Code $\to$ Execution $\to$ Code
cycle of $\Elayer{2}$ is realised within
the NF tower of Category~$\tau$.

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 146
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part09/ch55-the-tau-tower-machine.tex lines 313-336

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Computation.TowerMachine
• Name: ttm_nativity_check

Dependencies

• Canonical: III.D51, III.D49

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.