High-contrast homogenization: Provider.Regularity.RoundedSymmetricReferenceBounds

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

Near-identity bounds for the rounded symmetric reference

The canonical alignment kZero d = d + 5 makes the entrywise rounding error strictly smaller than the coarse 1 / 101 estimate used for grid positivity. This sharper slack controls the two inverse-grid factors in the transformed constant symmetric reference and yields the source's literal one-percent Loewner sandwich.

theorem HCPolySupport.HighContrast.norm_baseRoundedGrid_sub_normalizedRoot_le {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : ‖baseRoundedGrid m - Selection.normalizedRoot m‖ ≤ 1 / 400

At the canonical rounded generation, the normalized-root error is below one four-hundredth in operator norm.

theorem HCPolySupport.HighContrast.norm_baseRoundedReference_sub_one_le {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : ‖(baseRoundedGrid m)⁻¹ * specBound m⁻¹ • m * matTranspose (baseRoundedGrid m)⁻¹ - 1‖ ≤ 1 / 100

The scalar-normalized symmetric reference, pulled back by the base rounded grid, differs from the identity by at most one percent in operator norm.

theorem HCPolySupport.HighContrast.norm_roundedSymmetricReferenceCoefficient_sub_one_le {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) : ‖roundedSymmetricReferenceCoefficient abar hS y - 1‖ ≤ 1 / 100

Pointwise operator-norm form of the rounded reference estimate.

theorem HCPolySupport.HighContrast.roundedSymmetricReferenceCoefficient_order_bounds {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) : (99 / 100) • 1 ≤ roundedSymmetricReferenceCoefficient abar hS y ∧ roundedSymmetricReferenceCoefficient abar hS y ≤ (101 / 100) • 1

The source's literal 99/100--101/100 matrix-order sandwich for the constant symmetric reference in rounded coordinates.