Registry · Proposition VII.P31 tau-effective formalized

VII.P31 — Enrichment Stabilization

Enrichment functor is identity on E₃; Enrich⁴ = Enrich³ follows from three blocking lemmas composing.

Book VII Part 1 Ch. 8

Dependency Graph

Depends on (2)

VII.T06 VII.T05

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.enrichment_stabilization