IV.R237 — Lean formalization

The defect functional and Euler budget conservation are formalized in TauLib.BookIV.Physics.DefectFunctional and TauLib.BookIV.Physics.Thermodynamics. The eight fluid regimes are encoded as inductive type FluidRegime with membership predicates on the defect tuple.