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 we track theorem proof dependencies separately from statement dependencies. For Lean module imports, the website's Graphs tab is the place to look.
Our 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.
Use a map entry after the corresponding explanation has given its declaration a meaning. An enclosure theorem, for example, depends on local transfer laws and hypotheses about the graph, and following those entries shows where its premises come from. But a dependency edge alone doesn't say that a runtime path satisfies those premises. An entry's statement and explanatory text identify the objects being related, while its source link leads to the actual definition or proof.