Next: freeze source versions, chapter contracts, assumptions and theorem locators; retrieve existing declarations and prove only the missing interfaces. Chapter numbers, page coverage and completion totals will appear after that audit.
One underlying Lean graph
All references resolve to canonical declarations in the global index. Reading views do not create additional Lean modules.