Registry · Proposition I.P22 tau-effective formalized

I.P22 — Sector Independence

Every SectorFun is sector-independent by construction: B-output depends only on B-input, C-output depends only on C-input. The structural content of the split-CR equations.

Book I Part 13 Ch. 49

Dependency Graph

Depends on (1)

I.D42

Depended on by (2)

I.T40 I.T41

Lean Formalization

Module: TauLib.BookI.Holomorphy.DHolomorphic

Symbol: Tau.Holomorphy.sector_fun_independent