Registry · Theorem VII.T02 tau-effective formalized

VII.T02 — E₃ Non-Emptiness

E₃ enrichment layer is non-empty; BH basin law-code satisfies SelfDesc² and provides canonical carrier.

Book VII Part 1 Ch. 4

Dependency Graph

Depends on (1)

VII.L01

Depended on by (2)

VII.L03 VII.R51

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.ENonemptiness