High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedResponseMax

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

Exact normalized response maximum on adapted cells

Constant-skew removal, scalar normalization, and the exact affine pullback compose with distinct transformed primal and dual loads. The resulting identity-reference cube response is controlled by the physical block excess on the corresponding adapted cell.

theorem HCPolySupport.HighContrast.normalizedBlockResponseMax_le_adaptedCell_blockExcess {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (t k : ℤ) (w : Fin d → ℤ) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) : Book.Ch02.normalizedBlockResponseMax (translateCube w (originCube d k)) aRef 1 ≤ blockExcess (Book.Ch02.coarseBlockMatrix (Response.adaptedDomainAt ⋯ k w) (a.coeffOn (Response.adaptedDomainAt ⋯ k w))) (Book.Ch02.constantBlockMatrix abar)

The identity-reference normalized response on an aligned cube is bounded by the physical block excess on its exact adapted-cell image.