BoundaryDistance

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

The two-sided boundary distance of a Whitney layer

This module proves the assertion ABK26 records without proof — "the cubes in 𝒲(□_m, n) lie at distance roughly 3^{m-n} from the boundary ∂□_m" — and the two consequences its proof of l.bad.clusters.geometry draws from it:

• the two-sided estimate, in the form the consumers need: `3^{m-n} < 3^m/2
  • ‖cubeCenter □‖for every□ ∈ 𝒲(□_m,n) (three_zpow_lt_boundaryMargin_cubeCenter_of_mem_whitneyLayer) and 3^m/2 - ‖x‖ ≤ 3·3^{m-n}for everyx in a layer-n cube (boundaryMargin_le_of_mem_whitneyLayer). Here 3^m/2 - ‖x‖is theℓ^∞distance fromxto∂□_m, since □_mis the centred cube of side3^m`.
• the layer separation constant c = 2/3, dimension-free as computes it: cubes two or more layers apart have centres more than (2/3)·3^{m-n} apart (two_thirds_zpow_lt_norm_cubeCenter_sub_of_layers).
• the adjacency clause of the manuscript's first proof paragraph: two touching Whitney cubes lie in equal or neighbouring layers (whitneyLayer_index_close_of_cubeTouch). Following consequence 2 this needs no percolation input and no largeness of k₀ — only h_n ≥ 1.

Why the lower half is stated at the centre only

The consumer two_thirds_zpow_lt_norm_cubeCenter_sub_of_layers pairs the lower half at the centre of the shallower cube against the upper half at the centre of the deeper one, so the centre-only lower bound suffices; it is also the form for which the index arithmetic is exact.

Provider hypotheses

Both halves are proved for an abstract depth profile hn : ℕ → ℕ; no monotonicity, no gap bound and no dimension hypothesis is used. The adjacency clause adds only 1 ≤ hn n for the two layers involved (consequence 3: k₀ ≥ 1). Layer indices are automatically ≥ 1 because whitneyLayer m hn 0 = ∅.

References

• ABK26, sss.whitney.partition; l.bad.clusters.geometry.

Elementary cube arithmetic

theorem Algsuperdiff.Section3.Provider.Whitney.cubeRadius_eq_zpow_div_two {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeRadius Q = 3 ^ Q.scale / 2

theorem Algsuperdiff.Section3.Provider.Whitney.cubeCenter_mem_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.cubeCenter Q ∈ HCPolySupport.cubeSet Q

theorem Algsuperdiff.Section3.Provider.Whitney.cubeTouch_iff_dist_cubeCenter_le {d : ℕ} {Q R : HCPolySupport.TriadicCube d} : CubeTouch Q R ↔ dist (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeCenter R) ≤ HCPolySupport.cubeRadius Q + HCPolySupport.cubeRadius R

The ℓ^∞ characterization of CubeTouch at the centres.

theorem Algsuperdiff.Section3.Provider.Whitney.norm_cubeCenter_sub_le_of_cubeTouch {d : ℕ} {Q R : HCPolySupport.TriadicCube d} (h : CubeTouch Q R) : ‖HCPolySupport.cubeCenter Q - HCPolySupport.cubeCenter R‖ ≤ HCPolySupport.cubeRadius Q + HCPolySupport.cubeRadius R

Structure of a layer cube

theorem Algsuperdiff.Section3.Provider.Whitney.one_le_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : 1 ≤ n

theorem Algsuperdiff.Section3.Provider.Whitney.exists_interiorCube_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : ∃ C ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) n, ¬TouchesBoundary m C ∧ Q ∈ HCPolySupport.descendantsAtDepth C (hn n)

The interior cube of a layer-n Whitney cube: the depth-n non-boundary-touching descendant of □_m produced by the recursion.

theorem Algsuperdiff.Section3.Provider.Whitney.exists_boundaryAncestor_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : ∃ (A : HCPolySupport.TriadicCube d), A.scale = m - ↑(n - 1) ∧ TouchesBoundary m A ∧ HCPolySupport.cubeSet Q ⊆ HCPolySupport.cubeSet A

The boundary ancestor of a layer-n Whitney cube: the depth-(n-1) descendant of □_m that still touches ∂□_m.

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyLayer_index_unique {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) {n n' : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) (hQ' : Q ∈ whitneyLayer m hn n') : n = n'

Distinct layers of a nondecreasing profile sit at distinct scales, so a Whitney cube determines its layer index.

Additivity of the extreme index

theorem Algsuperdiff.Section3.Provider.Whitney.extremeIdx_add (t s : ℕ) : extremeIdx (t + s) = 3 ^ s * extremeIdx t + extremeIdx s

E_{t+s} = 3^s E_t + E_s: subdividing s further generations rescales the extreme index and adds the extreme index of the new depth.

The two-sided boundary distance

theorem Algsuperdiff.Section3.Provider.Whitney.abs_index_le_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) (j : Fin d) : |Q.index j| ≤ extremeIdx (n + hn n) - 3 ^ hn n

, the index bound. A layer-n Whitney cube has every index coordinate at most E_{n+h_n} - 3^{h_n}: it is a depth-h_n descendant of a non-touching depth-n cube, whose index is at most E_n - 1.

theorem Algsuperdiff.Section3.Provider.Whitney.three_zpow_lt_boundaryMargin_cubeCenter_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) : 3 ^ (m - ↑n) < 3 ^ m / 2 - ‖HCPolySupport.cubeCenter Q‖

, the lower half, at the centre: a layer-n Whitney cube has its centre at ℓ^∞ distance strictly more than 3^{m-n} from ∂□_m.

theorem Algsuperdiff.Section3.Provider.Whitney.boundaryMargin_le_of_mem_whitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.cubeSet Q) : 3 ^ m / 2 - ‖x‖ ≤ 3 * 3 ^ (m - ↑n)

, the upper half: every point of a layer-n Whitney cube is within 3·3^{m-n} of ∂□_m in the ℓ^∞ sense, because the cube sits inside a boundary-touching cube of size 3^{m-n+1}.

Layer separation and adjacency

theorem Algsuperdiff.Section3.Provider.Whitney.two_thirds_zpow_lt_norm_cubeCenter_sub_of_layers {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n n' : ℕ} (hnn' : n + 2 ≤ n') {Q R : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) (hR : R ∈ whitneyLayer m hn n') : 2 / 3 * 3 ^ (m - ↑n) < ‖HCPolySupport.cubeCenter Q - HCPolySupport.cubeCenter R‖

The layer-separation constant c = 2/3: Whitney cubes two or more layers apart have centres more than (2/3)·3^{m-n} apart in the ℓ^∞ sense. The constant is dimension-free.

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyLayer_index_close_of_cubeTouch {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) {n n' : ℕ} {Q R : HCPolySupport.TriadicCube d} (hQ : Q ∈ whitneyLayer m hn n) (hR : R ∈ whitneyLayer m hn n') (htouch : CubeTouch Q R) : n ≤ n' + 1 ∧ n' ≤ n + 1

The adjacency clause: two touching Whitney cubes lie in equal or neighbouring layers. Per consequence 2 this uses no percolation input and no largeness of k₀; only h_n ≥ 1 enters.