PerCoreEnergy

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The per-core minimizer energy bound

For a coefficient field c that is (1, Θ)-elliptic on the closed cube U := cubeSet (originCube d m), we produce a single block minimizer Z for (c, P) together with, for every core coreBox ℓ σ k meeting a finite index set K, the per-core energy bound of e.fixed.phase.max.energy:

∫_{coreBox ℓ σ k ∩ U} Z·𝐁(c)Z ≤ Cd · Θ · (3^m)² · ℓ^{d−2} · (Θ|p|² + |q|²).

The proof follows §4.3: the coupled representation (exists_coupledRepresentation) supplies Z, v, v*; the coupled Stampacchia estimate (coupled_stampacchia) supplies the sup-norm K∞ = C_d·3^m·√M²; the per-core smooth cutoff (CutoffData) plus local_block_energy (T2) supplies the energy bound, whose two terms M²·|supp η ∩ U| and Θ·K∞²·∫_U|∇η|² are collapsed by the uniform cutoff estimates (3ℓ)^d and d·(16/ℓ)²·(3ℓ)^d and the power identity ℓ^d = ℓ^{d−2}·ℓ². The energy is stated on the closed cube by transporting the open-cube integrals through the null-boundary bridge cubeSet_originCube_ae_eq_openCubeSet.

The numeric combination of the two local_block_energy terms

The null-boundary energy bridge

theorem HCPolySupport.setIntegral_coreBox_inter_cubeSet_eq_openCubeSet {d : ℕ} {m : ℤ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (f : Vec d → ℝ) : ∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m), f x = ∫ (x : Vec d) in coreBox ℓ σ k ∩ openCubeSet (originCube d m), f x

Set integrals over coreBox ∩ cubeSet and coreBox ∩ openCubeSet coincide: the two cubes differ only by the null boundary.

The per-core minimizer energy bound

theorem HCPolySupport.exists_perCore_minimizer_energy_le_uniform {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {m : ℤ} {Θ : ℝ}, 1 ≤ Θ → ∀ {ℓ : ℝ}, 4 ≤ ℓ → ℓ ≤ 3 ^ m → ∀ (σ : Vec d) (P : BlockVec d) {c : CoeffField d}, IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) c → ∀ (K : Finset (Fin d → ℤ)), ∃ (Z : BlockState d), IsBlockMuAdmissible (cubeSet (originCube d m)) P Z ∧ BlockResponseSpace c (cubeSet (originCube d m)) Z ∧ Mu (cubeSet (originCube d m)) P c = blockEnergyAverage (cubeSet (originCube d m)) c Z ∧ ∀ k ∈ K, ∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m), blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField c x) (Z.eval x)) ≤ Cd * Θ * (3 ^ m) ^ 2 * ℓ ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2)

Uniform per-core energy bound. The constant-outside form of exists_perCore_minimizer_energy_le: a single dimensional constant Cd, independent of the realization c and the core family K, bounds every per-core normalized energy. Uniformity comes from coupled_stampacchia_uniform (single sup-norm constant CdS) and local_block_energy_uniform (literal 514); the per-core numeric collapse is perCore_numeric with CdT := 514.

theorem HCPolySupport.exists_perCore_minimizer_energy_le {d : ℕ} [NeZero d] (hd : 3 ≤ d) {m : ℤ} {Θ : ℝ} (hΘ : 1 ≤ Θ) {ℓ : ℝ} (hℓ4 : 4 ≤ ℓ) (hℓL : ℓ ≤ 3 ^ m) (σ : Vec d) (P : BlockVec d) {c : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) c) (K : Finset (Fin d → ℤ)) : ∃ (Z : BlockState d) (Cd : ℝ), 0 ≤ Cd ∧ IsBlockMuAdmissible (cubeSet (originCube d m)) P Z ∧ BlockResponseSpace c (cubeSet (originCube d m)) Z ∧ Mu (cubeSet (originCube d m)) P c = blockEnergyAverage (cubeSet (originCube d m)) c Z ∧ ∀ k ∈ K, ∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m), blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField c x) (Z.eval x)) ≤ Cd * Θ * (3 ^ m) ^ 2 * ℓ ^ (d - 2) * (Θ * vecNormSq P.1 + vecNormSq P.2)

Per-core energy bound (e.fixed.phase.max.energy). For c elliptic on the closed cube there is a block minimizer Z for (c, P) and a dimensional constant Cd ≥ 0 such that every core meeting K has normalized energy ≤ Cd · Θ · (3^m)² · ℓ^{d−2} · (Θ|p|² + |q|²).