IV.R230 — Lean formalization

The three-way particle classification is formalized in TauLib.BookIV.Physics.QuantityFramework as inductive type ParticleKind with constructors ontic, radiation, and virtual. The OnticParticle structure bundles a defect configuration with proofs of persistence, localization, and full fiber topology.