ClusterGeometry

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

l.bad.clusters.geometry: the scale arithmetic of the cluster lemma

Partial node. This module delivers the carrier-free scale arithmetic on which the proof of ABK26's l.bad.clusters.geometry rests.

What is delivered

• whitneyScaleSeq_add_le and whitneyDepth_sub_lt_ten: the manuscript's generation count. The lift of a layer-n' cube to the coarsest scale 3^{m-n_min-h_{n_min}} in the region is a descendant within (n' + h_{n'}) - (n_min + h_{n_min}) generations, and the manuscript needs that number to be < 9 so that 𝓑(□) ⟹ 𝓑^*(□) (e.Bext.def looks at nine generations of descendants). With b ≤ 1/8 and n_min ≤ n' ≤ n_min + 3 the count is at most 6.
• four_mul_three_rpow_whitneyDepth_lt_two_thirds: the corrected gate

  4 · 3^{b(n+h_n)} · 3^{m-n-h_n}  <  (2/3) · 3^{m-n}    (b ≤ 1/8, k₀ ≥ 3).
  

  The manuscript writes 3^{b(n+h_n)}·3^{m-n-h_n} ≤ 3^{m-n}·3^{-(1-b)k₀} and then chooses k₀ with 3^{-(1-b)k₀} < c.

References

• ABK26, l.bad.clusters.geometry.

The generation count of the lift to 𝓑^*

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyScaleSeq_add_le {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hs k₀ r j : ℕ) : whitneyScaleSeq b hs k₀ (r + j) ≤ whitneyScaleSeq b hs k₀ r + j

Iterating e.hn.gap: the scale separation grows by at most one per layer.

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyDepth_sub_lt_ten {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hs k₀ : ℕ) {r n : ℕ} (hrn : r ≤ n) (hnr : n ≤ r + 3) : n + whitneyScaleSeq b hs k₀ n - (r + whitneyScaleSeq b hs k₀ r) < 10

The generation count. If two Whitney layers are at most three apart, the depth gap between them is smaller than ten, i.e. within the generations 0..9 of the proved e.Bext.def (Finset.range 10), so a bad layer-n cube forces the extended bad event at the coarser layer-r scale.

The layer-exclusion gate

theorem Algsuperdiff.Section3.Provider.Whitney.whitneyLayerExclusionExponent_le {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) {hs k₀ : ℕ} (hk₀ : 3 ≤ k₀) (n : ℕ) : b * ↑(n + whitneyScaleSeq b hs k₀ n) - ↑(n + whitneyScaleSeq b hs k₀ n) + ↑n ≤ -2

The exponent form: b(n+h_n) - (n+h_n) + n ≤ -2 whenever b ≤ 1/8 and k₀ ≥ 3.

theorem Algsuperdiff.Section3.Provider.Whitney.four_mul_three_rpow_whitneyDepth_lt_two_thirds {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) {hs k₀ : ℕ} (hk₀ : 3 ≤ k₀) (m : ℤ) (n : ℕ) : 4 * 3 ^ (b * ↑(n + whitneyScaleSeq b hs k₀ n)) * 3 ^ (m - ↑(n + whitneyScaleSeq b hs k₀ n)) < 2 / 3 * 3 ^ (m - ↑n)

4 · 3^{b(n+h_n)} · 3^{m-n-h_n}  <  (2/3) · 3^{m-n} .