Metric Inequality

ell_spine(x) <= ell_DAG(x) <= ell_occ(x). Three canonical complexity metrics: spine length (radial depth), DAG size (memoized work), occurrence size (naive work).

Metric Inequality

Summary

ell_spine(x) <= ell_DAG(x) <= ell_occ(x). Three canonical complexity metrics: spine length (radial depth), DAG size (memoized work), occurrence size (naive work).

Statement

%
\label{prop:metric-inequality}
For every $x \in \tau\text{-Idx}$:
\[
    \boxed{\ell_{\mathrm{spine}}(x)
    \;\leq\;
    \ell_{\mathrm{DAG}}(x)
    \;\leq\;
    \ell_{\mathrm{occ}}(x).}
\]

Proof / Justification

The spine visits only the $D$-children,
which form a subpath of the DAG.
So $\ell_{\mathrm{spine}} \leq \ell_{\mathrm{DAG}}$.
The DAG has at most as many nodes
as the quadtree has occurrences,
since the DAG identifies repeated nodes.
So $\ell_{\mathrm{DAG}} \leq \ell_{\mathrm{occ}}$.

The first inequality is strict
whenever $x$ has nontrivial index children
(i.e., when some coordinate is not $\alpha_1$).
The second is strict whenever any index
appears more than once in the full quadtree.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D24

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.