External extension tracking

The accepted ledger is also an external partially ordered graph of named theory presentations. A node is one exact rule signature. An edge must say whether it adds, removes, or replaces rules, interprets one signature in another, or proves a conservative translation; it carries the local theorem label or exact imported theorem that justifies that relationship. Shared surface syntax and successful artifact execution do not create edges.

This graph is deliberately editorial and metatheoretic. It exposes hidden axiom, universe, equality, recursion, coinduction, and computation growth without assuming an internal universe or lattice of all type theories. The recent proposal to internalize such extensions remains an epilogue subject until its independent proof and application base satisfies the book’s admission test.