IV.R236 — Lean formalization

The Planck character and tau-Heisenberg inequality are formalized in TauLib.BookIV.Physics.PlanckCharacter. The attainment statement uses the saturation theorem from TauLib.BookII.Interior.Saturation. Zero sorry terms in the formalization.