High-contrast homogenization:

Provider.PolynomialHomogenization.Root.EnergyPrice.GaugeCubeEnergyPriceWitness

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The capstone energy predicate, inhabited on a cube with a law-free constant

GaugePhysicalEnergyPriceAtWitness U aPhysical u Kenergy boundaryEnergy is the open analytic hypothesis of the Dirichlet capstone. This file inhabits it, byte-for-byte, at a triadic cube witness with

Kenergy = gaugeCubeEnergyPrice C d s (cubeScaleFactor Q),

an explicit function of the dimension, the fractional order, and the cube's side length only — no law, no sample, no ellipticity constant.

The three inputs are: the upstream dimension-only Dirichlet energy package (energyConsequencesRHSTheory), the coarse-ellipticity window of HCPoly.Provider.PolynomialHomogenization.Root.EnergyPrice.LawFreeCubeEnergyPrice (a single scalar hypothesis 𝓔 ≤ 1), and the positive-Besov/Euclidean-fractional comparison.

The un-squared law-free bound

The ENNReal energy average on a cube

theorem HCPolySupport.HighContrast.EnergyPrice.eVolumeAverage_coefficientEnergyDensity_eq {d : ℕ} (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) (u : H1Function (Book.Ch02.cubeDomain Q).carrier) : (eVolumeAverage (openCubeSet Q) fun (z : Vec d) => ENNReal.ofReal (coefficientEnergyDensity (a.coeffOn Q).toCoeffField u.grad z)) = ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube Q a u) ^ 2

The extended-real coefficient-energy average on a cube is the square of the ENNReal realization of the public cube energy norm.

The law-free capstone price at a cube witness