High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.InnerEllipsoidNormalization

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

The inner-ellipsoid normalization premise

The Dirichlet conjunct already bounds the domain above by its adapted ellipsoid. This file studies the effect of bounding it below by a concentric adapted ellipsoid of an explicit dimensional radius.

Two facts are proved. First, the class of domains satisfying both bounds is non-empty at every dimension and every comparison matrix: an adapted cell of a suitable generation fits between the two ellipsoids, so the proposed premise is not vacuous. Second, the lower bound forces the absolute gauge scale to be majorized by the outer sandwich radius, which is exactly the majorization a cell-anchored response rate needs in order to expose only the frozen outer data.

The absorption: the inner ellipsoid majorizes the gauge scale

theorem HCPolySupport.HighContrast.RowSupply.normalizedRootScale_mul_le_of_innerEllipsoid {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {c rho Rad : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hc : 0 ≤ c) (hInner : ellipsoid abar c ⊆ U) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : √(specBound (symmPart abar)⁻¹) * c ≤ Rad

A concentric adapted ellipsoid inside the domain forces the absolute gauge scale, times the ellipsoid's radius, below the outer sandwich radius of the gauge domain. This is the exact inequality that removes the absolute reference scale from a cell-anchored response constant.

Non-vacuity: an adapted cell fits between the two ellipsoids

The rate consequence at the shape the consumer reads