SealCaccioppoliGeometry #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Route (b) of the S4.3 boundary lane: the geometric containment machine-check #

What is at stake #

Route (b) wants to price the gradient of the anchor's solution on the boundary-flush cube

  K := wellPlacedCentre z m (n+2) + □_{n+2}       (`MeanControlWindowCube`)

by a single application of a boundary Caccioppoli estimate whose outer window still sits inside the frozen first-leg window

  W' := ((z + □_{n+3}) ∩ □_m) .

Each proved boundary Caccioppoli A has a core set (where the energy is read) and an outer set (where the L² right-hand side is read). A single application prices K iff core ⊇ K and outer ⊆ W'.

The configuration table (proved here) #

Write x' for the centre the A is entered at and k for its outer scale.

BoundaryOuterAssembly.exists_boundaryWindowEnergy_le_dirichletDatum at scale k: core truncatedWindow x' m (k-2) = (x'+□_{k-2}) ∩ □_m, outer wellPlacedCentre x' m k + □_k`.
- core ⊇ K forces n + 4 ≤ k (add_four_le_of_flushCube_subset_truncatedWindow).
- outer ⊆ W' forces k ≤ n + 3 (scale_le_of_image_add_subset_anchorWindow).
- Hence no k works at all: no_single_boundaryOuterAssembly_application.
- k = n+2: core (not_flushCube_subset_truncatedWindow_core); outer, and this is the pivotal positive fact (image_add_wellPlacedCentre_flush_subset_anchorWindow).
- k = n+3: core (same lemma, n+3 < n+4); outer, and for a second, independent reason — equal side lengths force the outer centre to be z itself (centre_eq_of_image_add_openCubeSet_subset) and on the boundary branch z + □_{n+3} ⊄ □_m (not_image_add_openCubeSet_subset_of_boundaryBranch); the two combine in not_exists_outer_at_scale_add_three.
- k = n+4: core at x' = wellPlacedCentre z m (n+2) (flushCube_subset_truncatedWindow_self); outer (not_image_add_subset_anchorWindow_of_add_four_le).
CoarseAssemblyDatum.exists_boundaryWindowEnergy_rebased_le_dirichletDatum: core x + □n (an untruncated scale-ncube), outerwellPlacedCentre x m (n+2) + □{n+2}`.
- core ⊇ K: not_flushCube_subset_image_add_openCubeSet_of_lt at j = n < n + 2.
- outer ⊆ W' whenever the entry centre lies in K, again by image_add_wellPlacedCentre_flush_subset_anchorWindow.
the raw BoundaryOuterCaccioppoli form at a TriadicCube of scale k: core caccioppoliCoreSet (originCube d k) x' = □_k ∩ (x' + □_{k-2}), outer □_k, both read in a translated frame c + ·.
- core ⊇ K forces n + 4 ≤ k (add_four_le_of_flushCube_subset_image_add_caccioppoliCoreSet), so the raw form reproduces exactly the same obstruction.

The single positive fact, and the only one, is the outer inclusion at k = n+2; the core is then two triadic scales too small. With the read window taken to be K itself, route (b) therefore cannot be closed by one application of any proved boundary Caccioppoli A.

Shrinking the read window to the flush scale-`n` sub-cube #

The obstruction is entirely caused by insisting that the read window be K. Take instead the scale-n sub-cube of K that shares K's flush σeᵢ face,

  K' := x' + □_n ,     x' := wellPlacedCentre z m (n+2) + σ·½(3^{n+2} − 3^n)·eᵢ ,

with (i, σ) the coordinate and sign of MeanControlWindowCube.overhang_of_boundaryBranch (flushSubCentre). Then all four requirements hold at once, at the outer scale k = n+2:

x' ∈ K — flushSubCentre_mem_flushCube (the displacement is 4·3^n < ½·3^{n+2} = 4.5·3^n, strictly);
K' ⊆ K ⊆ □_m — flushSubCube_subset_flushCube, flushSubCube_subset_openCubeSet, and K' ⊆ W' (flushSubCube_subset_anchorWindow);
K' is flush at the same face — flushSubCentre_faceLevel, flushSubCentre_faceLevel_signed;
the assembly fits exactly at k = n+2 (flushSubCube_boundaryOuterAssembly_fits): its core is truncatedWindow x' m (k-2) = truncatedWindow x' m n = K' — an equality, since K' ⊆ □_m (truncatedWindow_eq_flushSubCube) — and its outer window wellPlacedCentre x' m (n+2) + □_{n+2} is inside W' by the pivotal positive theorem instantiated at this x' (outer_subset_anchorWindow_flushSubCentre).

So the configuration table for K' has one row: read window K' (scale n), k = n+2, core = K' exactly, outer ⊆ W'. Every row above is a statement about the read window K (scale n+2) and stays exactly as proved; those rows are what force the smaller read window.

The pivotal positive theorem, in words #

The clamp wellPlacedCentre · m k is coordinatewise 1-Lipschitz (abs_wellPlacedCentre_sub_wellPlacedCentre_le) and fixes its own image (wellPlacedCentre_wellPlacedCentre). So for x' ∈ K, with cz := wellPlacedCentre z m (n+2) and c' := wellPlacedCentre x' m (n+2),

  |c'_i - cz_i| ≤ |x'_i - cz_i| < ½·3^{n+2} ,   |cz_i - z_i| < ½·3^{n+2} ,

hence |c'_i - z_i| < 3^{n+2} and every y ∈ c' + □_{n+2} obeys |y_i - z_i| < ½·3^{n+2} + 3^{n+2} = ½·3^{n+3} — the requirement, strictly.

References #

ABK26, l.harmonic.approximation.good.scales, Step 2 (boundary cubes).
CoarseGraining, Homogenization/Book/Ch03/Definitions.lean (caccioppoliCoreSet).

SealCaccioppoliGeometry #

Route (b) of the S4.3 boundary lane: the geometric containment machine-check #

What is at stake #

The configuration table (proved here) #

Shrinking the read window to the flush scale-n sub-cube #

The pivotal positive theorem, in words #

References #

0. Two elementary translation identities #

2. The clamp is 1-Lipschitz and idempotent #

3. The pivotal positive theorem #

4. The refutations #

5. The flush scale-n sub-cube, and the exact fit at k = n+2 #

Shrinking the read window to the flush scale-`n` sub-cube #

5. The flush scale-`n` sub-cube, and the exact fit at `k = n+2` #