From the article to the entire proof

What the inventory proves

Module ownership is the denominator: every project declaration, every complete type, every available theorem or definition body, and recursor reduction rules are included. Every compiled type, proof body and elaborated child link remains available. Original source projects and tactic scripts remain private. Shared subterms are stored once; exact expanded occurrence counts are computed without unfolding the graph. Large branches are collapsed visually and can be opened by their node number.

Article links identify a reviewed proof or supporting-module context. They do not certify that every article sentence follows from Lean. Lean/Mathlib dependencies outside this project remain named external boundaries. Surface syntax, tactics, macros and elaborator state are distinct from the twelve kernel expression constructors; the kernel diagram represents elaborated terms.