High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.WitnessZeroTraceAtCube

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

Gate R3, core: the witness zero-trace difference, at the gauge cube

DirichletForcedCubeSolution needs a zeroTraceDifference at the triadic cube, while the frozen clause states it as MemH1a0 on the physical domain (168:45-47). Every link of the transport is and public —

• memH1a0_affinePullback (HCPoly.Analytic.AffineH1a0) — the matrix gauge;
• matImage_inv_affineImage — the gauge image is a translate of the cube;
• exists_h10Function_of_memH1a0 (HCPoly.Analytic.H1a0ToH10) — the H¹₀ realization, with literal field equalities;
• H10Function.untranslate (CoarseGraining) — the translation half —

but no declaration composes them: every existing affine lemma is either pure-matrix (matImage L⁻¹) or pure-translation (translateSet z). This file supplies the composite.

theorem HCPolySupport.HighContrast.EnergyPrice.exists_h10Function_gaugeCube_of_memH1a0 {d : ℕ} [NeZero d] {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hUmeas : MeasurableSet U) (hUfin : MeasureTheory.volume U ≠ ⊤) {b : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {lamG LamG : ℝ} (hlamG : 0 < lamG) (hellG : ∀ᵐ (x : Vec d), IsEllipticMatrix lamG LamG (affineCoefficient L hL b x)) {Q : TriadicCube d} {c : Vec d} (hgauge : matImage L⁻¹ U = translateSet c (openCubeSet Q)) (hconv : IsOpenBoundedConvexDomain (translateSet c (openCubeSet Q))) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemH1a0 b U u Du) : ∃ (w : H10Function (openCubeSet Q)), (∀ (y : Vec d), w.toFun y = u (matVecMul L (y + c))) ∧ ∀ (y : Vec d), w.grad y = matVecMul (matTranspose L) (Du (matVecMul L (y + c)))

Gate R3, core. The physical MemH1a0 zero-trace datum of the frozen clause becomes an honest H¹₀ function on the gauge triadic cube, with its value and gradient given by the gauge-and-translate pullback.

def HCPolySupport.HighContrast.EnergyPrice.witnessDirichletForcedCubeSolution {d : ℕ} {Q : TriadicCube d} {aFam : Book.Ch03.CoeffFamily d} (uObs gObs : H1Function (Book.Ch02.cubeDomain Q).carrier) (hforced : Book.Ch03.IsForcedEquation Q aFam uObs 0) (hzero : ∃ (w : H10Function (Book.Ch02.cubeDomain Q).carrier), w.toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain Q).carrier] fun (x : Vec d) => uObs.toFun x - gObs.toFun x) : Book.Ch03.DirichletForcedCubeSolution Q aFam 0

Gate R3, packaged. Given the four pieces, the witness Dirichlet cube solution exists with its toH1 the prescribed (pulled-back) solution and its boundaryData the prescribed (pulled-back) datum — the combination no constructor provides.

Equations

• HCPolySupport.HighContrast.EnergyPrice.witnessDirichletForcedCubeSolution uObs gObs hforced hzero = { toH1 := uObs, boundaryData := gObs, weakSolution := hforced, zeroTraceDifference := hzero }