High-contrast homogenization: Provider.Window.ScaledStandardToAdapted

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

The scale-adapted standard-to-adapted bridge

The standard-to-adapted bridge carries a uniform standard envelope Y · burnDiscount to the adapted cell at the same burn base as the grid. The per-generation caps need the scale-adapted variant: when every standard subcell of scale k obeys the envelope Y · 3^{g(r−k)} (as the Dagger coarse bound provides at any burn scale, relative to the adapted cell's own scale r), the adapted cell obeys boundaryConst · Y — the Whitney rows lose 3^{-u} in volume and gain only 3^{gu} in envelope, so the same geometric series ζ_g closes with no burn factor at all.

theorem HCPolySupport.HighContrast.Window.adapted_scaled_of_standard {d : ℕ} (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {jStar : ℤ} (hj : ↑(kZero d) ≤ jStar) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) {a : CoeffSpace d} {E : BlockMat d} (hE : Book.Ch02.BlockPosDef E) {Y : ℝ} (hY : 0 ≤ Y) (r : ℤ) (y : Vec d) (hstandard : ∀ (k : ℤ) (w : Fin d → ℤ), standardCell d k w ⊆ adaptedCellTranslate (roundedGrid jStar n) r y → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (Y * 3 ^ (g * (↑r - ↑k))) E)) : BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (roundedGrid jStar n) r y) a) (blockScale (boundaryConst Cd g n * Y) E)

The scale-adapted Whitney bridge. Simultaneous standard-cell bounds with the scale-adapted envelope Y·3^{g(r−k)} imply the adapted-cell bound boundaryConst·Y, with no burn factor.