IV.R282 — Lean formalization

The entropy splitting and its mu-invariance are encoded in TauLib.BookIV.Physics.Thermodynamics. The structure EntropySplit carries visible and hidden components; theorem total_entropy_invariant verifies that their sum is independent of the readout scale. Zero sorry.