Conventions

This blueprint maps the Lean formalization of the paper. An item marked formalized (green in the dependency graph) is proved in Lean with no sorry, from Mathlib primitives, under the standard axioms. Several assembly theorems consume explicitly named hypothesis bundles (documented in each entry); these are recorded as hypotheses of the Lean statements, not hidden assumptions. As of 11 July 2026 the tree contains no sorry: every result of the paper, including both classical tightness criteria (Aldous and Mitoma), is proved in Lean from Mathlib primitives.