Scale roadmap inventories and the full DAG explorer

[Deicyde]

Closes #60. Includes the now-merged #95 trusted-snapshot layer.

Summary

• Teach Roadmap to inventory existing modules and declarations across a repository boundary without treating source inventories as mathematical proof targets.
• Replace every generated Mermaid dependency map—and the separate legacy full-DAG viewer—with one deterministic Canvas + semantic DOM explorer. Authored Mermaid diagrams remain supported.
• Give project, chapter, nested-scope, and compatibility routes the same search, filters, Map/Browse modes, inspector, path pivots, URL-addressable focus, and mobile bottom sheet.
• Never lay out the whole repository. Start with readable chapter cards, drill through authored scopes, and lazily load a compact global catalog only for search and legacy deep links.
• Render authored mathematical area: values or blueprint/atlas.json assignments as region hulls; topic bubbles are sized by scope, carry exact status rings and internal-dependency counts, and open authored prose in a persistent reading panel before drilling.
• Consolidate catalog leaves into their parent inventory pages, avoiding one generated HTML page per module.

Inventory contract

catalog: module is non-dispatchable and excluded from the Scoped roadmap completion percentage. It is reported through a separate neutral inventory metric and the INVENTORIED coverage disposition.

A catalog must:

• omit declaration and Mathlib-target metadata;
• link a local declaration ledger under blueprint/sources/ from ## Sources;
• list exact compiled public names in lean: before asserting formalized status; and
• be reached by INVENTORIED coverage evidence rather than standing in for DECOMPOSED mathematical exposition.

check --lean-root resolves every listed name. Completeness against declarations added later remains an authored assertion; #100 tracks deterministic inventory-drift reconciliation.

Unified explorer

The interaction model combines WikiLean's calm hierarchy and article context with LeanStructure's fast pan/zoom and pivot navigation:

• a true 100dvw × 100dvh application surface rather than a card inside a Material article;
• a 62/38 map-plus-reading layout for atlas views, with authored mathematical summaries, regions, Lean names, and honest zero-edge messaging;
• deterministic left-to-right DAG layout on desktop and top-to-bottom layout on mobile, with balanced grids for chapters that have no cross-edges;
• Canvas topology with bounded, keyboard-accessible DOM node controls and a complete paginated list mode;
• ranked title/id search, status and isolate filters, exact hidden counts, and no unbounded “show all” controls;
• persistent inspector with direct relations, transitive prerequisite/dependent pivots, article links, and neutral inventory language;
• durable #node=, direction, filter, isolate, and view state with duplicate-history suppression;
• readable-scale fitting: connected maps pan instead of shrinking below a 44 px interaction target;
• scopes above 120 direct items open honestly in Browse/search instead of drawing an unreadable cloud;
• ordinary scrolling when embedded, one-finger pan in the full-page app, modifier-wheel zoom, two-finger pinch, responsive bottom sheet, and semantic no-JavaScript/fetch-failure fallback;
• one generated viewer for all scales. /dependencies/full.html remains only as a stable compatibility route, not a second implementation or top-level competing view.

The runtime is dependency-free and 55.4 KB. Active projections, transitive path sets, and search results are cached between camera frames; search and hub relations grow in bounded 50-row batches.

Publication architecture

• Publication renders from one retained source snapshot supplied by Bind Lean source snapshots to filesystem generations #95; later edits cannot mix into emitted bytes.
• Publication v2 records the captured source hash and capability (retained-descriptor or portable-best-effort). Runtime v3 retains module catalogs and adds the open-statement policy, assumptions, waiting states, and retractions while preserving old-pickle compatibility.
• Automatic Lean links remain commit/blob-attested. Markdown, graph-data, and script URLs percent-encode authored path components.
• Scope payloads validate their schema, compute topology independently of node order, handle collapsed-view cycles deterministically, separate isolates from connected layout, distinguish scopes/boundaries/inventories, and preserve edge multiplicities.
• Markdown prose supplies bounded wiki excerpts; area: and atlas.json are authored mathematical taxonomies, never inferred from imports, paths, or titles. Containment regions and typed dependency arrows remain distinct.
• Markdown links whose labels contain bracketed inline mathematics are rewritten to consolidated parent anchors, so omitted catalog leaves never leave dead site links.
• dependencies/index.json contains searchable identity/context only—no edges or layout. Search opens the smallest authored scope containing a result.
• Existing v1 output directories can be clean-upgraded. Old /full.html#node=… bookmarks resolve through the global index into the same hierarchical explorer.

Scale evidence

• On the 14,576-entry Formal-Math corpus, both the project route and legacy full-route shell render only 36 subjects; no all-node graph is emitted.
• The local Formal-Math atlas now has seven authored mathematical regions, 36 subject summaries, exact per-region counts, and internal-dependency totals; it states honestly that the root currently has no authored cross-domain edges.
• The lazy searchable catalog is 4.86 MB raw, while the largest non-root scope projection contains only 21 visible items.
• A valid 1,200-catalog hierarchy rendered to 32 Markdown pages and 2.15 MB of site source in 48.29 seconds, with zero per-catalog leaf pages.
• The earlier 990 MB Formal-Math result predates the repaired evidence contract and is intentionally withdrawn: those catalogs must be regenerated with exact lean: names and canonical ## Sources ledgers before a new end-to-end benchmark is meaningful.

Validation

• GitHub Python 3.10 and 3.13 each pass Ruff, all 1,849 tests (53 skipped, 1 expected failure), make check-example, and the strict MkDocs build.
• Nineteen Playwright/WebKit cases cover knowledge-atlas regions/status rings/prose, full-viewport geometry, connected chain/star readability, 1,000-item flat-scope fallback, mobile overlap/panning/pagination, global search and legacy routing, keyboard focus, history/Back, selection/filter state, duplicate script inclusion, and no-JavaScript/fetch-failure fallbacks.
• A strict 14,576-article Formal-Math MkDocs build passes with absorbed catalog links, including bracketed mathematical labels, rewritten to their parent anchors.
• GitHub Python 3.10, Python 3.13, WebKit, Windows, real-Lean, and CLA checks all pass at 2e2633e7; the Windows job also exercises the native directory-generation guard added during the final main merge.
• Independent backend, adversarial UX/accessibility, performance, and final integration reviews: approved; no known code blocker.

[Deicyde]

Final repair head is 2e2633e7. It closes the catalog fail-open path in audit/Doctor, restores current-main development guidance, uses canonical Lean-name parsing, corrects publication-v2 prose, fails closed on dangling atlas symlinks, and versions the changed public outputs as runtime v4 / coverage v2. Exact local full suite: 1,895 passed, 7 skipped, 1 expected failure; focused schema/render/audit suite: 299 passed; lint and check-example pass. Exact-head CI is running.

[Deicyde]

Final exact-head status at 2e2633e7: all 11 GitHub checks pass; local full suite 1,895 passed, 7 skipped, 1 expected failure; schema/render/audit focused suite 299 passed; Ruff and check-example pass; independent catalog and schema reviews approve. Ready for human review. Merge order: land #165 first, then restack #90 onto that transactional publication boundary before merging #90. Given #90’s long history, squash-merge it after the restack.

[Deicyde]

Stack correction: #165 and #90 independently define incompatible autoform-publication/v2 contracts. Green CI on each sibling head does not validate their combination. #90 is reviewable for its inventory/explorer design, but this exact head must not merge. Land #165 first, port the explorer onto its retained transactional publication path, resolve the combined contract with a new schema version (normally v3), rerun the full suite and all 11 checks, then restore review: ready and squash-merge.