High-contrast homogenization: Provider.PolynomialHomogenization.AffineChapter3Comparison

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

Chapter 3 comparison data from weak solutions

On an open cube, the smooth compact-test weak equation upgrades to the full zero-trace weak equation once the coefficient flux is known to lie in L². This constructs the deterministic Chapter 3 comparison datum directly from the high-contrast weak-solution predicate.

The zero-trace difference below is deliberately cube-local. A zero-trace difference on a larger domain does not in general remain zero trace after restriction to an interior cube.

theorem HCPolySupport.HighContrast.forceBesovRegularity_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : Book.Ch03.ForceBesovRegularity Q s 0

The zero vector field satisfies every Chapter 3 force-regularity exponent.

theorem HCPolySupport.HighContrast.coarseGrainingComparisonDatum_zero_of_hcWeakSolutions {d : ℕ} {Q : TriadicCube d} {a : Book.Ch03.CoeffFamily d} {a0 : Book.Ch03.ConstantCoeffMatrix d} (u v : H1Function (Book.Ch02.cubeDomain Q).carrier) (hu : IsWeakSolutionOn (a.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.grad) (hv : IsWeakSolutionOn (constantCoeffField a0.matrix) (Book.Ch02.cubeDomain Q).carrier v.grad) (w : H10Function (Book.Ch02.cubeDomain Q).carrier) (hw : w.toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain Q).carrier] fun (x : Vec d) => u.toFun x - v.toFun x) : ∃ (W : Book.Ch03.CoarseGrainingComparisonDatum Q a a0 0), W.u = u ∧ W.v = v

Two high-contrast weak solutions on the same open cube, with an actual cube-level zero-trace difference, form the zero-force Chapter 3 comparison datum.