High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.FillingCoefficientAbsorption

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

The α half of the witness weak-error transport, absorbed

The translated-cube transport observationHomogenizationError_le_referencePowerTail_fixedParent prices the weak error of a really translated gauge family on a centered cube, with the loss

observationParentConvolutionFactor d s ε abar M K
  = (observationFillingCoefficient d ε abar · geometricDiscount (1-2s) 1 ⁻¹)
      · 3 ^ (2 s (M - K)).

The filling coefficient is exactly max 1 (6 d √d · (ε · α)) with α = √(specBound (symmPart abar)⁻¹) (HCPoly.Provider.PolynomialHomogenization.Root.RowSupply.OuterC0MatrixScaleIdentity), and it is provably unbounded on the bare surface. This file discharges the α factor from the inner-ellipsoid premise together with the outer ball of the consumer's Whitney system, giving

observationFillingCoefficient d ε abar ≤ max 1 (18 d² Rad).

The variant of the absorption proved here takes only 0 ≤ Rad and the outer inclusion — not a full HasBallSandwich — because 0 < rho is not on the frozen clause's binder surface while system.outer_ball and hRad : 0 < Rad are.

theorem HCPolySupport.HighContrast.EnergyPrice.abs_lt_of_vecNormSq_lt {d : ℕ} {x : Vec d} {r : ℝ} (hr : 0 ≤ r) (h : vecNormSq x < r ^ 2) (i : Fin d) : |x i| < r

A coordinate bound from a strict Euclidean bound.

theorem HCPolySupport.HighContrast.EnergyPrice.vecNormSq_single {d : ℕ} (i : Fin d) (t : ℝ) : (vecNormSq fun (k : Fin d) => if k = i then t else 0) = t ^ 2

The Euclidean square of a single-coordinate spike.

theorem HCPolySupport.HighContrast.EnergyPrice.normalizedRootScale_mul_le_of_innerEllipsoid_outerBall {d : ℕ} [NeZero d] {abar : Mat d} {U : Set (Vec d)} {cc : Vec d} {c Rad : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hc : 0 ≤ c) (hRad : 0 ≤ Rad) (hInner : ellipsoid abar c ⊆ U) (hOut : matImage (matSqrt (symmPart abar))⁻¹ U ⊆ euclideanBallAt cc Rad) : √(specBound (symmPart abar)⁻¹) * c ≤ Rad

The absolute gauge scale is bounded by the outer radius alone. A concentric adapted ellipsoid inside the physical domain, together with an outer Euclidean ball for the gauge image, forces α · c ≤ Rad.