High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessGaugePullback

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

The composed row uHat/hHat/huHat/hhHat

exists_memAffineH10_affinePullback pulls both the boundary datum and the solution back through an invertible matrix, producing gradients fun y ↦ matVecMul (matTranspose L) (·.grad (matVecMul L y)). At L := matSqrt (symmPart abar) the transpose is the matrix itself, because the symmetric square root of a positive definite matrix is Hermitian, so the two gradients land in exactly the huHat premise/hhHat shape.

theorem HCPolySupport.HighContrast.RowSupply.matTranspose_matSqrt_symmPart {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : matTranspose (matSqrt (symmPart abar)) = matSqrt (symmPart abar)

The symmetric square root of a positive definite matrix is its own transpose.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessGaugePullback {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (h u : H1Function U) (haff : MemAffineH10 U h u) : ∃ (uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)) (hHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)), (uHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (u.grad (matVecMul (matSqrt (symmPart abar)) y))) ∧ (hHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (h.grad (matVecMul (matSqrt (symmPart abar)) y))) ∧ MemAffineH10 (matImage (matSqrt (symmPart abar))⁻¹ U) hHat uHat

Row uHat/hHat/huHat/hhHat. The frozen affine boundary pair on the physical witness domain pulls back to the gauge domain with exactly the gradient identities that module requires.