IV.R252 — Lean formalization

Lean verification: temporal_multiplicative in TauLib.BookIV.Sectors.CouplingFormulas, proved by ring. The spatial sectors B and C do not sum to 1; the remaining spatial budget is absorbed by the omega-sector at the crossing point.