Registry · Proposition II.P02 established formalized

II.P02 — Sector Inheritance

Every tau-admissible point inherits a bipolar sector assignment from the boundary structure via fiber coordinates, compatible with the idempotent decomposition of H_tau.

Book II Part 1 Ch. 7

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookII.Interior.BipolarDecomposition

Symbol: Tau.BookII.Interior.sector_complete