Coarse-graining support:

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletBVForce

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Centered-force averaged BV localization for the zero-Dirichlet RHS apex

This leaf proves the raw averaged localization estimate for the centered-force part of the harmonic-remainder BV budget. It deliberately stops at the natural s^{-2} * lambda^{-1} scale; converting this into the corrected weak-flux compact scale is a separate coefficient-normalization step.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletHarmonicRemainderCenteredForceAverage_le_raw_lambdaInv {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (j : ℕ) : (coarsePoincareRHSDepthWeight s j * descendantsAverage Q j fun (R : TriadicCube d) => 250 * s⁻¹ ^ 2 * (lambdaSq R (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * cubeBesovPositiveVectorSeminormTwo R s fun (x : Vec d) => g x - cubeAverageVec R g)) ^ 2) ≤ 250 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Raw averaged control of the centered-force part of the harmonic-remainder BV budget.

This proves the analytic localization step before any enlargement to the corrected weak-flux compact scale. The natural output has s^{-2} * lambda^{-1} units.