Denotational Order

The canonical linear order on Obj(tau): orbit-first (by K1 generator order), then depth-within-orbit. Extends K1 from generators to all objects.

Denotational Order

Summary

The canonical linear order on Obj(tau): orbit-first (by K1 generator order), then depth-within-orbit. Extends K1 from generators to all objects.

Statement

%
\label{def:denotational-order}
The \textbf{denotational order} $<_\tau$ on $\Obj(\tau)$
is defined as follows.
For $x, y \in \Obj(\tau)$:
\begin{enumerate}
    \item If $x \in O_g$ and $y \in O_h$ with $g \neq h$
          (including $g$ or $h$ equal to $\omega$),
          then $x <_\tau y$ iff $g < h$
          in the generator order $\KAxiom{1}$.
          (All of $O_\alpha$ precedes all of $O_\pi$,
          which precedes all of $O_\gamma$, etc.)

    \item If $x, y \in O_g$ for the same generator $g$
          (or both are $\omega$),
          then $x <_\tau y$ iff
          $\mathrm{depth}(x) < \mathrm{depth}(y)$.
\end{enumerate}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 49
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch15-denotational-order.tex lines 44-63

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Order
• Name: Tau.Denotation.denotational_order

Dependencies

• Canonical: I.D07, I.T01, I.K1

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.