High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.PhysicalFrameTransport

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

The physical-frame pair from the gauge pair

The frozen Dirichlet conjunct is written in the physical frame, at the L-conjugated pair

negSobolevNorm U s (L (∇u − ∇h)) + negSobolevNorm U s (L⁻¹ (a ∇u − ā ∇h))

with L = matSqrt (symmPart abar), while the terminal Seam-2 bound is produced in the gauge frame, on Uhat = matImage L⁻¹ U, at the pair

negSobolevNorm Uhat s (∇û − ∇h_hat) + negSobolevNorm Uhat s (â ∇û − ∇h_hat).

The step between them is the affine dual comparison negSobolevNorm_matImage_le_opNorm (HCPoly.Analytic.AffineNegSobolevNorm) applied twice, with the two pullback identities matSqrt_gradient_difference_affinePullback and skewCenteredFlux_affinePullback (HCPoly.Provider.Regularity.AffineTransfer) identifying the pulled-back physical fields with the gauge fields. This is exactly the Kout half of the anisotropic flux defect, isolated from its descendant-cube context.

The frame factor does not need to be folded. Its constant is √(hsAffineFactor L⁻¹ s ‖L‖), which is precisely the outputFactor that the terminal bound carries on its left-hand side as a free parameter. Instantiated there, the two occurrences are the same term and cancel; no bound on ‖L‖, ‖L⁻¹‖ or the eccentricity is spent here. That is why outputFactor was left free there in the first place.

theorem HCPolySupport.HighContrast.RowSupply.negSobolevPhysicalPair_le_outputFactor_mul_gaugePair {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {Uphys Uhat : Set (Vec d)} (hUhat : Uhat = matImage (matSqrt (symmPart abar))⁻¹ Uphys) (hUmeas : MeasurableSet Uhat) (hU0 : MeasureTheory.volume Uhat ≠ 0) {s : ℝ} (hs : 0 ≤ ↑d + 2 * s) (aPhysical : CoeffField d) (uGrad hGrad : Vec d → Vec d) (uHat hHat : H1Function Uhat) (huHat : uHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (uGrad (matVecMul (matSqrt (symmPart abar)) y))) (hhHat : hHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (hGrad (matVecMul (matSqrt (symmPart abar)) y))) {aHat : CoeffField d} (haHat : aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (z : Vec d) => aPhysical z - skewPart abar) : ((negSobolevNorm Uphys s fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (uGrad y - hGrad y)) + negSobolevNorm Uphys s fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (aPhysical y - skewPart abar) (uGrad y) - matVecMul (symmPart abar) (hGrad y))) ≤ ENNReal.ofReal √(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖) * ((negSobolevNorm Uhat s fun (y : Vec d) => uHat.grad y - hHat.grad y) + negSobolevNorm Uhat s fun (y : Vec d) => matVecMul (aHat y) (uHat.grad y) - hHat.grad y)

The physical pair is the gauge pair at the output factor. Both frozen negative-Sobolev terms transport at the single constant √(hsAffineFactor L⁻¹ s ‖L‖), with no other loss.