CaccioppoliInteriorGeometry #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The interior-regime geometry of the coarse-grained Caccioppoli window #
The frozen §4.3 anchor's second conjunct (the frontier-empty clause) is gated on
((z + □_{n+2}) image) ∩ frontier (□_m) = ∅ .
This module turns that gate into the two geometric facts the coarse-grained
Caccioppoli step needs, and matches the window triple of ABK26's
l.coarse.grained.Caccioppoli.RHS to CoarseGraining's own caccioppoliCoreSet.
What the gate buys #
image_add_openCubeSet_subset_of_frontier_inter_empty: the translated parent
cube is contained in □_m. The proof is topological, not coordinatewise: the
translated open cube is convex, hence preconnected; the complement of
frontier □_m is the disjoint union of the open set □_m and the open set
(closure □_m)ᶜ; a preconnected set inside that union which meets □_m lies in
□_m. It meets □_m because z ∈ □_m and 0 ∈ □_{n+2}.
The Caccioppoli window triple is CoarseGraining's own #
caccioppoliCoreSet Q x = openCubeSet Q ∩ openCubeAtScale x (Q.scale - 2) .
Carrier convention (resolution A4) #
Every cube is an origin cube; a window centred at z is realized by
translating the sample. The geometry lemmas below therefore appear twice: once
for the untranslated image (fun y => z + y) '' □_k used by the frozen
statement, and once for the shifted centre w = x - z used by the translated
frame in which the Caccioppoli is applied.
References #
- ABK26,
l.coarse.grained.Caccioppoli.RHS. - ABK26,
e.energy.bound.interior.
1. Translations: images and translateSet #
The frozen statement's translated window is CoarseGraining's translateSet.
CoarseGraining's openCubeAtScale at a real centre is the frozen statement's
translated origin cube.
2. The gate: a preconnected set off the frontier stays inside #
A preconnected set which meets an open set and misses its frontier lies
inside it. The complement of frontier U is the disjoint union of the two
open sets U (for open U, interior U = U) and (closure U)ᶜ.
The centre of an origin cube lies in it.
The interior gate gives the full parent cube.
If z ∈ □_m and the translated parent cube z + □_k misses frontier □_m,
then z + □_k ⊆ □_m. This is the inclusion the frozen theorem's
frontier-empty clause supplies to the interior Caccioppoli application, and it
is what makes the Dirichlet locus of that application empty.
3. The two-scale window triple #
Origin cubes are nested in their scale.
If the two-scale core window already sits inside the outer cube,
CoarseGraining's caccioppoliCoreSet is that window.
The shifted child centre lies in the parent cube.
From the frozen theorem's geometry binder, the shifted centre w = x - z lies
in □_{n+1}, hence in □_{n+2}: CoarseGraining's Caccioppoli hypothesis x ∈ openCubeSet Q holds in the translated frame.
A window centred in □_{n+1} of scale at most n+1 sits in □_{n+2}.
The one geometric estimate behind both the Dirichlet patch inclusion (k = n+1)
and the core identity (k = n) of the two-scale window triple.
The Dirichlet patch of the translated frame sits inside the parent.
Under the frozen theorem's geometry binder, the Caccioppoli localization patch
(x - z) + □_{n+1} is a subset of □_{n+2}: the interior regime's hypothesis.
The Caccioppoli core is the translated child cube.
Under the frozen theorem's geometry binder, read in the translated frame at the
outer cube □_{n+2} and the shifted centre w = x - z,
caccioppoliCoreSet (□_{n+2}) (x - z) = (x - z) + □_n ,