TauLib

Compiled Lean projection

TauLib now belongs to the Corpus lane because it is one of the Corpus projections: a compiled Lean module inventory, source map, Registry-link map, import graph, and generated module documentation.

That ownership move does not weaken verification. It makes the boundary cleaner: the Corpus publishes the compiled projection; Verify asks what the projection covers, what its formal terms mean, where semantic bridges hold, and what remains externally assessable.

• 512 Lean modules

  Lean modules in the pinned TauLib source projection.

• 142,406 lines

  Source lines counted from the imported TauLib snapshot.

• 14,601 declarations/evals

  Declarations and computational evaluations discovered by the projection scanner.

• 3,323 registry links

  Registry-to-module anchors that connect the atomic Corpus to Lean source.

Formalization Release Lines

TauLib publishes through two release lines plus a per-result proof-package layer. Each release line is a distinct citable surface with its own status, audience, and update cadence.

• TauLib v2 Snapshot

  Frozen Lean projection of the Second-Edition Corpus. Public · pinned · citable. The current public docs at taulib.site render against this snapshot; the snapshot's pinned commit + Lean toolchain are recorded in the Release Manifest.

• TauLib v3 Library

  Layered active library — import-isolated kernel, Mathlib-facing bridges, community-readable module structure. In preparation · private repository · not yet citable. See Verify · TauLib for the inspection-bridge framing.

• Research Modules / Proof Packages

  Isolated proof packages and reproducibility bundles for specific formal results. Each package has its own state (in construction · draft · candidate · released · superseded) and is citable per-package once released. See Formalization Release Lines.

The everything below (“Entry points”, “Verification boundary”) refers to the TauLib v2 Snapshot — the public release line. TauLib v3 surfaces will land as the layered library moves from private working to public release.

Entry points

• Module explorer

  Filter TauLib modules by book, family, module name, and Registry ID.

• Generated module docs

  One generated page per module with imports, source links, and Registry anchors.

• Projection status

  Counts, source pin, and projection boundaries.

• Architecture

  Book and family structure, import graph, and relation to the Monograph Corpus.

Verification boundary

Lean compilation is treated here as a published baseline artifact. The Verify lane is still the place to inspect semantic adequacy, bridge assumptions, empirical accountability, and external assessment.