Coarse-graining support:

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletCorrectedWeakFluxAveraged

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

Corrected zero-Dirichlet weak-flux apex with averaged corrector energy

This leaf consumes the proved averaged Neumann-corrector energy estimate in the corrected zero-Dirichlet weak-flux route. It removes the exposed hcorr/hcorrectorBudget arguments from the previous component theorem and constructs the descendant harmonic-remainder selector inside the apex.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.negativeBesovSeminormTwo_matVecMul_grad_le_const_mul_weakFluxCorrectionBound {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a g) (C s : ℝ) {Bcorr lam Lam : ℝ} (hC_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (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)) (z : TriadicCube d → Vec d → Vec d) (hzdecomp : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w0 : AHarmonicFunction a (cubeSet R)), (z R = fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ∧ ∀ x ∈ cubeSet R, ρ.toH10.grad x = w0.toH1.grad x + z R x) (hcorr : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s k * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s k ≤ Bcorr) (hcorrectorForceBudget : Bcorr * (1 - Real.rpow 3 (-s))⁻¹ ≤ 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) (hC_sq : 32500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 + 2500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ C ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (ρ.toH10.grad x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

The corrected weak-flux component with the averaged corrector-energy force budget inserted directly.

This is the scalar repair that avoids the false comparison lambda^{-1} <= Lambda: the coefficient-energy component is bounded by the proved weak-flux energy compact scale, and the corrector-energy component is bounded by its own proved Lambda * lambda^{-1} force scale.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.negativeBesovSeminormTwo_fluxDefect_le_two_mul_const_mul_of_fluxRHSBound {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q a g) (a0 : Mat d) (s : ℝ) (gradU : Vec d → Vec d) (w : AHarmonicFunction a (cubeSet Q)) {lam Lam lam0 Lam0 : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hgrad : ∀ x ∈ cubeSet Q, gradU x = w.toH1.grad x + ρ.toH10.grad x) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hresponseSum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * zeroTraceFluxApexConstant d s * coarseFluxResponseRHSBound Q a a0 s gradU g

Zero-Dirichlet one-cube RHS apex with the weak-flux component routed directly through the proved averaged corrector-energy budget. The theorem no longer exposes Bcorr, hcorr, hcorrectorBudget, or the invalid lambda^{-1} <= Lambda comparison, and it constructs the descendant omega/w0 harmonic-remainder decomposition internally.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.besovFluxDefect_le_constant_mul_bound {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam lam0 Lam0 : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hg : CubeVectorBesovHRegularity Q s g) (hresponseSum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 v.grad) ≤ 2 * zeroTraceFluxApexConstant d s * coarseFluxResponseRHSBound Q a a0 s v.grad g

PDE-facing corrected one-cube RHS apex with the zero-trace corrector and harmonic split constructed internally, consuming the note-facing H^s regularity package for the right-hand side.