IV.R224 — Lean formalization

The Generator-Sector Correspondence is formalized in TauLib.BookIV.Sectors.SectorParameters with five sector instantiations. Injectivity of Phi on primitive sectors is verified as gen_sector_injective with zero sorry terms. The 4+1 structure (four primitive + one derived) is forced.