High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1NormalizedRootEllipsoidGeometry

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

Exact-root geometry for the C1 consumer

The normalized-root coordinate map sends an adapted physical ellipsoid to the Euclidean quadratic sublevel set at the same intrinsic radius. This isolates the geometry needed by the exact-root corrector telescope from the separately rounded coordinate system used by the finite Lipschitz terminal.

theorem HCPolySupport.HighContrast.Root.matImage_normalizedRoot_inv_ellipsoid_eq {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : matImage (Selection.normalizedRoot (symmPart abar))⁻¹ (ellipsoid abar r) = {y : Vec d | vecNormSq y ≤ r ^ 2}

Pulling an adapted ellipsoid back by the exact normalized root produces the Euclidean quadratic sublevel set at the same intrinsic radius.