Registry · Proposition I.P09 established formalized

I.P09 — 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).

Book I Part 4 Ch. 20

Dependency Graph

Depends on (1)

I.D24

Lean Formalization

Module: TauLib.BookI.Coordinates.ABCD

Symbol: Tau.Coordinates.metric_inequality_check