Registry · Theorem I.T20 tau-effective formalized

I.T20 — Composition Closure

HolFun is closed under composition: if f1 and f2 are tower-coherent reduce-form functions, then f1 o f2 is tower-coherent. Proven via reduction_compat on composed reduce-form functions.

Book I Part 13 Ch. 51

Dependency Graph

Depends on (2)

I.D47 I.D46

Depended on by (3)

I.D51 I.P24 I.T22

Lean Formalization

Module: TauLib.BookI.Holomorphy.DiagonalProtection

Symbol: Tau.Holomorphy.comp_reduce_coherent