MeanControlWindowCube

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

The mean comparison, step 1: a boundary-flush cube inside the anchor's own

window

Nothing here imports that file, and nothing here claims the anchor or any source node.

The geometric obstruction this module removes

The mean comparison asks for a bound on the scalar

  S = |⨍_{c+□_{n+2}} (u − h)| ,    c = wellPlacedCentre x m (n+2) ,

on the boundary branch (z+□_{n+2}) ∩ ∂□_m ≠ ∅. The only extra information the boundary branch carries is the zero trace of u − h on ∂□_m, so any producer must reach ∂□_m from the cube it works on. The covering cube of the anchor's own centre x does not reach it: the branch is a statement about z, and x is only known to lie in z + □_{n+1}, so x can sit a distance 3^{n+1}/2 short of the clamp level and wellPlacedCentre x m (n+2) + □_{n+2} can then be strictly interior to □_m.

This module produces the cube that does reach it, from the anchor's own binders and with no new construction: the same wellPlacedCentre clamp, applied to z instead of x. Writing

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

three facts are proved.

• K ⊆ □_m (image_add_wellPlacedCentre_subset_openCubeSet, reused): the equation, the Caccioppoli and the coarse-graining envelope are all available on K.
• K ⊆ (z+□_{n+3}) ∩ □_m (image_add_wellPlacedCentre_z_subset_anchorWindow): K sits inside the frozen window W', so every quantity read on K is transportable to the frozen first and fifth legs by the 3^d measure ratio.
• K is flush against ∂□_m (wellPlacedCentre_flush, faceLevel_sub_lt_of_mem_wellPlacedCube): on the boundary branch there are a coordinate i and a sign σ = ±1 with

    σ · (wellPlacedCentre z m (n+2))ᵢ + ½·3^{n+2} = ½·3^m ,
  

  i.e. the σeᵢ face of K lies exactly in the frontier hyperplane of □_m, and consequently every point of K is within 3^{n+2} of that hyperplane.

The last item is what the funded coarse-grained boundary Poincaré needs and what the x-centred covering cube cannot supply: u − h has zero trace on the face, so a comparator on K that shares u's boundary data agrees with the datum h there. The n+3 ≤ m binder of the frozen statement is what makes the (n+2) clamp legitimate (n + 2 ≤ m suffices, and is implied).

1. Coordinates of a translated open cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_image_add_openCubeSet_coord_iff {d : ℕ} {j : ℤ} {z y : HCPolySupport.Vec d} : y ∈ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ j < y i - z i ∧ y i - z i < 1 / 2 * 3 ^ j

Membership in a translated open triadic cube, coordinatewise.

2. The negated interior gate, in clamp normal form

theorem Algsuperdiff.Section4.Provider.ExcessDecay.overhang_of_boundaryBranch {d : ℕ} {j m : ℤ} {z : HCPolySupport.Vec d} (hfr : (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≠ ∅) : ∃ (i : Fin d) (σ : ℝ), (σ = 1 ∨ σ = -1) ∧ wellPlacedHalfGap m j < σ * z i

The boundary branch, quantitatively.

If the parent cube z + □_j meets the frontier of □_m, then in some coordinate i and some direction σ = ±1 the centre z already exceeds the clamp level wellPlacedHalfGap m j = ½·3^m − ½·3^j of the well-placed cube of side 3^j. This is exactly the hypothesis under which the clamp saturates, so it is the bridge from the anchor's negated gate to a boundary-flush cube.

3. The clamp saturates: the cube is flush against the frontier

theorem Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedCentre_flush {d : ℕ} {m k : ℤ} (hkm : k ≤ m) {z : HCPolySupport.Vec d} {i : Fin d} {σ : ℝ} (hσ : σ = 1 ∨ σ = -1) (hover : wellPlacedHalfGap m k < σ * z i) : σ * wellPlacedCentre z m k i = wellPlacedHalfGap m k

The flush face.

If the centre z exceeds the clamp level in the direction σeᵢ, then the well-placed centre of side 3^k saturates the clamp in that coordinate: σ·cᵢ = wellPlacedHalfGap m k.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.wellPlacedCentre_faceLevel {d : ℕ} {m k : ℤ} (hkm : k ≤ m) {z : HCPolySupport.Vec d} {i : Fin d} {σ : ℝ} (hσ : σ = 1 ∨ σ = -1) (hover : wellPlacedHalfGap m k < σ * z i) : σ * wellPlacedCentre z m k i + 1 / 2 * 3 ^ k = 1 / 2 * 3 ^ m

The flush face, at the frontier level. The σeᵢ face of the well-placed cube wellPlacedCentre z m k + □_k lies exactly in the frontier hyperplane {σ yᵢ = ½·3^m} of □_m.

4. The flush cube sits inside the frozen window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_wellPlacedCentre_sub_lt {d : ℕ} {m k : ℤ} (hkm : k ≤ m) {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (i : Fin d) : |wellPlacedCentre z m k i - z i| < 1 / 2 * 3 ^ k

The well-placed centre of z never moves z by as much as a half side.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_z_subset_anchorWindow {d : ℕ} {n m : ℤ} (hnm : n + 2 ≤ m) {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The flush cube lies in the frozen window.

wellPlacedCentre z m (n+2) + □_{n+2} ⊆ (z+□_{n+3}) ∩ □_m: every quantity read on the flush cube transports to the frozen clause's own window at the 3^d measure ratio.