1.3. Documentation coverage🔗

The catalog is regenerated by scripts/generate-blueprint-catalog.py. Its committed JSON audit records every explicit public definition, abbreviation, opaque declaration, inductive type, structure, class, theorem, and lemma in the Lean source. It also records private declarations as deliberate exclusions. Build-time statistics, docstring coverage, generated reader cues, source previews, and catalog assignments are displayed by the unified website rather than copied into this prose. Structure-generated projections are accessible through their parent structure but are not double-counted as source declarations.

The full library, including RobinMatrix.lean, is expected to build with zero open proofs. RobinMatrix has its own research catalog because a compiled counterexample, interface, or conditional theorem must not be confused with an end-to-end certificate of the cited paper.