High-contrast homogenization:

Provider.PolynomialHomogenization.PrintOrderNormalizedReferencePowerTail

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

Power tails for an exactly normalized reference coefficient

One global affine-pullback coefficient family supplies every reference cube. A fixed enclosure of the exact normalized root controls every physical row, and a further natural generation shift absorbs the resulting geometric and exponent-gap factor. This version retains the pointwise square-root estimate and the halved decay rate derived inside the qualitative converter.

theorem HCPolySupport.HighContrast.exists_shiftedNormalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s rho kappa delta : ℝ) (S X : CoeffSpace d → ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1) (hrhoGap : rho < 2 * s) (hkappa : 0 < kappa) (hdelta : 0 ≤ delta) (hrow : Quenched.HasAllLaterPhysicalBlockRow rho kappa delta (Book.Ch02.constantBlockMatrix abar) S X a) (hXone : 1 ≤ X a) (hburn : S a ≤ X a) : ∃ (aRef : Book.Ch03.CoeffFamily d) (L : ℕ), (∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) ∧ ScalarIdentityPowerTail aRef s (√delta) (kappa / 2) (3 ^ ↑(Quenched.triadicCeilingIndex (X a) + L))

A physical block row produces one global exactly normalized reference family whose identity weak errors retain the square-root amplitude and the halved row-decay rate above the shifted triadic scale.