High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitCarriers

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

The carriers of the burn split: depth, anchor, window

The burn-split envelope needs a depth D doing three things at once: absorbing the boundary constant (HC (2.123)), covering the canonical grid enlargement so the aligned-cell containment is inherited, and being the height of a coupled window so the mesoscale envelope is available at depth 2D.

All three are met by one choice, D = canonicalGridEnlargement d (C_d Π ζ_g), with the window anchored at the burn scale built the way coupledExecBurn builds its own — the ceiling that makes the coupling inequality true by construction. The anchor is a function of (d, g, Π, K, C_d) alone, so the window threshold that the source scale inherits is a delay and not a generation.

noncomputable def HCPolySupport.HighContrast.Quenched.burnSplitDepth (d : ℕ) (Cd g Pi : ℝ) : ℕ

The burn depth: the grid enlargement built from the boundary constant's own aspect ratio.

Equations

• HCPolySupport.HighContrast.Quenched.burnSplitDepth d Cd g Pi = HCPolySupport.HighContrast.Quenched.canonicalGridEnlargement d (Cd * Pi * HCPolySupport.HighContrast.zetaG g)

noncomputable def HCPolySupport.HighContrast.Quenched.burnSplitAnchor (d : ℕ) (Q K : ℝ) (D : ℕ) : ℤ

The burn anchor, built as coupledExecBurn builds its own: the ceiling that makes the coupling inequality true at height 2D.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.boundaryConst_le_three_pow_burnSplitDepth {d : ℕ} (hd : 2 ≤ d) {Cd g : ℝ} (hCd : 1 ≤ Cd) (hg : g ∈ Set.Ico 0 1) {mAl : Mat d} {Pi : ℝ} (hPi : 1 ≤ Pi) (hecc : witnessEccentricity mAl ≤ Pi) : boundaryConst Cd g mAl ≤ 3 ^ burnSplitDepth d Cd g Pi

The depth absorbs the boundary constant. The Lean form of HC (2.123) at this choice of depth.

theorem HCPolySupport.HighContrast.Quenched.succ_canonicalGridEnlargement_le_burnSplitDepth {d : ℕ} (hd : 2 ≤ d) {Cd g : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) (hg : g ∈ Set.Ico 0 1) {Pi : ℝ} (hPi : 1 ≤ Pi) : canonicalGridEnlargement d Pi + 1 ≤ burnSplitDepth d Cd g Pi

The depth covers the grid enlargement, with a generation to spare. So an aligned-cell containment stated at t + G + 1 is inherited at t + D.

theorem HCPolySupport.HighContrast.Quenched.isCoupledWindow_burnSplitAnchor {d : ℕ} (hd : 2 ≤ d) {Q K : ℝ} {D : ℕ} (hD : 1 ≤ D) : IsCoupledWindow d Q K (burnSplitAnchor d Q K D) (burnSplitAnchor d Q K D + ↑(2 * D))

The window at the burn depth is coupled. The anchor is built by the same ceiling that coupledExecBurn uses, so the coupling inequality holds by construction.