From Groups to Gravitational Waves: a pure-Lean-4 (no Mathlib), dimension-parametric formalization of mathematical physics through general relativity. 0 sorry; the n>=4 gravitational-wave threshold formalized.