Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube.Constructor

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredCoeff_buffered_localAcirc_le_alpha_of_scale {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s t CeffLocal CeffWork : ℝ} {k j : ℕ} {ρ₁ ρ₂ lam Lam : ℝ} {hheight : ℝ → ℝ → ℝ} (η : QuantitativeCubeCutoff Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) (hCeffLocal : 0 ≤ CeffLocal) (hCeffWork : 0 ≤ CeffWork) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) (hscale : (2 * coarseCaccioppoliCenteredAverageFront d s CeffLocal + 4 * coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + 2 * coarseCaccioppoliCenteredBesovGradientFront d s CeffLocal) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j) : have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField η.toFun) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρm) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρm) CeffLocal ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

Buffered exact centered local coefficient, with descendant-local canonical A^\circ factors, localized directly to the parent Alpha coefficient. The cutoff radius is the midpoint, while the height and Alpha radius pair remain the full outer pair.

theorem HCPolySupport.BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit.of_centeredFronts {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hwork_constant_cross : 81 * Real.rpow 3 s * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hwork_centered_fronts_alpha : 81 * (2 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * Clocal) + 4 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * Clocal) + 2 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * Clocal)) ≤ ↑(Fintype.card (Fin d)) * Calpha / (s * (1 - s))) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (4 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 2 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) : BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit Q a s t Clocal Calpha Ccross

Split buffered exact-to-parent-raw coefficient bounds from closed-cube ellipticity and separate note budgets.

Calpha controls the explicit height and centered absorption coefficient, while Ccross controls only the constant/cross branch.

theorem HCPolySupport.boundaryCaccioppoliSmallCubeCoefficientSplitAllRadii.of_centeredFronts {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hwork_constant_cross : 81 * Real.rpow 3 s * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hwork_centered_fronts_alpha : 81 * (2 * coarseCaccioppoliCenteredAverageFront d s (↑(Fintype.card (Fin d)) * Clocal) + 4 * coarseCaccioppoliCenteredBesovHessianFront d s (↑(Fintype.card (Fin d)) * Clocal) + 2 * coarseCaccioppoliCenteredBesovGradientFront d s (↑(Fintype.card (Fin d)) * Clocal)) ≤ ↑(Fintype.card (Fin d)) * Calpha / (s * (1 - s))) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (4 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 2 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) : boundaryCaccioppoliSmallCubeCoefficientSplitAllRadii Q a s t Clocal Calpha Ccross

All-radii split buffered exact-to-parent-raw coefficient bounds from closed-cube ellipticity and separate note budgets.

This is the proof-producing coefficient package used by the standard beta-dependent radius iteration.