Registry · Theorem VII.T05 tau-effective formalized

VII.T05 — Canonical Ladder Theorem

Enrichment series is canonical ladder: non-empty at every layer, strictly increasing, terminated by Saturation Theorem.

Book VII Part 1 Ch. 7

Dependency Graph

Depends on (3)

VII.L03 VII.L04 VII.T06

Depended on by (2)

VII.P02 VII.P31

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.CanonicalLadderTheorem