TauLib Architecture

Book and family structure

TauLib follows the Corpus construction rather than standing outside it. Module families track books, construction layers, and local formalization neighborhoods.

BookI

• Addressability

  4 modules.

• Boundary

  39 modules.

• CF

  1 module.

• Coordinates

  13 modules.

• Denotation

  9 modules.

• Holomorphy

  12 modules.

• Kernel

  4 modules.

• KernelFoundation

  4 modules.

• Logic

  3 modules.

• MetaLogic

  7 modules.

• Orbit

  8 modules.

• Polarity

  21 modules.

• Sets

  8 modules.

• Topos

  13 modules.

• Root

  1 module.

BookII

• CentralTheorem

  7 modules.

• Closure

  7 modules.

• Domains

  3 modules.

• Enrichment

  6 modules.

• Geometry

  5 modules.

• Hartogs

  9 modules.

• Interior

  5 modules.

• Mirror

  5 modules.

• Prologue

  1 module.

• Regularity

  5 modules.

• Topology

  6 modules.

• Transcendentals

  6 modules.

• Root

  1 module.

BookIII

• Arithmetic

  9 modules.

• Bridge

  8 modules.

• Computation

  6 modules.

• Doors

  10 modules.

• Enrichment

  3 modules.

• Hinge

  2 modules.

• Mirror

  3 modules.

• Physics

  7 modules.

• Prologue

  1 module.

• Sectors

  4 modules.

• Spectral

  13 modules.

• Spectrum

  4 modules.

• Root

  1 module.

BookIV

• Arena

  6 modules.

• Calibration

  15 modules.

• Coda

  3 modules.

• Electroweak

  17 modules.

• ManyBody

  6 modules.

• MassDerivation

  3 modules.

• Particles

  7 modules.

• Physics

  11 modules.

• QuantumMechanics

  7 modules.

• Sectors

  6 modules.

• Strong

  8 modules.

• Root

  1 module.

BookV

• Astrophysics

  12 modules.

• Coda

  5 modules.

• Cosmology

  18 modules.

• FluidMacro

  7 modules.

• Gravity

  5 modules.

• GravityField

  13 modules.

• Orthodox

  5 modules.

• Prologue

  2 modules.

• Temporal

  7 modules.

• Thermodynamics

  6 modules.

• Root

  1 module.

BookVI

• Agency

  2 modules.

• Closure

  2 modules.

• Consumer

  7 modules.

• CosmicLife

  4 modules.

• LifeCore

  4 modules.

• Mind

  2 modules.

• Persistence

  2 modules.

• Sectors

  4 modules.

• Source

  3 modules.

• Root

  1 module.

BookVII

• Ethics

  1 module.

• Final

  1 module.

• Logos

  1 module.

• Meta

  4 modules.

• Social

  1 module.

• Root

  1 module.

Meta

• Root

  1 module.

Tour

• Root

  8 modules.

• GuidedTour

  7 modules.

Root

• Root

  1 module.

Relation to Verify

Architecture here means Corpus architecture: modules, imports, and Registry anchors. Verify uses this architecture to ask higher-level questions about coverage, bridge adequacy, and claim boundaries.

Categorical structure note

TauLib does not import Mathlib.CategoryTheory or instantiate the Mathlib Category typeclass on TauObj. The categorical structure of τ is realized through hand-rolled morphism types (CatTau, HolEndCat, TauArrow, id_arrow, arrow_comp_stage) defined within TauLib itself, rather than as an instance : Category TauObj.

This is a deliberate architectural choice — the program treats τ as a categorical structure in its own right, with the morphism layer earned from K0–K6 and the progression operator ρ rather than inherited from Mathlib’s general category-theory hierarchy. A reviewer should expect to find:

• class Category / def Hom / Iso constructions inside TauLib/BookI/Category/… and TauLib/BookII/Categorical/…, not via Mathlib instances.
• A separate Mathlib-bridge layer (where Mathlib CategoryTheory is used as a comparison target) is on the formalization roadmap; it is not part of the current release.

The K0–K6 themselves are realized in TauLib as theorems-by-construction over the inductive Generator and TauObj types — i.e. they hold for the chosen representation by definition of how those inductives are built — rather than as Lean axiom declarations in the strict TCB sense. The three custom axioms that do sit outside Mathlib’s trusted base are inventoried separately at Custom Axioms; K0–K6 are not among them. This is why the program describes K0–K6 as the kernel’s structural commitments on the marketing surface rather than as its TCB axioms.