Registry · Theorem VII.T03 tau-effective formalized

VII.T03 — Sector Decomposition at E₃

Every E₃-admissible content belongs to exactly one of five sectors; four pure sectors pairwise disjoint except at S_L intersection.

Book VII Part 1 Ch. 5

Dependency Graph

Depends on (2)

VII.D05 VII.D07

Depended on by (6)

VII.L05 VII.L06 VII.P03 VII.R52 VII.T04 VII.T38

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.SectorDecompositionAtE