High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.BoundaryEnergyFiniteness

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

(ε): the boundary-energy finiteness transport

Tabulating the module against the restated Dirichlet clause exposes one premise not named elsewhere. The hBoundaryTop premise asks for boundaryEnergy ≠ ⊤, and the energy price from the modules named above instantiates boundaryEnergy at the gauge-conjugated boundary datum

hsNormSq U s₀ (fun y ↦ matVecMul (matSqrt (symmPart abar)) (g₀.grad y)),

while the hole supplies finiteness for the unconjugated one, hsNormSq U s₀ g₀.grad ≠ ⊤.

The transport is the pointwise matrix action hsNormSq_matVecMul_le (HCPoly.Analytic.AffineFractionalNorm), whose cost is the squared operator norm — finite, so it moves finiteness across with nothing to pay. No hypothesis on abar, the domain or the order is needed.

theorem HCPolySupport.HighContrast.RowSupply.hsNormSq_matSqrt_symmPart_ne_top {d : ℕ} (abar : Mat d) {U : Set (Vec d)} {s : ℝ} {G : Vec d → Vec d} (hG : hsNormSq U s G ≠ ⊤) : (hsNormSq U s fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (G y)) ≠ ⊤

(ε). The frozen hole's finiteness premise for the boundary datum transports to the gauge-conjugated boundary energy that the hBoundaryTop premise reads.