High-contrast homogenization: Provider.Regularity.PrintOrderIdentityCubeDualRegularity

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

Identity-coefficient cube dual regularity at the printed order

The identity background is the scalar background at sigma = 1. For a zero-trace potential field w whose sum with an L² datum F is solenoidal on a triadic cube, the printed-order dual negative Besov norms of w and of w + F are controlled by the same norm of F, with a constant depending only on the dimension and on the printed order.

The proof is the duality argument at the printed order. A unit full-dual test in one coordinate is turned into an identity-coefficient Dirichlet datum; the solution's gradient is a positive Besov test with a budget fixed before the cube; the Dirichlet pairing identity moves the test from w to F; and the genuine dual norm of F absorbs it. The printed order is below the trace threshold, which is exactly the range in which the coordinate bridge holds.

theorem HCPolySupport.HighContrast.exists_printOrderIdentityCubeDualRegularityWithConstant (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (Cid : ℝ), PrintOrderIdentityCubeDualRegularityWithConstant d g Cid

Identity-coefficient cube dual regularity at the printed order, with a constant fixed before the cube, the potential field, and the datum.