8. Formalization Map
The chapters below trace the main definitions, executable boundaries, and proved results through TorchLean. This is a declaration-level map: an edge records a mathematical or implementation dependency between selected entries, and theorem proof dependencies are tracked separately from statement dependencies. The website's Graphs tab remains the place to inspect Lean module imports.
The selection favors declarations that explain an entire subsystem. Small helper lemmas stay in the API reference, where their full statements and source locations are easier to inspect.