CollarMass

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

The collar-vs-bad mass comparison: hmasscol discharged

LayerUniform.sum_sum_ofReal_two_leg_le_ofReal_layerContrib and its concrete twin ConclusionCompetitor.toReal_tsum_simplexPartition_cutoff_two_leg_le_payload price the collar leg of e.sum-of-a-decomp (ABK26) by the free sequence Bad, through the caller-supplied datum

hmasscol : ∀ n, ∑ □ ∈ collarLayer M m hn n omega, |□| / |□_m| ≤ Bad n .

LayerUniform's module docstring discloses this as a remaining step of Step 3 ("The mass comparison. is NOT proved here and is NOT assumed to be true"). This module proves it, at the proved carrier and with an explicit dimension-only constant and an explicit layer window.

The mathematics

The collar family of layer n is collarLayer = 𝒩(ℐ) ∩ 𝒲(□_m,n), the Whitney cubes of layer n that touch a bad cube (e.neighborhood.def, at the cubewise reading ∃ □' ∈ ℐ, dist(□,□') = 0; the printed reading agrees on the finite families the manuscript uses, ClusterLayerConstraint's reconciliation). Two geometric facts turn its mass into bad mass.

1. The layer window. A layer-n cube touching a layer-j cube forces `|n
   • j| ≤ 1---BoundaryDistance.whitneyLayer_index_close_of_cubeTouch, the adjacency clause (second sentence; pin corrected), proved's two-sided boundary distance with **no** percolation input and **no** connectivity. With e.hn.def/e.hn.gap(/5937:hnondecreasing,h_{j+1} ≤ h_j + 1) the *depth* gap is then |(n + h_n) - (j + h_j)| ≤ 2 (layerDepth_sub_le_two), which is exactly the ±2`-generation window, here derived from the touch relation rather than assumed from the scale.
2. The bounded overlap. Fix a bad cube R of layer j. Every layer-n cube Q touching R has, in every coordinate, |Q.index i - R.index i · 3^{scale R - scale Q}| ≤ (1 + 3^{scale R - scale Q})/2 ≤ 5 (abs_index_sub_mul_zpow_le_five), so its index lies in an explicit box of 11 integers per coordinate; distinct cubes of one layer have distinct indices, whence at most 11^d of them (card_le_eleven_pow_of_forall_cubeTouch). Each of them carries mass at most 9^d times the mass of R (cubeMassRatio_le_nine_pow_mul, the same ±2 depth window). Choosing for each collar cube one bad cube it touches and summing fibrewise gives the constant 11^d · 9^d = 99^d.

The conclusion (sum_cubeMassRatio_collarLayer_le) is

∑_{□ ∈ 𝒩(ℐ) ∩ 𝒲(□_m,n)} |□|/|□_m|
    ≤ 99^d · ∑_{j = n-1}^{n+1} ∑_{□ ∈ ℐ_j} |□|/|□_m| .

Composed with the proved mass form of l.bad.cubes.density (ConclusionAssembly.sum_cubeMassRatio_badFamilyLayer_le_layerQuantity, i.e.) and the same depth window, this becomes the consumer-shaped

∑_{□ ∈ 𝒩(ℐ) ∩ 𝒲(□_m,n)} |□|/|□_m|
    ≤ 9 · 99^d · ( exp(-c(d) E^{-2} γ^{-1}) + 3^{-(n+h_n)/2} )

(sum_cubeMassRatio_collarLayer_le_layerQuantity). The sharper split the proof actually establishes is 99^d · (3·exp(...) + 9·3^{-(n+h_n)/2}); 9·99^d is the clean common majorant, and 9 is 3 (the three layers of the window) times 3 (the at most two generations of depth a window layer can lose).

What the consumer must do with it

Bad is a free sequence in toReal_tsum_simplexPartition_cutoff_two_leg_le_payload, constrained there by hBad0, hBadMass : Bad j ≤ Cmass·3^{-j} and hBadDens: Bad j ≤ ε + 3^{-(j+h_j)/2}. Since hmasscol : ∀ n, ∑_{collar} ≤ Bad n does not mention Ccol, the constant cannot be folded there; the route is

Bad j := 9·99^d · ( exp(-c(d) E^{-2} γ^{-1}) + 3^{-(j+h_j)/2} ) ,

with which hmasscol IS sum_cubeMassRatio_collarLayer_le_layerQuantity verbatim. The remaining bookkeeping, named and NOT discharged here: (a) hBadDens carries coefficient exactly 1 on the 3^{-·/2} term, so re-establishing it at this Bad needs a shift of the consumer's own free (hs, k₀) pair (the manuscript's k₀ := c E^{-2} γ^{-1} absorbs dimension-only factors by shrinking c); (b) hBadMass : Bad j ≤ Cmass·3^{-j} fails for large j at any j-constant ε-term, and no Cmass re-selection and no per-binder split can restore it --- the feasible route is Bad j:= min(9·99^d·(A + 3^{-L_j/2}), Cmass·3^{-j}), whose second branch follows from collarLayer_subset + hmassgood + hMass, all already in the consumer's slot. Both are the consumer's, and the dimension-only constant is absorbed by the C_col ↦ C·C_col reconciliation (performed here on the Bad slot rather than on Ccol). No printed density input is strengthened: the right-hand side is the printed l.bad.cubes.density threshold, read at the three layers of the window.

Main results

• abs_index_sub_mul_zpow_le_five, card_le_eleven_pow_of_forall_cubeTouch: the dimension-only overlap count 11^d at the cubewise touch relation.
• layerDepth_sub_le_two: the ±2 depth window.
• sum_cubeMassRatio_collarLayer_le: the obligation, at 99^d and the three-layer window n-1, n, n+1.
• sum_cubeMassRatio_collarLayer_le_layerQuantity: the same priced by l.bad.cubes.density, in the Bad n shape the consumer instantiates.

References

• ABK26, sss.whitney.partition (e.hn.def, e.hn.gap, e.W.n.def, e.bad.cubes.in.partition, e.neighborhood.def); l.bad.clusters.geometry (the adjacency clause); l.bad.cubes.density; Step 3 of p.bfA.multiscalebound (the collar family 𝒩(ℐ) ∩ 𝒲(□_n,k)).

Index localization of a touching pair

theorem Algsuperdiff.Section3.Provider.Multiscale.abs_index_sub_mul_zpow_le_five {d : ℕ} {Q R : HCPolySupport.TriadicCube d} (hsc : R.scale - Q.scale ≤ 2) (htouch : Whitney.CubeTouch Q R) (i : Fin d) : |↑(Q.index i) - ↑(R.index i) * 3 ^ (R.scale - Q.scale)| ≤ 5

Index localization of a touching pair. If the closed cubes □ and □' meet (e.neighborhood.def's dist(□,□') = 0) and □' is at most two generations coarser, then the index of □ sits within 5 of the rescaled index of □' in every coordinate: the touch inequality |x·3^{s} - y·3^{s'}| ≤ (3^{s} + 3^{s'})/2 divided by 3^{s} reads |x - y·3^{s'-s}| ≤ (1 + 3^{s'-s})/2 ≤ 5.

theorem Algsuperdiff.Section3.Provider.Multiscale.card_le_eleven_pow_of_forall_cubeTouch {d : ℕ} {sQ : ℤ} {R : HCPolySupport.TriadicCube d} {A : Finset (HCPolySupport.TriadicCube d)} (hsc : R.scale - sQ ≤ 2) (hA : ∀ Q ∈ A, Q.scale = sQ ∧ Whitney.CubeTouch Q R) : A.card ≤ 11 ^ d

The bounded-overlap count, the dimension-only C_d the manuscript folds into #𝒩(ℐ) ≤ C_d·#ℐ: at most 11^d cubes of one common scale sQ can touch a fixed cube R at most two generations coarser. Their indices lie in an explicit box of 11 integers per coordinate, and distinct cubes of a common scale have distinct indices.

theorem Algsuperdiff.Section3.Provider.Multiscale.cubeMassRatio_le_nine_pow_mul {d : ℕ} (m : ℤ) {Q R : HCPolySupport.TriadicCube d} (h : Q.scale - R.scale ≤ 2) : Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ 9 ^ d * Whitney.cubeMassRatio (HCPolySupport.originCube d m) R

Mass at comparable scales. A cube at most two generations finer than R carries at most 9^d = (3^d)^2 times the mass of R inside □_m.

The layer-index window

theorem Algsuperdiff.Section3.Provider.Multiscale.layerDepth_sub_le_two {hn : ℕ → ℕ} (hmono : Monotone hn) (hgap : ∀ (j : ℕ), hn (j + 1) ≤ hn j + 1) {n j : ℕ} (h1 : n ≤ j + 1) (h2 : j ≤ n + 1) : ↑n + ↑(hn n) - (↑j + ↑(hn j)) ≤ 2 ∧ -2 ≤ ↑n + ↑(hn n) - (↑j + ↑(hn j))

The ±2 depth window. For a nondecreasing scale profile obeying e.hn.gap, neighbouring layer indices sit at depths n + h_n differing by at most two: layer n-1 is coarser by 1 + (h_n - h_{n-1}) ∈ {1,2} and layer n+1 is finer by 1 + (h_{n+1} - h_n) ∈ {1,2}.

The collar mass comparison

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cubeMassRatio_collarLayer_le {d : ℕ} (M : ABKModel d) {m : ℤ} {hn : ℕ → ℕ} (hn1 : ∀ (j : ℕ), 1 ≤ hn j) (hmono : Monotone hn) (hgap : ∀ (j : ℕ), hn (j + 1) ≤ hn j + 1) (omega : Cutoff.CutoffSample d) (n : ℕ) : ∑ Q ∈ collarLayer M m hn n omega, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ 99 ^ d * ∑ j ∈ Finset.Icc (n - 1) (n + 1), ∑ R ∈ Whitney.badFamilyLayer M m hn j omega, Whitney.cubeMassRatio (HCPolySupport.originCube d m) R

The collar-vs-bad mass comparison --- the disclosed hmasscol obligation of LayerUniform and ConclusionCompetitor, discharged at the proved carrier:

∑_{□ ∈ 𝒩(ℐ) ∩ 𝒲(□_m,n)} |□|/|□_m|
    ≤ 99^d · ∑_{j = n-1}^{n+1} ∑_{□ ∈ ℐ_j} |□|/|□_m| .

The constant is 11^d (the overlap count) times 9^d (the mass ratio across the depth window) and is dimension-only; the window n-1, n, n+1 is exact, and comes from the adjacency clause through whitneyLayer_index_close_of_cubeTouch. No connectivity of ℐ, no disjointness of component neighborhoods and no percolation input is used.

The collar mass at the proved Whitney and percolation carriers

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cubeMassRatio_collarLayer_le_layerQuantity {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 1 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (n : ℕ) : ∑ Q ∈ collarLayer M m (Whitney.whitneyScale M m E b k₀ omega) n omega, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q ≤ 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(layerQuantity b (Percolation.hsep M m E b omega) k₀ n / 2)))

The collar mass priced by l.bad.cubes.density, in the shape the Step-3 consumer instantiates Bad n at:

∑_{□ ∈ 𝒩(ℐ) ∩ 𝒲(□_m,n)} |□|/|□_m|
    ≤ 9·99^d · ( exp(-c(d) E^{-2} γ^{-1}) + 3^{-(n+h_n)/2} ) .

The three layers of the window contribute the threshold at their own depths; each such depth is within two generations of n + h_n, costing a factor 3 on 3^{-h/2}, so the regrouping constant is 3·3 = 9 (the sharper split the proof establishes is 3·exp(...) + 9·3^{-(n+h_n)/2}). The dimension-only factor 9·99^d is carried on the consumer's Bad slot (the C·C_col reconciliation; it cannot literally fold into Ccol --- see the consumer note above); the printed density input is not strengthened.