Registry · Remark
IV.R392
tau-effective
formalized
IV.R392 — OQ-B2 Resolved
OQ-B2 RESOLVED: 5/7 = EW projection density on A_spec(L). Residual: CF Compression Thesis.
Lean Formalization
Module: TauLib.BookIV.Electroweak.EWProjection
Symbol: remark_oq_b2_resolved