Registry · Lemma VII.L03 tau-effective formalized

VII.L03 — Non-Emptiness at Each Layer

Each enrichment layer E_k (k=0,1,2,3) is non-empty with constructive carriers: kernel, holonomy sectors, Life predicate, BH basin law-code.

Book VII Part 1 Ch. 7

Dependency Graph

Depends on (2)

VII.L01 VII.T02

Depended on by (2)

VII.L18 VII.T05

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.NonemptinessAtEachLayer