High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitNssEnvelope

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

The burn-split pathwise envelope in normalized-source form

The mesoscale (burn-split) adapted-cell ceiling, converted to the normalized-source-scale form the abstract single-cell variance consumes: at window top k + D the ceiling is the dimensional constant 2 times NSS_{S'}(k+D-1)^g — no boundary constant, no grid-norm power. This is the print's frame discipline (the printed argument): the geometry is absorbed into the burn depth D, which rides only in scale thresholds.

theorem HCPolySupport.HighContrast.Quenched.coarseBlock_adaptedCell_burnsplit_nss {d : ℕ} (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} (hE : Book.Ch02.BlockPosDef E) {Sh : CoeffSpace d → ℝ} {D : ℕ} (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), Sh a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑D - ↑k) 0)) E)) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) (hD : boundaryConst Cd g n ≤ 3 ^ D) (k : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, adaptedCell (roundedGrid l n) k ⊆ centeredCube d (k + ↑D) → BlockMatLoewnerLE (coarseBlock (adaptedCell (roundedGrid l n) k) a) (blockScale (2 * normalizedSourceScale Sh (k + ↑D - 1) a ^ g) E)

The burn-split pathwise envelope, normalized-source form.