TauLib

TauLib is the public Lean 4 formalization repo of the Panta Rhei Research Program.

This repository is the active contributor-facing source for Lean development: build files, source modules, guided tours, documentation generation, CI, and issue/PR review. The full research-program observatory lives at panta-rhei.site, while the dedicated Lean documentation site generated from this repo is taulib.site.

TauLib verifies formal proof obligations where they are represented in Lean. It does not, by itself, establish empirical truth, bridge adequacy, semantic correspondence to prose, or external scientific acceptance. Current release metrics, trusted-base details, axiom/sorry status, and count reconciliation are published in the Release Manifest.

Start Here

Need	Route
Read the public verification overview	Verify / TauLib
Check current metrics and trusted base	Release Manifest
Browse generated Lean documentation	taulib.site
Inspect the source	TauLib/ and TauLib.lean
Report a concrete Lean defect	TauLib Issues
Ask a public question	Organization Discussions

Quick Start

Prerequisites

• Lean 4 via elan (version managed by lean-toolchain)

Clone and Build

git clone https://github.com/Panta-Rhei-Research/taulib.git
cd taulib
lake build

The first build downloads Mathlib (for tactics) and compiles ~1,256 lake jobs. Subsequent builds use the cache and are fast.

Use as a Dependency

Add to your lakefile.lean:

require TauLib from git
  "https://github.com/Panta-Rhei-Research/taulib.git" @ "main"

Or in lakefile.toml:

[[require]]
name = "TauLib"
git = "https://github.com/Panta-Rhei-Research/taulib.git"
rev = "main"

Dedicated Documentation Site

The taulib.site site is generated from this repository. Its purpose is narrow: expose Lean-oriented documentation, module pages, source links, and pointers back to the full verification context on panta-rhei.site.

The documentation workflow uses doc-gen4, filters the generated output to TauLib content, extracts module pages into the Jekyll documentation shell under site/, and deploys through GitHub Pages.

# First build (initializes doc-gen4):
cd docbuild && MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 && cd ..

# Generate full documentation:
./scripts/build_docs.sh

# Preview locally:
cd docbuild/.lake/build/doc && python3 -m http.server 8000

Guided Tours

Open these files in VS Code with the Lean 4 extension and step through line by line:

Tour	Time	What You'll See
Tour/VerifyItYourself.lean	15 min	Start here. 5 surprising claims, verified live — the skeptic’s tour
Tour/Foundations.lean	10 min	5 generators, 7 axioms, ρ operator, master constant, rigidity
Tour/CentralTheorem.lean	10 min	Split-complex ring, τ³ fibration, O(τ³) ≅ Aspec(ℒ)
Tour/Physics.lean	15 min	EW synthesis, 3 generations, CMB, rotation curves, baryogenesis
Tour/OneConstant.lean	10 min	Full constants ledger: α, h, ℓ₁, ωb, r — all from ιτ
Tour/MillenniumProblems.lean	15 min	GRH, BSD, Poincaré, Hodge, Navier-Stokes through the τ-lens
Tour/LifeFromPhysics.lean	10 min	4+1 life sectors, genetic code, neural architecture, crossing limit
Tour/MindAndEthics.lean	15 min	Categorical Imperative, consciousness, free will, Logos, the three structural commitments (Commitment defs replacing the v2 sorry encoding)

Pick Your Path

Audience	Start With	Then Explore
Skeptic / Reviewer	Tour/VerifyItYourself	Tour/OneConstant → any module you doubt
Mathematician	Tour/Foundations → Tour/CentralTheorem	Tour/MillenniumProblems → BookIII/Doors/GrandGRH
Physicist	Tour/Physics → Tour/OneConstant	BookIV/Electroweak/EWSynthesis → BookV/Cosmology/CMBSpectrum
Biologist	Tour/LifeFromPhysics	BookVI/Source/GeneticCode → BookVI/Consumer/Neural
Philosopher	Tour/MindAndEthics	BookVII/Ethics/CIProof → BookVII/Final/Boundary
Lean user	Tour/Foundations → lakefile.lean	Browse generated documentation and source modules

See the Architecture Guide for detailed reading paths, dependency graphs, and per-book start files.

---

Module Architecture

TauLib modules are organized under seven book namespaces plus guided tours. The dependency order is strict: each book builds only on what came before.

TauLib
 ├── BookI    Categorical Foundations
 ├── BookII   Categorical Holomorphy
 ├── BookIII  Categorical Spectrum
 ├── BookIV   Categorical Microcosm
 ├── BookV    Categorical Macrocosm
 ├── BookVI   Categorical Life
 ├── BookVII  Categorical Metaphysics
 └── Tour     Interactive Guides

Book I — Categorical Foundations (94 files, 20,554 lines)

The foundation builds everything from the 5 generators, using 12 module families:

Family	Files	Content
Kernel	4	5 generators, axioms K0–K6, ρ operator
Orbit	8	Orbit generation, closure, iterator ladder, rigidity: Aut(τ) = {id}
Denotation	9	τ-Idx (earned natural numbers), rank transfers, program monoid
Coordinates	10	Normal form, ABCD chart, hyperfactorization, Chebyshev coordinates
Polarity	14	Prime Polarity Theorem, lemniscate ℒ, CRT, bipolar algebra
Boundary	14	Split-complex ring ℍ[j], number tower, ιτ, characters
Sets	8	Internal set theory, Cantor refutation, counting
Logic	3	Truth₄ logic, explosion barrier, Boolean recovery
Holomorphy	9	ω-germ transformers, Global Hartogs, presheaf essence
Topos	7	Earned arrows, functors, sites, sheaves
MetaLogic	7	Proof-theoretic mirror, linear discipline, structural exclusion
CF	1	Continued fraction window algebra

Books II–VII

Book	Key Content
II Holomorphy	τ³ = τ¹ ×f T², Central Theorem: O(τ³) ≅ Aspec(ℒ)
III Spectrum	Spectral forces, Millennium-problem stress tests, τ-Turing machine
IV Microcosm	Electroweak synthesis, generations, Majorana, strong CP, Higgs
V Macrocosm	Gravity, CMB, rotation curves, baryogenesis, lensing
VI Life	Life predicate, origin-of-life surfaces, neural architecture
VII Metaphysics	Saturation, archetypes, Categorical Imperative, social ontology

---

Key Results

Formalized results with their Lean entry points:

Result	Lean Identifier	ppm	Book
Central Theorem: O(τ³) ≅ Aspec(ℒ)	central_fwd_3_15	—	II
Rigidity: Aut(τ) = {id}	rigidity_non_omega	—	I
Three Generations: H₁(τ³; ℤ) ≅ ℤ³	gen_count_three	exact	IV
9 EW Quantities from ιτ + mn	nine_ew_quantities	sub-ppm	IV
Majorana Neutrinos: σ = Cτ	all_neutrinos_majorana	—	IV
Strong CP: θQCD = 0	theta_qcd_zero_from_sa_i	exact	IV
CMB First Peak: ℓ₁ (NLO)	first_peak_holonomy_thm	+69	V
20 Galaxy Rotation Curves	flat_rotation_theorem	RMS 0.067 dex	V
Baryogenesis: ηB = α · ιτ15 · (5/6)	sakharov_reduction	~1%	V
S₈ Tension Resolved: S₈ = 0.783	s8_tau_value	within 1σ	V
Categorical Imperative as j-closed fixed point	ci_j_closed_fixed_point	—	VII
Saturation: Enrich(E₃) = E₃	saturation_theorem	—	VII

---

Axioms and Sorry

TauLib is maximally transparent about its foundations. The Release Manifest is the authoritative public status page for current axiom and sorry counts.

3 Axioms (all conjectural, all Book III)

Axiom	Module	Classification	Pattern
bridge_functor_exists	BookIII/Bridge/BridgeAxiom	Conjectural	Finite checks pass; axiom asserts ∀ n
spectral_correspondence_O3	BookIII/Doors/SpectralCorrespondence	Conjectural	Finite checks pass; axiom asserts ∀ n
grand_grh_adelic	BookIII/Doors/GrandGRH	Conjectural	Finite checks pass; axiom asserts ∀ n

All three follow a "compute-then-axiomatize" pattern: a decidable finite check is verified computationally via native_decide, then an axiom asserts the property holds universally. This makes the conjectural boundary maximally sharp and auditable. Every theorem whose proof transitively invokes one of these axioms is a conditional result, conditional on the universal extension of the named finite-checked predicate. CI on every push to main asserts the count is exactly 3 via test $(grep -r '^axiom ' TauLib/ --include='*.lean' | wc -l | tr -d ' ') = 3.

Retired in peer-review-fixes-v1 (2026-04-19): a fourth axiom, central_theorem_physical : True in BookIV/Arena/BoundaryHolonomy, was deleted. An axiom of type True is a no-op — True is inhabited by trivial, so the declaration added nothing to the theory while inflating the axiom count. The architectural intent (pointing the Book IV reader at the Book II Central Theorem) is now carried by documentation comments and the registry cross-reference [IV.T96].

0 Sorry (target state, post peer-review-fixes-v1)

The v2 state of the library shipped with three theorem X : True := sorry declarations in Book VII — one each for omega_point_theorem, science_faith_boundary, and no_forced_stance. Pre-publication simulated peer review identified this encoding as performative: True is inhabited by trivial, so a sorry on a True goal is a marker with no formal content, and no_forced_stance : True := sorry was being justified by citation of registry VII.T47 — which was itself no_forced_stance. Self-referential.

The peer-review-fixes-v1 PR retires all three by replacing them with def values of a Commitment structure (in TauLib/BookVII/Meta/Commitment.lean) carrying the commitment's statement, warrant, and registry_id as inspectable data:

Declaration	Module	Kind	Encodes
omega_point_theorem	BookVII/Logos/Sector	def : Commitment	[VII.T46] ω-Point commitment; warrant cites VII.T47
science_faith_boundary	BookVII/Logos/Sector	def : Commitment	[VII.P29] science-faith boundary; Reg_C stance-stability
no_forced_stance	BookVII/Final/Boundary	def : Commitment	[VII.T47] No-Forced-Stance; constitutive of the framework

#print axioms omega_point_theorem reports no axioms (these are defs, not axioms or theorems). rg ':= sorry' TauLib/ returns zero matches at the release state documented in the Release Manifest. Books I–VI have been sorry-free since Wave 12; the v2 Book VII sorries were retired in peer-review-fixes-v1.

---

Dependency Policy

TauLib uses Mathlib for proof tactics only:

Allowed	Not Allowed
simp, omega, ring, aesop	Mathlib.Order.*
decide, native_decide, norm_num	Mathlib.Algebra.*
linarith, positivity, field_simp	Mathlib.CategoryTheory.*
constructor, exact, apply	Mathlib.Topology.*

The dependency policy is designed to make imported mathematical content visible. TauLib uses Mathlib for tactics and infrastructure, while framework-specific mathematical constructions are represented in this repository. This does not mean that Lean compilation alone settles the program's external mathematical, empirical, or interpretive claims; those boundaries are recorded on the main verification site.

---

The Books

TauLib formalizes content from the Panta Rhei series (2nd Edition, 2026):

#	Title	Chapters	LaTeX Pages
I	Categorical Foundations	83	461
II	Categorical Holomorphy	66	484
III	Categorical Spectrum	104	415
IV	Categorical Microcosm	83	455
V	Categorical Macrocosm	97	504
VI	Categorical Life	45	412
VII	Categorical Metaphysics	74	521
	Total	552	3,252

Available at panta-rhei.site.

---

Documentation

Document	Description
Architecture Guide	Module dependency graph, reading paths by audience, per-book start files
Scope Labels	The 4-tier scope discipline: established, τ-effective, conjectural, metaphorical
Glossary	Key terms, symbols, constants, and registry ID format
Formalization Status	Local status notes; authoritative current metrics live in the Release Manifest
Contributing	Issue reporting, code style, citation, and fork guidelines

---

Building and Development

# Build the full library (~1,256 lake jobs)
lake build

# Build a specific book
lake build TauLib.BookI

# Check Lean version
cat lean-toolchain

Continuous Integration

Every push to main triggers a full lake build via GitHub Actions. The CI badge at the top of this README reflects the latest build status.

---

Citation

If you use TauLib in academic work, please cite:

@software{taulib2026,
  author    = {Fuchs, Thorsten and Fuchs, Anna-Sophie},
  title     = {{TauLib}: Mechanized Formalization of Category $\tau$},
  year      = {2026},
  version   = {2.0.0},
  url       = {https://github.com/Panta-Rhei-Research/taulib},
  note      = {Lean 4 source repository; current metrics and trusted-base details are maintained in the Panta Rhei Release Manifest},
  license   = {Apache-2.0}
}

Or use GitHub's "Cite this repository" feature, which reads from CITATION.cff.

---

License

Copyright 2025–2026 Thorsten Fuchs and Anna-Sophie Fuchs.

Licensed under the Apache License, Version 2.0.