Address DAG

Full quadtree (recurse on all 4 coordinates by index) globally deduplicated by index identity. Diamond-shaped finite DAG: branching out from root, reconverging via shared indices, terminating at alpha_1.

Address DAG

Summary

Full quadtree (recurse on all 4 coordinates by index) globally deduplicated by index identity. Diamond-shaped finite DAG: branching out from root, reconverging via shared indices, terminating at alpha_1.

Statement

%
\label{def:address-dag}
The \textbf{Address DAG} of $x \in \tau\text{-Idx}$
is the finite directed acyclic graph
$\mathrm{DAG}(x) = (V, E)$ where:
\begin{itemize}
    \item $V$ is the set of all indices reachable
          from $x$ by iterating $\mathrm{Ch}$:
          the transitive closure of the children relation.
    \item $E = \{(u, v) : v \in \mathrm{Ch}(u),\;
          u \in V\}$.
\end{itemize}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 62
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch20-dimension-fibration.tex lines 402-415

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.ABCD
• Name: Tau.Coordinates.dag_indices

Dependencies

• Canonical: I.D23, I.D17

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.