Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoli.Interface

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

Coarse Caccioppoli interface

This file keeps the public Prop structure for the arbitrary-scale Caccioppoli surface. The final unconditional public apex theorem is declared in HCPolySupport.Book.Ch03.Theorems.CoarseCaccioppoliDilationTransport and re-exported by HCPolySupport.Book.Ch03.Theorems.CoarseCaccioppoli.

Audit tag

Claim: define the single public arbitrary-scale Caccioppoli package consumed by the scale-normalization proof from the scale-zero theorem.

Downstream target: CoarseCaccioppoli.lean and CoarseCaccioppoliRHS/Theory.lean. New public Caccioppoli variants must amend the Ch3 surface contract first.

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

Public theorem package for the boundary and interior coarse-grained Caccioppoli inequalities. The constant is dimension-only; all exponent dependence on s,t is displayed in the public RHS definitions. The boundary theorem is local in a center x ∈ Q; the interior theorem is the centered cube estimate from the notes, with arbitrary translated cubes represented by the choice of Q.

• 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 → 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 → interiorCaccioppoliCoreEnergy Q a (cubeCenter Q) u ≤ interiorCaccioppoliRHS C Q a s t u