High-contrast homogenization: Provider.PolynomialHomogenization.ConvexCubeComparison

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

Identity harmonic replacement on a comparison cube

An H¹ weak solution on an open triadic cube has an identity-coefficient harmonic replacement with the same boundary trace. The replacement is built by solving for its zero-trace correction, so both the second weak equation and the Chapter 3 comparison datum are consequences rather than inputs.

theorem HCPolySupport.HighContrast.exists_identityCoarseGrainingComparisonDatum_of_hcWeakSolution {d : ℕ} {Q : TriadicCube d} {a : Book.Ch03.CoeffFamily d} (u : H1Function (Book.Ch02.cubeDomain Q).carrier) (hu : IsWeakSolutionOn (a.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.grad) : ∃ (W : Book.Ch03.CoarseGrainingComparisonDatum Q a (identityConstantCoeffMatrix d) 0), W.u = u

A high-contrast weak solution on a compatible Chapter 3 cube family admits an identity-coefficient, zero-force comparison datum on that same cube.