High-contrast homogenization: Provider.PolynomialHomogenization.Root.CorrectorDecay.AffineDetBound

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

theorem HCPolySupport.HighContrast.absDet_rpow_two_div_le {d : ℕ} [NeZero d] (L : Mat d) : |Matrix.det L| ^ (2 / ↑d) ≤ (√↑d * ‖L‖) ^ 2

The determinant contribution to affine H¹ distortion is controlled by the Euclidean operator norm with a dimension-only factor.