Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliScaleZero

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

Scale-zero coarse Caccioppoli inequality

This file contains the full scale-zero proof and theorem packages used by the arbitrary-scale public Caccioppoli interface.

Audit tag

Claim: assemble the single note-facing scale-zero Caccioppoli package from the scalar envelope, with all s,t dependence displayed in the public RHS.

Downstream target: coarseCaccioppoliScaleZeroTheory, consumed by the arbitrary-scale Caccioppoli interface. No additional public *Theory surface belongs in this file.

structure HCPolySupport.Book.Ch03.CoarseCaccioppoliScaleZeroTheory (d : ℕ) [NeZero d] : Prop

Note-facing scale-zero Caccioppoli package. This is the full public statement with m = 0: the constant is dimension-only, while all s,t dependence is displayed in boundaryCaccioppoliRHS and interiorCaccioppoliRHS.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ (∀ {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} (u : BoundaryCaccioppoliDatum Q a x), 0 < s → 0 < t → s + t < 1 → x ∈ openCubeSet Q → Q.scale = 0 → boundaryCaccioppoliCoreEnergy u ≤ boundaryCaccioppoliRHS C s t u) ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (u : CubeSolution Q a), 0 < s → 0 < t → s + t < 1 → Q.scale = 0 → interiorCaccioppoliCoreEnergy Q a (cubeCenter Q) u ≤ interiorCaccioppoliRHS C Q a s t u

theorem HCPolySupport.Book.Ch03.coarseCaccioppoliScaleZeroTheory (d : ℕ) [NeZero d] : CoarseCaccioppoliScaleZeroTheory d

Fully proved note-facing scale-zero Caccioppoli package (m = 0).