IV.R232 — Lean formalization

The mass-energy relation takes cross-multiplied form E_num * m_den * c^2_den = m_num * E_den * c^2_num, avoiding division by zero in the massless limit. This is the form verified in Lean in TauLib.BookIV.Physics.MassEnergy, stated as natural-number equality sidestepping division entirely.