High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentityHarmonicComparison

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

Common-scale rounded harmonic comparison

The physical rounded response row is first identified exactly with the canonical response row of the rounded coefficient and rounded constant matrix. The finite q = 2 recurrence then feeds the already selected common-scale dual comparison without changing the printed order or scale normalization.

theorem HCPolySupport.HighContrast.exists_identityHarmonicComparisonConstant (d : ℕ) [NeZero d] (g Cdual : ℝ) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderIdentityCubeDualRegularityWithConstant d g Cdual) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : Book.Ch03.CoeffFamily d) (m : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad), have W := identityHarmonicReplacementDatum a m u hu; have E := scalarIdentityWeakError a (printCertificateOrder g) m; have A := Book.Ch03.h1EnergyNormOnCube (originCube d m) a u; (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) (printCertificateOrder g) fun (x : Vec d) => u.grad x - W.v.grad x) ≤ C * E * A ∧ cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) (printCertificateOrder g) (Book.Ch03.homogenizationComparisonFluxField (originCube d m) a (identityConstantCoeffMatrix d) u W.v) ≤ C * E * A ∧ (cubeBesovScaleWeight 1 (originCube d m) * cubeLpNorm (originCube d (m - 1)) 2 fun (x : Vec d) => u.toFun x - W.v.toFun x) ≤ C * E * A

In the exact gauge frame the printed finite response recurrence closes directly against the identity dual regularity theorem. No rounded reference, generation, or tolerance occurs in the statement.