Registry · Definition I.D16a established formalized

I.D16a — 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.

Book I Part 3 Ch. 15

Dependency Graph

Depends on (3)

I.D07 I.T01 I.K1

Depended on by (1)

I.P07

Lean Formalization

Module: TauLib.BookI.Denotation.Order

Symbol: Tau.Denotation.denotational_order