ClassificationScaling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transport the exact metric classification across the classical constant-rescaling identity for Riemannian distance.

theorem OAI.PositiveEinsteinFour.scaledEDistance_mul line 18
theorem OAI.PositiveEinsteinFour.classified_of_constant_scaling line 27
Source documentation
A normalization step needs only its ordinary distance-scaling law; the final model and positive scale are then transported by this theorem.
```
theorem classified_of_constant_scaling (g h : SmoothMetric M) (c : ℝ) (hc : 0 < c)
    (hd : ∀ x y, scaledEDistance h 1 x y = scaledEDistance g c x y)
    (hh : Classified h) : Classified g := by
…
```
Mentions: OAI.PositiveEinsteinFour.Classified