TauLib
The Lean 4 formalization library for Category τ — 450 modules, 125,771 lines, 0 sorry in Books I-VI.
What TauLib Is
TauLib is the Lean 4 formalization library for the Panta Rhei Research Program. It machine-checks the mathematical claims of the seven-book monograph series, providing an independent verification layer that anyone can inspect and run.
Clone and build:
git clone https://github.com/Panta-Rhei-Research/taulib
cd taulib && lake build
Build completes with 0 errors and 0 sorry in Books I-VI.
What TauLib Verifies
Lean compilation verifies internal consistency: every theorem follows from the axioms, every definition type-checks, every computation evaluates. This is a strong guarantee — but it is not the same as empirical truth.
What Lean checks: The mathematical derivation chain from K0-K6 through to every claimed theorem.
What Lean does not check: Whether the framework’s physical predictions match experiment. That requires empirical testing.
How TauLib Relates to the Books
Each TauLib module corresponds to a specific chapter or section in the monograph series:
| Book | Modules | Key content |
|---|---|---|
| I — Foundations | 94 | Kernel axioms, orbit structure, coordinates, polarity, boundary |
| II — Holomorphy | 65 | Interior, topology, geometry, Central Theorem, Hartogs |
| III — Spectrum | 70 | Enrichment, sectors, spectral theory, computation, Millennium doors |
| IV — Microcosm | 89 | Particle physics, QM, electroweak, QCD, nuclear |
| V — Macrocosm | 80 | Gravity, cosmology, BBN, black holes, fluid dynamics |
| VI — Life | 30 | Life definition, genetics, cellular, ecology, consciousness |
| VII — Metaphysics | 7 | Ontology, ethics, Logos, final boundary |
| Tours | 8 | Interactive verification tours for different audiences |
Entry Points
Documentation
- API Documentation — 445 module pages generated from Lean 4 source
- Architecture — Module dependency graph and reading paths
- Formalization Status — Per-book statistics, axiom inventory, sorry inventory
- Scope Labels — The 4-tier scope classification system
- Glossary — Technical terms and conventions
Interactive Tours
- VerifyItYourself — 5 claims, verified live
- Foundations — Axioms and rigidity
- CentralTheorem — O(τ³) ≅ A_spec(L)
- Physics — 9 electroweak predictions
Repositories
- TauLib (contributor) — Active development
- Formalization (frozen) — Frozen verification snapshot