Documentation Provenance

The full API reference is generated by doc-gen4 from an exactly pinned Lean/mathlib environment. It is generated documentation rather than project-authored Lean source, so it does not receive the project source header.

Generated static assets

The staged tree carries doc-gen4's generated CSS, JavaScript, search runtime, and favicon assets: style.css, color-scheme.js, declaration-data.js, expand-nav.js, find/find.js, how-about.js, importedBy.js, instances.js, jump-src.js, mathjax-config.js, nav.js, search.js, and favicon.svg. They come from doc-gen4 commit e2af49a, licensed Apache-2.0; that upstream revision has no NOTICE file.

Imported documentation

To keep rendered types, navigation, search, instances, and import links complete, the artifact also contains generated pages for Lean, Lake, Std, Init, mathlib, Aesop, Batteries, Qq, ProofWidgets, ImportGraph, LeanSearchClient, and Plausible. These pages are dependency documentation, not part of the claim that LeanInfoTheory supports 31 public modules and 601 public declarations. The assembled artifact includes an upstream licence directory; before assembly, that route is an explicit placeholder.

Network runtime dependencies

Generated pages currently request Lato 3.0.0 and JuliaMono 0.051 styles from cdnjs, the Polyfill v3 service from cdnjs, and MathJax 3 from jsDelivr. These files are not vendored into the site. Navigation and plain signatures remain available without them, while fonts, legacy browser compatibility, and mathematical typesetting may require network access. The website validation gate checks these requests and does not claim that the API site is fully self-contained.

Hand-written site styling

The hand-written site's styles.css is derived from the CC0-1.0 Cayman theme and deliberately carries no exclusive project copyright header.