High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ExactRootGaugeTerminalAssembly

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

ExactRootGaugeTerminal, assembled

This module inhabits the large-scale C¹ slope approximation's ball terminal at the event-retaining certificate, modulo a single named analytic hypothesis, ExactRootBallTriangle — the weighted-energy triangle inequality on the exact-root pullback ball. Everything else is discharged:

• the row's certificate is read off the root certificate at the consumer's own corrector smallness (exists_rowCertificate_of_rootGoodScaleAt), so the five-ceiling reconciliation gains no sixth constraint; the scale the rebasing costs is absorbed by the terminal's own free delay L;
• the terminal's carrier is the row's carrier (rootJointCarrier_eq_rowCarrier), and the gauge-pullback clause is then definitional (pushforwardMarker_gaugePullback);
• the far branch is the cube row packaged between two volume-ratio comparisons (farBranch_estimate);
• the near band is the ball-to-ball comparison, the triangle, and the corrector's own energy against the solution's (nearBranch_estimate);
• when the whole radius range lies in the near band — which happens exactly when 108 √d · rStart > R, and then no triadic cube of the row is available at all — the terminal closes at eRef := 0 with no triangle inequality, because the corrector at slope 0 is trivial.

ExactRootBallTriangle is Minkowski for ‖s^{1/2} ·‖_{L_underlined²(V)}, stated for the exact pair of square-integrable fields the terminal compares. The repository proves it only for H1Functions on triadic cubes (weightedGradNorm_sub_le_add_sub_h1), never on a general set; the domain-generic ingredients that would discharge it (sqrt_normalizedLocalSymmetricEnergy_add_le, ofReal_normalizedLocalSymmetricEnergy_eq_weightedGradNorm_sq, both stated for an arbitrary U : Set (Vec d)) need one IsEllipticFieldOn witness and two MemVectorL2 witnesses on the ball that this module did not build.

def HCPolySupport.HighContrast.CorrectorComposition.ExactRootBallTriangle (d : ℕ) [NeZero d] : Prop

The one analytic ingredient not discharged here: the weighted-energy triangle inequality on the exact-root pullback ball, for the two fields the terminal actually compares — the exact-root pullback of an MemH1a solution gradient, and an affine-plus-corrector field of a joint local equation. Both are square-integrable on the ball, which is exactly what makes the statement true; it is Minkowski for ‖s^{1/2} ·‖_{L_underlined²(V)}.

The membership premises are deliberately part of the statement. The unrestricted triangle inequality over arbitrary fields is false: lintegral is the lower integral, so for a Bernstein set S (inner measure 0 on both S and Sᶜ) the pair F = 1_S • v, G = -1_{Sᶜ} • v has weightedGradNorm _ _ F = weightedGradNorm _ _ G = 0 while F - G = v. Stating the hypothesis over arbitrary fields would therefore make every theorem depending on it vacuous.

Equations

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

theorem HCPolySupport.HighContrast.CorrectorComposition.degenerate_le_nearBranchConstant {d : ℕ} [NeZero d] {B Aslope : ℝ} (hB : 0 < B) (hAslope : 0 < Aslope) : ((216 * √↑d) ^ d) ^ (1 / 2) * (108 * √↑d) ≤ nearBranchConstant d B Aslope

The degenerate-case constant is below the near-band constant.

The terminal

theorem HCPolySupport.HighContrast.CorrectorComposition.exactRootGaugeTerminal_onReconciled_of_ballTriangle (d : ℕ) [NeZero d] (htri : ExactRootBallTriangle d) (cStar : ℝ → ℝ) {g : ℝ} (hg : g ∈ Set.Ico 0 1) (hcStar : 0 < cStar g) {κc : ℝ} (hκc : 0 < κc) {eta : ℝ} (heta : eta ∈ Set.Ioo 0 1) : ExactRootGaugeTerminal d (reconciledRootGoodScaleOn d cStar g κc) (Root.RootPushCorrectorFamilyPredicate d) eta

The exact-root gauge ball terminal at the event-retaining certificate, modulo the weighted-energy triangle inequality on the ball.