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

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

Energy RHS: Public theorem package

Audit tag

Claim: expose the single public package for Dirichlet and mean-zero Neumann energy consequences with right-hand side.

Downstream target: InhomogeneousEquationsTheory. The remaining analytic inputs belong in the Dirichlet/Neumann subfiles; this file should stay as the package assembly endpoint.

structure HCPolySupport.Book.Ch03.EnergyConsequencesRHSTheory (d : ℕ) [NeZero d] : Prop

Public theorem package for the Dirichlet and mean-zero Neumann energy consequences with right-hand side.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ (∀ {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (v : DirichletForcedCubeSolution Q a g), 0 < s → s < 1 → ForceBesovRegularity Q s g → ForceBesovRegularity Q s (dirichletBoundaryGradientField v) → dirichletForcedSolutionEnergyNorm Q a v ≤ dirichletEnergyWithRHSRHS C Q a s g v) ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (w : NeumannForcedCubeSolution Q a g), 0 < s → s < 1 → ForceBesovRegularity Q s g → neumannForcedSolutionEnergyNorm Q a w ≤ neumannEnergyWithRHSRHS C Q a s g

theorem HCPolySupport.Book.Ch03.energyConsequencesRHSTheory {d : ℕ} [NeZero d] : EnergyConsequencesRHSTheory d

Final public theorem package for the Dirichlet and mean-zero Neumann energy estimates with right-hand side. The Dirichlet branch follows the manuscript route: zero-trace corrector energy, homogeneous weak testing, Besov duality, homogeneous coarse flux Poincare, and scalar cancellation.