IV.R250 — Lean verification

All six cross-coupling formulas are encoded in TauLib.BookIV.Sectors.CouplingFormulas with structures cross_coupling_AD through cross_coupling_CD; the theorem cross_coupling_order verifies the strict ordering using rational bounds on iota_tau.