Tour 01: Foundations of Category τ

A 10-minute interactive introduction. Step through this file in VS Code with the Lean 4 extension — hover over #check and #eval to see results.

Category τ begins with 5 generators, 6 structural axioms, and a single primitive operator ρ. From these alone, TauLib derives arithmetic, algebra, analysis, physics, biology, and philosophy — with zero imports from Mathlib’s mathematical content.

Prerequisites: None. This tour is self-contained.