Curriculum topology
Book Map and Part IV nodes connect mathematical reading order to the modules and declarations that currently support each chapter.
Generated library topology · progressive disclosure
Underlying Lean Graph of BanditRLlib
Start with the library trunk, then open one curriculum, source chapter, module, milestone, or declaration branch at a time. Search can jump directly to any of the 10,434 indexed Lean declarations without drawing the whole library at once.
10Book Map chapters
5Part IV source chapters
796Lean modules
10,434indexed declarations
Reading rule. Formal module/import/declaration structure and reviewed compiled evidence remain distinct from conceptual overlays. The Settings ↔ techniques view is deliberately dashed: it explains why different bandit settings need different mathematical moves, but it does not turn those teaching/research links into Lean theorem dependencies. Whole-chapter status and individual compiled declarations remain separate.
Shared canonical nodes. Empty views have source mapping pending.
Loading graph…
Mobile starting view
Choose a readable branch first
The interactive canvas is available on demand; these direct routes keep the first mobile view readable and leave vertical scrolling uninterrupted.
No matching branch is visible.
Click or press Enter on a node to inspect and expand it · drag to pan · wheel to zoomThree graph layers, three meanings
Lean library topology
Module-import and reviewed teaching edges expose reusable prerequisites. Search reveals an exact declaration together with its parent module and recorded neighbors.
Proof-structure evidence
The Proof Graph Laboratory separately reports the frozen compiled-environment observation and experimental support-compression metrics.
Progressive-loading boundary. Views, searches, and module branches load independent generated JSON slices. The complete 11,347-node export is never fetched automatically; researchers can download the full graph artifact explicitly.
Evidence boundary. The browser graph is a generated navigation index, not a kernel trace, elaborator trace, or proof certificate. Exact Lean statements and the verified build gate remain authoritative.
What a contribution changes
- Reuse an existing branch.A new theorem points to the exact modules and declarations it consumes instead of duplicating them.
- Close a named leaf.A partial or blocked milestone gains compiled evidence while its broader chapter boundary stays honest.
- Add a cross-branch bridge.A reviewed dependency edge records a reusable connection between algorithm families or mathematical layers.
- Expose an unresolved interface.A missing history law, concentration bridge, or source theorem remains visible rather than appearing as proved.
The independent interaction design is informed by Samplinglib's public Underlying Lean Graph of Libraries. No Samplinglib source, stylesheet, template, or graph data is copied.