feat(Pseudo-Riemannian/Lorentzian): major refactor / add Lorentzian metric

[or4nge19]

Major refactor, mostly to align to and follow patterns from the recent mathlib Riemannian API and ongoing mathlib Levi-Civita pipeline. Main improvements:

• upgraded smoothness (from chart to ContMDiff)
• implementation of canonical inertia data for a real quadratic form on a finite-dimensional real
  vector space (for a more robust negDim condition and PR/Lorentzian constraints)
• extracted a more general MetricTensor and properties from Pseudo-Riemannian.
• trimmed RiemannianMetric to directly leverage mathlib
• implement Lorentzian metric as Pseudo-Riemannian metric of index/negative dimentions 1
• added minimal interaction lemmas

[or4nge19]

I think the PR is ready for review after fixing lints and splitting it into, say, 3 parts (most of it is a refactor, though with substantial additions to the existing API in light of mathlib recent developments).