High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.CdualGaugeWitnessTerminal

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

Cdual at the gauge witness, from the cube projection stability

The consumer instantiates the printed duality at the gauge image Uhat = matImage (matSqrt (symmPart abar))⁻¹ Uphys with the gauge-transformed coefficient, whose constant reference is the identity. Under the frozen adapted-cell premise the gauge image is a triadic cube translated by an arbitrary real vector, so the whole clause reduces — by translation invariance and duality — to the positive H^s stability of the zero-trace gradient projection on that cube, at

Cdual = 2 * Cproj + 1,

law-free in the sample and in the comparison matrix.

theorem HCPolySupport.HighContrast.RowSupply.hodgeHypothesis_translateSet_identity {d : ℕ} (z : Vec d) (S : Set (Vec d)) {s C : ℝ} (hbase : ∀ (w F : Vec d → Vec d), MemVectorL2 S F → IsPotentialZeroTraceOn S w → (IsSolenoidalOn S fun (y : Vec d) => w y + F y) → negSobolevNorm S s w ≤ ENNReal.ofReal C * negSobolevNorm S s F) (w F : Vec d → Vec d) : MemVectorL2 (translateSet z S) F → IsPotentialZeroTraceOn (translateSet z S) w → (IsSolenoidalOn (translateSet z S) fun (y : Vec d) => w y + F y) → negSobolevNorm (translateSet z S) s w ≤ ENNReal.ofReal C * negSobolevNorm (translateSet z S) s F

The identity-reference Hodge hypothesis moves off an arbitrary translation.

theorem HCPolySupport.HighContrast.RowSupply.printFaithfulDomainFluxDefectDuality_of_cubeProjection_of_potential {d : ℕ} [NeZero d] {L : Mat d} (hL : IsUnit (Matrix.det L)) (zc : Vec d) (Q : TriadicCube d) {Uphys Uhat : Set (Vec d)} (hUphys : Uphys = (fun (x : Vec d) => zc + matVecMul L x) '' openCubeSet Q) (hUhat : Uhat = matImage L⁻¹ Uphys) {s Cproj : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hproj : CubeGradientProjectionHsStability d Q s Cproj) (aHat : CoeffField d) (u h : H1Function Uhat) (hFdefect : MemVectorL2 Uhat fun (x : Vec d) => matVecMul (aHat x - 1) (u.grad x)) (hpot : IsPotentialZeroTraceOn Uhat fun (x : Vec d) => u.grad x - h.grad x) (hsol : IsSolenoidalOn Uhat fun (x : Vec d) => matVecMul (aHat x) (u.grad x) - h.grad x) : PrintFaithfulDomainFluxDefectDuality Uhat s aHat u h (2 * Cproj + 1)

The printed two-row duality at the gauge witness, conditional only on the positive H^s stability of the zero-trace gradient projection on the cube. The reference matrix in the gauge coordinates is the identity, so no constant-matrix estimate is involved.