Coarse-graining support: Support.Book.Ch03.Theorems.EnergyRHS.HarmonicRemainderSplit

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

Energy RHS: harmonic remainder split wrappers

This file contains the terminal wrappers which turn the Dirichlet decomposition into the zero-trace hypothesis required by the harmonic-remainder estimate.

Audit tag

Claim: the manuscript Dirichlet split supplies the zero-trace boundary difference, and hence the public harmonic-remainder estimate needed by the Dirichlet energy assembly.

Downstream target: EnergyRHS/Theory.lean. This file is endpoint assembly only and introduces no public *Theory package.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_sqrt_two_energy_le_of_zeroTrace {d : ℕ} [NeZero d] {C : ℝ} (hC_absorb : √2 * (1 + ↑d * Real.rpow 3 (↑d + 1)) * (↑d * √5) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hzero : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.toH1.grad x - dirichletBoundaryGradientField v x) : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Direct public harmonic-remainder estimate from the zero-trace boundary condition. This combines weak testing, public Besov duality, and the finite-depth homogeneous flux Poincare wrapper.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_zeroTrace_boundaryDifference_of_split {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hgrad : v.toH1.grad =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] fun (x : Vec d) => ρ.toH10.grad x + w.toH1.grad x) : IsPotentialZeroTraceOn (cubeSet Q) fun (x : Vec d) => w.toH1.grad x - dirichletBoundaryGradientField v x

The Dirichlet decomposition supplies the zero-trace boundary condition needed by the homogeneous harmonic-remainder estimate. Indeed w - h = (v - h) - ρ at the gradient level on the cube, and both terms on the right have zero trace.

theorem HCPolySupport.Book.Ch03.dirichletHarmonicRemainder_sqrt_two_energy_le_of_split {d : ℕ} [NeZero d] {C : ℝ} (hC_absorb : √2 * (1 + ↑d * Real.rpow 3 (↑d + 1)) * (↑d * √5) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (w : AHarmonicFunction (publicCoeffField Q a) (cubeSet Q)) (hs : 0 < s) (hs_le : s ≤ 1) (hboundary : ForceBesovRegularity Q s (dirichletBoundaryGradientField v)) (hgrad : v.toH1.grad =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] fun (x : Vec d) => ρ.toH10.grad x + w.toH1.grad x) : √(2 * cubeAverage Q (coefficientEnergyDensity (publicCoeffField Q a) fun (x : Vec d) => w.toH1.grad x)) ≤ C * s.rpow (-(1 / 2)) * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) * scaleNormalizedPositiveBesovVectorNormTwo Q s (dirichletBoundaryGradientField v)

Harmonic-remainder estimate in the exact shape needed by the public Dirichlet energy assembly. The zero-trace condition is derived from the manuscript split rather than passed as an extra public hypothesis.