Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.CoarseFluxResponseRHS

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

Public/internal coarse-flux-response RHS bridge

This file contains the terminal dimension-loss comparison for the deterministic coarse-flux-response RHS written with the Chapter 3 public coefficient field.

Audit tag

Claim: the deterministic public-coefficient coarse-flux-response RHS is bounded by the Chapter 3 public RHS after the explicit dimension-square loss.

Downstream target: CoarseFluxResponseRHS.lean through the public PublicInternalBridges import surface. This file is bridge plumbing only and introduces no public *Theory package.

theorem HCPolySupport.Book.Ch03.coarseFluxResponseBound_le_dimSquared_publicRHS {d : ℕ} [NeZero d] (C : ℝ) (Q : TriadicCube d) (a : CoeffFamily d) (a0 : ConstantCoeffMatrix d) {s : ℝ} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) (hC : 0 ≤ C) (hs : 0 < s) (hB_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) (hH_nonneg : 0 ≤ Ch02.HomogenizationErrorOnCube Q s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) a a0.matrix) (herror : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) (publicCoeffField Q a) a0.matrix = Ch02.HomogenizationErrorOnCube Q s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) a a0.matrix) : C * coarseFluxResponseRHSBound Q (publicCoeffField Q a) a0.matrix s (forcedSolutionGradientField u) g ≤ coarseFluxResponseWithRHSRHS (↑d ^ 2 * C) Q a a0 s g u