TauLib's modules follow a strict dependency order. Each layer builds only on what came before.
Book I (Foundations)
Kernel ─→ Orbit ─→ Denotation ─→ Coordinates
│
Polarity ─→ Boundary
│ │
Sets, Logic Holomorphy
│ │
Topos ───────┘
│
MetaLogic
│
CF
Book II (Holomorphy)
Interior ─→ Domains ─→ Topology ─→ Geometry
│
Transcendentals ─→ Enrichment ─→ CentralTheorem
│
Regularity ─→ Hartogs ─→ Closure ─→ Mirror
Book III (Spectrum)
Enrichment ─→ Sectors ─→ Spectral ─→ Arithmetic
│
Bridge ─→ Computation ─→ Doors ─→ Hinge
│
Physics ─→ Mirror ─→ Spectrum (TTM)
Books IV–VII build on I–III
BookIV (Microcosm) ──→ BookV (Macrocosm) ──→ BookVI (Life) ──→ BookVII (Metaphysics)
"Show me the axioms and what they imply."
BookI/Kernel/Signature.lean— The 5 generators and ρ operatorBookI/Kernel/Axioms.lean— Axioms K1–K6BookI/Orbit/Rigidity.lean— Aut(τ) = {id} (categoricity)BookI/Boundary/Iota.lean— The master constant ι_τ = 2/(π+e)BookII/CentralTheorem/CentralTheorem.lean— O(τ³) ≅ A_spec(L)BookIII/Bridge/BridgeAxiom.lean— The one conjectural gap
"I don't believe this. Show me the evidence."
Tour/VerifyItYourself.lean— 5 extraordinary claims, verified liveTour/OneConstant.lean— Full constants ledger from ι_τ aloneBookIII/Bridge/BridgeAxiom.lean— The scope ledger: what is proved vs. conjectured
"Show me the predictions."
Tour/Physics.lean— Interactive overview of all key predictionsTour/OneConstant.lean— α, h, ℓ₁, ω_b, r — all from ι_τBookIV/Electroweak/EWSynthesis.lean— 9 EW quantities from ι_τ + m_nBookV/Cosmology/CMBSpectrum.lean— CMB first peak at +69 ppmBookV/Astrophysics/RotationCurves.lean— 20 galaxies, no dark matter
"Show me the proofs."
Tour/Foundations.lean— 5 generators, 7 axioms, rigidityTour/CentralTheorem.lean— O(τ³) ≅ A_spec(L) holographic isomorphismTour/MillenniumProblems.lean— GRH, BSD, Poincaré through the τ-lensBookI/Orbit/Rigidity.lean— Aut(τ) = {id}BookIII/Doors/GrandGRH.lean— Spectral reformulation of RH
"Show me how life emerges."
Tour/LifeFromPhysics.lean— 4+1 life sectors, genetic code, neural archBookVI/Source/GeneticCode.lean— Codon degeneracy as error correctionBookVI/Consumer/Neural.lean— Neural architecture as τ³ computerBookVI/CosmicLife/CrossLimit.lean— The Crossing-Limit Theorem
"Show me the ethics and metaphysics."
Tour/MindAndEthics.lean— CI formalization, consciousness, free will, LogosBookVII/Ethics/CIProof.lean— The Categorical Imperative as theoremBookVII/Logos/Sector.lean— Consciousness as global sectionBookVII/Final/Boundary.lean— Boundary commitments encoded as inspectable dataBookVII/Social/Ontology.lean— Social ontology as sheaf theory
"Show me how it's built."
Tour/Foundations.lean— Interactive walkthrough of the axiomslakefile.lean— Mathlib tactics-only dependency policyBookI/Kernel/Axioms.lean— See how axioms become Lean theorems- Browse generated module documentation or the source tree
| Book | Start Here | What You'll Find |
|---|---|---|
| I | BookI/Kernel/Signature.lean |
The 5 generators — where everything begins |
| II | BookII/Interior/Tau3Fibration.lean |
The τ³ = τ¹ ×_f T² construction |
| III | BookIII/Enrichment/CanonicalLadder.lean |
The E₀ ⊊ E₁ ⊊ E₂ ⊊ E₃ ladder |
| IV | BookIV/Sectors/SectorParameters.lean |
The 5 sector decomposition |
| V | BookV/Gravity/GravitationalConstant.lean |
G from the torus vacuum |
| VI | BookVI/LifeCore/Distinction.lean |
The 5-condition life predicate |
| VII | BookVII/Meta/Saturation.lean |
Saturation theorem |
This architecture note describes reading paths and module families. It does not own current counts. See the Release Manifest for the authoritative module, declaration, axiom, sorry, and trusted-base status.