Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.Setup.SolutionInputs

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

structure HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) : Prop

The fixed localized energy profile used by the harmonic-gradient Caccioppoli endpoints.

This is the solution-side part that genuinely belongs to the chosen localized energy density: nonnegativity and integrability on the cube, and comparison with each radius-pair harmonic energy on the inner closed cube. It does not assert that a full-cube pair-energy average equals the localized outer-radius profile; that statement is false for a general solution and must not be hidden inside the profile package.

• base_nonneg (x : Vec d) : x ∈ cubeSet Q → 0 ≤ baseEnergy x
• base_integrable : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume
• inner_energy_le ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs.of_constantFamily {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (u : AHarmonicFunction a (openCubeSet Q)) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a (fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) fun (x x_1 : ℝ) => u

The natural energy density of a single harmonic function supplies the fixed localized energy profile for the constant radius-pair family.

structure HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicSolutionInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (C : ℝ) (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (i : Fin d) : Prop

Legacy componentwise solution-side assumptions for the harmonic-gradient Caccioppoli surface.

This groups the fixed localized energy profile, strict positivity of the canonical gradient factors, and the projected Poincare family for the selected component. The projected Poincare field is a compatibility input for older componentwise endpoints; the corrected note-facing route must use the full-dual vector Poincare family instead.

• profile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w
• positive_factors : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w
• projected_poincare : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i

structure HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorProfilePoincareInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (C : ℝ) (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) : Prop

The actual live compatibility inputs for the repaired vector small-cube route: fixed localized profile plus projected-vector Poincare.

This package deliberately omits the old strict positive-factor field. The faithful small-cube route only needs nonnegative local cutoff sizes and gradient circ bounds, both derived directly in the proof; strict positivity would incorrectly exclude the zero harmonic solution. The projected-vector Poincare field is still a legacy consumer boundary and must be replaced by the full-dual vector route before this becomes note-facing.

• profile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w
• projected_vector_poincare : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareVectorFamily Q a C w

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorProfilePoincareInputs.mono_C {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {C₁ C₂ : ℝ} {baseEnergy : Vec d → ℝ} {w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)} (h : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorProfilePoincareInputs Q a C₁ baseEnergy w) (hC : C₁ ≤ C₂) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorProfilePoincareInputs Q a C₂ baseEnergy w

Enlarge the projected-vector Poincare constant inside the live profile/Poincare package.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Note-faithful raw bridge for the vector harmonic Caccioppoli endpoint.

This is the intended landing pad for the local subcube/Besov argument in the LaTeX proof. It is stated only on the Chapter-3 radius sequence, which is the actual recurrence used by the proof and keeps the canonical cutoff away from the outer-radius endpoint 1. Unlike the older canonical coefficient schedules, this bridge is already after the local 3^{k+h} against 3^{-h} cancellation and therefore targets the note's radius-recursion coefficients directly.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Split note-faithful raw bridge for the vector harmonic Caccioppoli endpoint. Calpha controls the explicit height/absorption coefficient and Ccross controls the cross coefficient.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

All-radii split raw bridge for the vector harmonic Caccioppoli endpoint. This is the bridge shape consumed by the standard beta-dependent hole-filling iteration.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridge {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Interior counterpart of the note-faithful raw bridge. The current interior Caccioppoli backbone reuses the same coefficient shape as the boundary case; the distinction is in how the local estimate is produced.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Split interior counterpart of the note-faithful raw bridge. As in the boundary bridge, Calpha controls the explicit height/absorption coefficient and Ccross controls the cross coefficient.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

All-radii split raw bridge for the centered interior endpoint.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridge {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Boundary raw bridge for an arbitrary-center local patch radius profile.

This is the translated/localized counterpart of CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge: the recurrence uses the same note-facing coefficients, but the energy profile is centered at the boundary/interior patch center and has base scale Q.scale - 1.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplit {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Split boundary raw bridge for an arbitrary-center local patch radius profile. Calpha controls the explicit height/absorption coefficient and Ccross controls the cross coefficient.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

All-radii split raw bridge for an arbitrary-center local patch radius profile.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorLocalPatchNoteRawBridge {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) : Prop

Interior counterpart of the local-patch raw bridge. The coefficient shape is again identical to the boundary bridge at the radius-recursion level.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorLocalPatchNoteRawBridge.of_boundary {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (h : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridge Q center a s t C uL2Sq baseEnergy) : CoarseCaccioppoliInteriorCanonicalHarmonicVectorLocalPatchNoteRawBridge Q center a s t C uL2Sq baseEnergy

The local-patch interior and boundary vector raw bridges have the same radius-sequence recurrence shape.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge.of_noteRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t (↑(Fintype.card (Fin d)) * C) uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t (↑(Fintype.card (Fin d)) * C) coarseCaccioppoliTriadicGapScale) (coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy)) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge Q a s t C uL2Sq baseEnergy

An all-radii boundary raw estimate restricts to the note-faithful Chapter-3 radius-sequence bridge.

theorem HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridge.of_noteRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t (↑(Fintype.card (Fin d)) * C) uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t (↑(Fintype.card (Fin d)) * C) coarseCaccioppoliTriadicGapScale) (coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy)) : CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridge Q a s t C uL2Sq baseEnergy

An all-radii interior raw estimate restricts to the note-faithful Chapter-3 radius-sequence bridge.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit.of_allRadii {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (hraw : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii Q a s t Calpha Ccross uL2Sq baseEnergy) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit Q a s t Calpha Ccross uL2Sq baseEnergy

An all-radii split boundary raw bridge restricts to the legacy radius-sequence split bridge.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplit.of_allRadii {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (hraw : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplitAllRadii Q center a s t Calpha Ccross uL2Sq baseEnergy) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorLocalPatchNoteRawBridgeSplit Q center a s t Calpha Ccross uL2Sq baseEnergy

An all-radii split local-patch raw bridge restricts to the legacy radius-sequence split local-patch bridge.

theorem HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridge.of_boundary {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (h : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge Q a s t C uL2Sq baseEnergy) : CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridge Q a s t C uL2Sq baseEnergy

The interior and boundary vector raw bridges have the same radius-sequence recurrence shape at this level.

theorem HCPolySupport.CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplit.of_boundary {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (baseEnergy : Vec d → ℝ) (h : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit Q a s t Calpha Ccross uL2Sq baseEnergy) : CoarseCaccioppoliInteriorCanonicalHarmonicVectorNoteRawBridgeSplit Q a s t Calpha Ccross uL2Sq baseEnergy

The split interior and boundary vector raw bridges have the same radius-sequence recurrence shape at this level.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicSolutionInputs.of_projectedPoincareCircBounds {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (i : Fin d) (hProfile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w) (hpositiveFactors : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w) (hProjectedCirc : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i) (coarseCaccioppoliCanonicalGradientAcircOne Q a) (coarseCaccioppoliCanonicalGradientAcircOneSub Q a s)) : CoarseCaccioppoliBoundaryCanonicalHarmonicSolutionInputs Q a C baseEnergy w i

Build the legacy solution-side package from the existing projected-Poincare and circ package for the canonical gradient component. The final theorem only needs the projected-Poincare part; the two circ estimates are useful upstream and are safely forgotten here.

structure HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (i : Fin d) : Prop

The remaining analytic/profile hypotheses for the legacy componentwise harmonic-gradient endpoint at the Chapter-3 radii.

This package deliberately does not hide the coefficient schedule or the multiscale ellipticity data. Its role is to name the solution-side inputs: fixed localized energy profile, flux/gradient energy controls, nonzero energy factors, the explicit full-cube/localized energy compatibility equality, and the projected Poincare family for the selected component.

• base_nonneg (x : Vec d) : x ∈ cubeSet Q → 0 ≤ baseEnergy x
• base_integrable : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume
• inner_energy_le ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x
• energy_average ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂
• flux_energy ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x
• nonzero_energy_factors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w
• gradient_energy ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x
• projected_poincare : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs.of_profile_energyControls {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) {lam Lam : ℝ} (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (i : Fin d) (hs : 0 < s) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂) (hProfile : CoarseCaccioppoliBoundaryCanonicalHarmonicProfileInputs Q a baseEnergy w) (hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w) (hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i) : CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs Q a s C baseEnergy w i

Extend a fixed localized profile package to the final analytic-input package by deriving the flux and gradient energy-control fields from closed-cube ellipticity, while keeping the nondegeneracy and projected Poincare inputs explicit.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicSolutionInputs.to_analyticInputs_energyControls {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} {s C lam Lam : ℝ} {baseEnergy : Vec d → ℝ} {w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)} {i : Fin d} (hSolution : CoarseCaccioppoliBoundaryCanonicalHarmonicSolutionInputs Q a C baseEnergy w i) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂) (hs : 0 < s) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) : CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs Q a s C baseEnergy w i

Extend the clean solution-side package to the analytic-input package under closed-cube ellipticity.

The solution package records strict positivity of the canonical gradient factors. The analytic package only needs the weaker nonzero-energy part, so this bridge forgets the extra Acirc positivity while deriving the flux and gradient energy controls from closed-cube ellipticity.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs.of_closedCubeHarmonicEnergyControls {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s C : ℝ) {lam Lam : ℝ} (baseEnergy : Vec d → ℝ) (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (i : Fin d) (hs : 0 < s) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x) (hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume) (hinner_energy_le : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂) (hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w) (hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i) : CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs Q a s C baseEnergy w i

Build the final analytic/profile input package from the remaining profile, nondegeneracy, and projected-Poincare fields, while deriving the flux and gradient energy-control fields from closed-cube ellipticity.

This is a compatibility bridge for the current coarse-Poincare API: it uses AHarmonicFunction.toCubeSet, so it requires ellipticity on cubeSet Q. The pure note-facing open-cube version remains the next analytic target.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds.of_multiscaleEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)) (hC : 0 < C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds Q a s t C uL2Sq w

Localize the canonical harmonic coefficient schedule to the raw radius-recursion coefficient schedule. This is the final coefficient-only composition step: single-cube coefficient bounds plus standard multiscale data produce the raw Alpha/Bcross inequalities consumed by the newest wrappers.