High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationHarmonicComparison

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.

noncomputable def HCPolySupport.HighContrast.inverseAffinePrimalLoad {d : ℕ} (q : Mat d) (X : BlockVec d) : BlockVec d

Affine primal-load transform applying the inverse transpose of q to the first component and q to the second.

Equations

• HCPolySupport.HighContrast.inverseAffinePrimalLoad q X = (HCPolySupport.matVecMul (HCPolySupport.matTranspose q)⁻¹ X.1, HCPolySupport.matVecMul q X.2)

noncomputable def HCPolySupport.HighContrast.inverseAffineDualLoad {d : ℕ} (q : Mat d) (X : BlockVec d) : BlockVec d

Affine dual-load transform applying q to the first component and its inverse transpose to the second.

Equations

• HCPolySupport.HighContrast.inverseAffineDualLoad q X = (HCPolySupport.matVecMul q X.1, HCPolySupport.matVecMul (HCPolySupport.matTranspose q)⁻¹ X.2)

noncomputable def HCPolySupport.HighContrast.inverseCenteredPrimalLoad {d : ℕ} (abar : Mat d) (P : BlockVec d) : BlockVec d

Primal load obtained by spectral rescaling and restoration of the skew-centering contribution.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.inverseCenteredDualLoad {d : ℕ} (abar : Mat d) (Q : BlockVec d) : BlockVec d

Dual load obtained by rescaling its second component and restoring the skew contribution in the first.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.baseRoundedPhysicalResponseValueSet {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (a : CoeffSpace d) (abar : Mat d) (k : ℤ) (w : Fin d → ℤ) : Set ℝ

Physical response values on an adapted cell for primal and dual loads corresponding to the same unit full-block vector.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.homogenizationErrorOnCube_eq_roundedGenerationSpatialWeakError {d : ℕ} [NeZero d] {geom : RoundedGenerationAnalyticGeometry d} (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d) (hRounded : ∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) (s : ℝ) (m : ℤ) : Book.Ch02.HomogenizationErrorOnCube (originCube d m) s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) aRounded (geom.referenceMatrix abar hS) = geom.spatialWeakError a abar hS s m

The standard Chapter 2 homogenization error of the exact rounded coefficient family is the physical rounded weak-error row. This public bridge exposes the identity already used internally by the rounded harmonic comparison, without changing either response family.

theorem HCPolySupport.HighContrast.exists_roundedGenerationHarmonicComparisonSpecializationConstant (d : ℕ) [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (s Cdual : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (hCdual : 0 ≤ Cdual) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d), (∀ (R : TriadicCube d), (aRounded.coeffOn R).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) → ∀ (m : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsWeakSolutionOn (aRounded.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad), (∀ {w F : Vec d → Vec d}, MemVectorL2 (cubeSet (originCube d m)) F → IsPotentialZeroTraceOn (cubeSet (originCube d m)) w → (IsSolenoidalOn (cubeSet (originCube d m)) fun (x : Vec d) => matVecMul (geom.referenceMatrix abar hS) (w x) + F x) → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s fun (x : Vec d) => matVecMul (geom.referenceMatrix abar hS) (w x)) ≤ Cdual * cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s F ∧ (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s fun (x : Vec d) => matVecMul (geom.referenceMatrix abar hS) (w x) + F x) ≤ Cdual * cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s F) → have W := geom.harmonicReplacementDatum abar hS aRounded m u hu; have E := geom.spatialWeakError a abar hS s m; have A := Book.Ch03.h1EnergyNormOnCube (originCube d m) aRounded u; (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s fun (x : Vec d) => u.grad x - W.v.grad x) ≤ C * E * A ∧ cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) s (Book.Ch03.homogenizationComparisonFluxField (originCube d m) aRounded (geom.referenceConstantCoeffMatrix abar hS) 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

The printed finite response recurrence, specialized to the rounded harmonic replacement and closed by the genuine-dual comparison.