High-contrast homogenization: Provider.Window.BurnSplitStandardToAdapted

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

The burn-split standard-to-adapted bridge

adapted_scaled_of_standard transfers simultaneous standard-cell bounds to an adapted cell and pays boundaryConst Cd g n for the transfer, because it applies the eccentricity-carrying Whitney row estimate to every row — including the top one, where the sharp estimate is the partition property.

The printed conversion (Lemma 2.13 of HC, whose conclusion is (2.124)) does not pay that. It splits the Whitney rows at the burn depth D: on the band u ≤ D the hypothesis envelope is flat, so those rows are covered by the total row weight alone, which is at most one; only the rows below the band meet the geometric estimate, and there the envelope's growth 3 ^ (g (u - D)) is beaten by the volume decay 3 ^ (-u), leaving 3 ^ (-D). The geometric constant therefore multiplies 3 ^ (-D) rather than the whole sum, and is absorbed once the depth exceeds log₃ (Cd 𝔢 ζ_g / δ) — HC (2.123), and its stated principle that the aspect ratio enters through a scale restriction and nowhere else.

Everything outside the row accounting is adapted_scaled_of_standard's proof unchanged.

theorem HCPolySupport.HighContrast.Window.adapted_burnsplit_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) (D : ℕ) (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 * max (↑r - ↑k - ↑D) 0)) E)) : BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (roundedGrid jStar n) r y) a) (blockScale ((1 + Cd * witnessEccentricity n * zetaG g * 3 ^ (-↑D)) * Y) E)

The burn-split Whitney bridge. Standard-cell bounds whose envelope is truncated D scales above the adapted cell's own imply the adapted-cell bound with constant 1 + Cd * 𝔢 * ζ_g * 3 ^ (-D): the eccentricity rides on the burn depth instead of multiplying.