The Universe Postulate (K0)

The Universe Postulate (I.K0) is the foundational axiom of the τ-framework: there exists a small (∞, 1)-category τ — the categorical kernel — that supports the five canonical generators (K1–K5) under the no-ω axiom (K6). Everything else in the framework is a theorem about τ; the postulate asserts only that τ exists.

Categorical invariant. The single posited atom of the framework: an (∞, 1)-categorical universe τ with a distinguished collection of generators and a closure constraint.

Primary registry anchor: I.K0

Supporting items: I.K1, I.K2, I.K3, I.K4, I.K5, I.K6

1. I.K0 — Universe Postulate — the categorical kernel τ exists (foundational; no further derivation)

Lean modules referenced: TauLib.BookI.Kernel.Axioms

Status: Formalized

Module: TauLib.BookI.Kernel.Axioms

Lean kind: axiom

Lean symbol: Tau.BookI.Kernel.universePostulate