ClusterLayerConstraint

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

l.bad.clusters.geometry, clause (1): the layer constraint

This module proves the layer constraint of ABK26's Lemma l.bad.clusters.geometry for the closure-touching neighborhood 𝒩(𝒞) of a connected component 𝒞 of the bad family:

• whitneyNeighborhood_layer_index_close — any two cubes of 𝒩(𝒞) occupy equal or neighbouring Whitney layers;
• whitneyNeighborhood_finite_and_mem_leastLayer_or_succ — consequently 𝒩(𝒞) is finite and contained in its least occupied layer together with that layer's successor, which is the manuscript's 𝒩(𝒞) ⊆ 𝒲(□_m,n-1) ∪ 𝒲(□_m,n) ∪ 𝒲(□_m,n+1) read at the least occupied layer ("in particular, every 2-connected component intersects at most two consecutive layers").

Only the deterministic geometric layer is delivered: as in the manuscript, the statements are conditional on avoidance of the bad-cluster diameter failure, carried by the binder havoid below. No probability estimate is used.

The avoidance binder

havoid is shaped exactly on the conclusion of the proved distance-two machinery,

havoid : ∀ h : ℕ, hs ≤ h → ∀ u ∈ Percolation.cubeFinset (d := d) h,
  (Percolation.badClusterDiam M m h omega u : ℝ) < (3 : ℝ) ^ (b * (h : ℝ))

which is e.diameter.deterministic in the cube-side units of Percolation.badClusterDiam. It is discharged verbatim by the proved Percolation.badClusterDiam_lt_of_hsep_le at hs:= Percolation.hsep M m E b omega, since h_n ≥ h_hat_sep for every n (hsep_le_whitneyScaleSeq); this is the concrete corollary badFamily_whitneyNeighborhood_finite_and_mem_leastLayer_or_succ at the end of the module. In the abstract helper, havoid remains an explicit conditional A obligation; the concrete corollary discharges it from the manuscript's p.minimal.scale.separation input rather than adding it to a source-facing statement.

The proof, and where each ingredient lives

1. "Cubes in layer n lie at distance of order 3^{m-n} from ∂□_m; cubes in layers differing by two or more occupy disjoint regions, so adjacent cubes come from consecutive layers." — two_thirds_zpow_lt_norm_cubeCenter_sub_of_layers and whitneyLayer_index_close_of_cubeTouch of BoundaryDistance, at the dimension-free c = 2/3.
2. "□ is a descendant of □ within < 9 generations, so 𝓑(□) forces 𝓑^*(□); adjacent cubes lift to identical or adjacent cubes at scale 3^{m-n_min-h_{n_min}}." (the diameter display) — IsWhitneyLift and the dictionary below, with the generation count supplied by the proved whitneyDepth_sub_lt_ten and the site adjacency proved as Percolation.Connected₂ (distance two).
3. "Applying e.diameter.deterministic with h = n_min + h_{n_min} … choosing k₀ large enough that 4·3^{-(1-b)k₀} < c." (as corrected) — the proved gate four_mul_three_rpow_whitneyDepth_lt_two_thirds at k₀ ≥ 3.

The core induction runs along the chain relation of the component and carries the lifted site path with it, so that at the first cube that would reach layer n_min + 2 the diameter bound and the layer separation collide.

The two readings of 𝒩(𝒥)

whitneyNeighborhood is the cubewise reading ∃ □' ∈ 𝒥, dist(□,□') = 0, which for an infinite 𝒥 is strictly smaller than the printed dist(□, ⋃𝒥) = 0. The finiteness delivered here proves the local comparison: 𝒩(𝒞) is finite, hence so is 𝒞, and on a finite family the two readings coincide (whitneyNeighborhood_eq_whitneyNeighborhoodDist_of_finite, applied to the component in whitneyNeighborhood_eq_dist_reading).

References

• ABK26, l.bad.clusters.geometry.

The least occupied Whitney layer

def Algsuperdiff.Section3.Provider.Whitney.whitneyLayerIndices {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (J : Set (HCPolySupport.TriadicCube d)) : Set ℕ

The set of Whitney layers a family occupies.

Equations

• Algsuperdiff.Section3.Provider.Whitney.whitneyLayerIndices m hn J = {n : ℕ | ∃ Q ∈ J, Q ∈ Algsuperdiff.Section3.Provider.Whitney.whitneyLayer m hn n}

noncomputable def Algsuperdiff.Section3.Provider.Whitney.leastWhitneyLayer {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (J : Set (HCPolySupport.TriadicCube d)) : ℕ

The least Whitney layer a family occupies (n_min).

Equations

• Algsuperdiff.Section3.Provider.Whitney.leastWhitneyLayer m hn J = sInf (Algsuperdiff.Section3.Provider.Whitney.whitneyLayerIndices m hn J)

theorem Algsuperdiff.Section3.Provider.Whitney.leastWhitneyLayer_le_of_mem {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {J : Set (HCPolySupport.TriadicCube d)} {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ J) (hQn : Q ∈ whitneyLayer m hn n) : leastWhitneyLayer m hn J ≤ n

theorem Algsuperdiff.Section3.Provider.Whitney.exists_mem_leastWhitneyLayer {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {J : Set (HCPolySupport.TriadicCube d)} (hne : J.Nonempty) (hJ : J ⊆ whitneyPartition m hn) : ∃ Q ∈ J, Q ∈ whitneyLayer m hn (leastWhitneyLayer m hn J)

The lift to the base lattice

def Algsuperdiff.Section3.Provider.Whitney.IsWhitneyLift {d : ℕ} (m : ℤ) (h : ℕ) (V A : HCPolySupport.TriadicCube d) : Prop

The lift □: A is a depth-h triadic descendant of □_m having the Whitney cube V among its descendants within the nine generations of e.Bext.def.

Equations

• Algsuperdiff.Section3.Provider.Whitney.IsWhitneyLift m h V A = (A ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) h ∧ ∃ g < 10, V ∈ HCPolySupport.descendantsAtDepth A g)

theorem Algsuperdiff.Section3.Provider.Whitney.closedBall_subset_closedBall_of_mem_descendantsAtDepth {d : ℕ} {A V : HCPolySupport.TriadicCube d} {g : ℕ} (h : V ∈ HCPolySupport.descendantsAtDepth A g) : Metric.closedBall (HCPolySupport.cubeCenter V) (HCPolySupport.cubeRadius V) ⊆ Metric.closedBall (HCPolySupport.cubeCenter A) (HCPolySupport.cubeRadius A)

theorem Algsuperdiff.Section3.Provider.Whitney.exists_isWhitneyLift {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {n h : ℕ} {V : HCPolySupport.TriadicCube d} (hV : V ∈ whitneyLayer m hn n) (hh : h ≤ n + hn n) (hgap : n + hn n - h < 10) : ∃ (A : HCPolySupport.TriadicCube d), IsWhitneyLift m h V A

Every Whitney cube of a layer at least as deep as h has a lift at depth h, provided the generation gap stays inside the nine generations of e.Bext.def.

theorem Algsuperdiff.Section3.Provider.Whitney.badExtended_of_isWhitneyLift {d : ℕ} {M : ABKModel d} {m : ℤ} {h : ℕ} {omega : Cutoff.CutoffSample d} {V A : HCPolySupport.TriadicCube d} (hlift : IsWhitneyLift m h V A) (hbad : omega ∈ BadEvents.bad M V) : omega ∈ BadEvents.badExtended M A

The bad event at a Whitney cube forces the extended bad event at its lift: the manuscript's "□ is a descendant of □ within < 9 generations and 𝓑(□) occurs, so 𝓑^*(□) occurs".

theorem Algsuperdiff.Section3.Provider.Whitney.index_mem_badSiteFinset_of_isWhitneyLift {d : ℕ} {M : ABKModel d} {m : ℤ} {h : ℕ} {omega : Cutoff.CutoffSample d} {V A : HCPolySupport.TriadicCube d} (hlift : IsWhitneyLift m h V A) (hbad : omega ∈ BadEvents.bad M V) : A.index ∈ Percolation.badSiteFinset M m h omega

The lift of a bad Whitney cube is a bad site of the base lattice at depth h: this is the entry point into the proved 2-cluster machinery.

theorem Algsuperdiff.Section3.Provider.Whitney.latDist_index_le_one_of_cubeTouch {d : ℕ} {m : ℤ} {h : ℕ} {U W AU AW : HCPolySupport.TriadicCube d} (hU : IsWhitneyLift m h U AU) (hW : IsWhitneyLift m h W AW) (htouch : CubeTouch U W) : Percolation.latDist AU.index AW.index ≤ 1

"Adjacent cubes lift to identical or adjacent cubes": the lifts of two touching Whitney cubes are at lattice sup distance at most one, so in particular they are 2-adjacent in the sense.

theorem Algsuperdiff.Section3.Provider.Whitney.norm_cubeCenter_sub_le_of_isWhitneyLift {d : ℕ} {m : ℤ} {h : ℕ} {U W AU AW : HCPolySupport.TriadicCube d} (hU : IsWhitneyLift m h U AU) (hW : IsWhitneyLift m h W AW) : ‖HCPolySupport.cubeCenter U - HCPolySupport.cubeCenter W‖ ≤ (↑(Percolation.latDist AU.index AW.index) + 1) * 3 ^ (m - ↑h)

The physical distance between two Whitney cubes, in terms of the lattice distance of their lifts: passing from cube centres to lattice sites costs one side length in total (the "+1" of the corrected display).

The diameter estimate at a common lift scale

theorem Algsuperdiff.Section3.Provider.Whitney.norm_cubeCenter_sub_lt_of_connected₂ {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {h : ℕ} {omega : Cutoff.CutoffSample d} {U W AU AW : HCPolySupport.TriadicCube d} {z : Fin d → ℤ} (hU : IsWhitneyLift m h U AU) (hW : IsWhitneyLift m h W AW) (hz : z ∈ Percolation.badSiteFinset M m h omega) (hconnU : Percolation.Connected₂ (Percolation.badSiteFinset M m h omega) z AU.index) (hconnW : Percolation.Connected₂ (Percolation.badSiteFinset M m h omega) z AW.index) (hdiam : ↑(Percolation.badClusterDiam M m h omega z) < 3 ^ (b * ↑h)) : ‖HCPolySupport.cubeCenter U - HCPolySupport.cubeCenter W‖ < 3 ^ (b * ↑h) * 3 ^ (m - ↑h)

The physical diameter estimate at the lift scale. Two Whitney cubes whose lifts are 2-connected inside the bad site set of a common base site z have centres less than 3^{bh}·3^{m-h} apart: the manuscript's first inequality, read between cube centres.

The core: the component occupies at most two layers

The headline statements

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyNeighborhood_layer_index_close {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ whitneyPartition m (whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ S) {A D : HCPolySupport.TriadicCube d} {nA nD : ℕ} (hA : A ∈ whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) (hD : D ∈ whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) (hAn : A ∈ whitneyLayer m (whitneyScaleSeq b hs k₀) nA) (hDn : D ∈ whitneyLayer m (whitneyScaleSeq b hs k₀) nD) : nA ≤ nD + 1 ∧ nD ≤ nA + 1

l.bad.clusters.geometry(1), the pairwise form. On avoidance of the bad-cluster diameter failure, any two Whitney cubes in the closure-touching neighborhood of one connected component of an abstract bad family occupy equal or neighbouring Whitney layers.

The family S is any subfamily of 𝒲(□_m) all of whose cubes are bad; the manuscript's ℐ is the instance badFamily_whitneyNeighborhood_finite_and_mem_leastLayer_or_succ below.

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyNeighborhood_finite_and_mem_leastLayer_or_succ {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ whitneyPartition m (whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ S) : (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)).Finite ∧ ∀ R ∈ whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀), R ∈ whitneyLayer m (whitneyScaleSeq b hs k₀) (leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀))) ∨ R ∈ whitneyLayer m (whitneyScaleSeq b hs k₀) (leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) + 1)

l.bad.clusters.geometry(1), the layer form. The neighborhood of a connected component of an abstract bad family is finite and contained in its least occupied Whitney layer together with that layer's successor: the manuscript's "every 2-connected component intersects at most two consecutive layers".

The concrete bad family

theorem Algsuperdiff.Section3.Provider.Whitney.badFamily_whitneyNeighborhood_finite_and_mem_leastLayer_or_succ {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ badFamily M m (whitneyScale M m E b k₀ omega) omega) : (whitneyNeighborhood m (whitneyScale M m E b k₀ omega) (badComponent (badFamily M m (whitneyScale M m E b k₀ omega) omega) Q₀)).Finite ∧ ∀ R ∈ whitneyNeighborhood m (whitneyScale M m E b k₀ omega) (badComponent (badFamily M m (whitneyScale M m E b k₀ omega) omega) Q₀), R ∈ whitneyLayer m (whitneyScale M m E b k₀ omega) (leastWhitneyLayer m (whitneyScale M m E b k₀ omega) (whitneyNeighborhood m (whitneyScale M m E b k₀ omega) (badComponent (badFamily M m (whitneyScale M m E b k₀ omega) omega) Q₀))) ∨ R ∈ whitneyLayer m (whitneyScale M m E b k₀ omega) (leastWhitneyLayer m (whitneyScale M m E b k₀ omega) (whitneyNeighborhood m (whitneyScale M m E b k₀ omega) (badComponent (badFamily M m (whitneyScale M m E b k₀ omega) omega) Q₀)) + 1)

The concrete instance at the manuscript's own bad family ℐ = badFamily M m h_n omega, with the avoidance binder discharged by the proved e.diameter.deterministic (Percolation.badClusterDiam_lt_of_hsep_le).