High-contrast homogenization: Provider.PolynomialHomogenization.Root.Duality.CdualUnconditional

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

Cdual at the gauge witness, from consumer-supplied data only

Both exports below fix the constant before the comparison matrix, the cube index, the translation, the domain and the order: Cdual depends on the dimension alone, through the cube Calderón--Zygmund constant. That is the uniformity the frozen clause needs, since its C₀ is fixed before U.

Every hypothesis is supplied by the consumer surface: the geometry, the order, the gauge coefficient and the flux-defect L² membership come from the frozen clause's binder surface, and the two PDE hypotheses of the printed lemma — u − v ∈ H₀^{1−s}(U) and ∇·(a∇u − a₁∇v) = 0 — are taken at the physical domain, exactly as ScheduledLocalizationRowSupply states them, and transported to the gauge image here. Every analytic input is proved.

theorem HCPolySupport.HighContrast.RowSupply.exists_printFaithfulDomainFluxDefectDuality_gaugeWitness (d : ℕ) [NeZero d] : ∃ (Cdual : ℝ), 0 ≤ Cdual ∧ ∀ {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (zc : Vec d) (m : ℤ) {Uphys Uhat : Set (Vec d)}, Uphys = (fun (x : Vec d) => zc + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d m) → Uhat = matImage (matSqrt (symmPart abar))⁻¹ Uphys → ∀ {s : ℝ}, 0 < s → s < 1 / 2 → ∀ (aPhysical : CoeffField d) (u h : H1Function Uphys) (uHat hHat : H1Function Uhat), (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 Uphys h u → IsWeakSolutionOn aPhysical Uphys u.grad → IsWeakSolutionOn (fun (x : Vec d) => abar) Uphys h.grad → ∀ {aHat : CoeffField d}, (aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (x : Vec d) => aPhysical x - skewPart abar) → (MemVectorL2 Uhat fun (y : Vec d) => matVecMul (aHat y - 1) (uHat.grad y)) → PrintFaithfulDomainFluxDefectDuality Uhat s aHat uHat hHat Cdual

The printed two-row duality at the gauge witness. Cdual is fixed before the comparison matrix, the domain and the order; the two PDE premises are consumed at the physical domain and transported here.