IV.R272 — Lean formalization

The complete Planck character construction is formalized in TauLib.BookIV.Physics.PlanckCharacter with three key theorems: planck_sigma_fixed (sigma-fixedness), planck_attained_min (minimality), and planck_from_relational (hbar = M*L^2*H/(2pi)). All zero sorry.