MinimalScaleSeparation

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

p.minimal.scale.separation: the minimal scale separation for bad clusters

This module provides the threshold and tail ingredients used toward ABK26's Proposition p.minimal.scale.separation: the function hsep above which both deterministic bad-cluster bounds hold, its defining characterizations, and its Gamma-tail.

The carrier of hsep

The manuscript defines hsep as the infimum of the set of j in N_0 above which both deterministic bounds hold at every scale h >= j, with the value infinity when no such j exists. Here:

hsepSet omega := { j : 1 <= j and every h >= j is good } ,
hsep omega    := sInf (hsepSet omega) .

hsepSet is upward closed, so hsep is the manuscript's threshold and the conclusion "every h >= hsep is good" is correct by construction — this is badClusterDiam_lt_of_hsep_le and badExtendedDensity_le_of_hsep_le. Two disclosures come with the carrier.

• The manuscript's hsep ranges over N_0; ours is >= 1 whenever it is meaningful, because the proved per-scale conclusions are stated for h >= 1 (the manuscript's own h in N convention in l.percolation.bad.clusters). Both consumers use hsep additively (e.hn.def), so the shift is immaterial.
• On the event where no j works, sInf empty = 0 is a junk value. That event is exactly {omega : not (hsepSet omega).Nonempty}, it is carried explicitly in every probabilistic statement (through scaleSeparationFail_eq), and it is null (measureReal_hsepSet_not_nonempty_of_gates).

Units

Everything is in the cube-side units of BadClusters.lean and BadClusterDiameter.lean: the lattice 3^{m-h} Z^d cap cu_m is cubeFinset h through z = 3^{m-h} u, and the printed diameter threshold 3^{bh} 3^{m-h} is 3^{bh}.

The tail constant

The manuscript's proof bounds P[hsep >= j] by a union bound over h >= j and then writes <= C exp(-3^{(1-sigma) b j}). The geometric constant of that union bound is (1 - exp(-(1-sigma) b log 3))^{-1}, which is not bounded by any C(d): it blows up as (1-sigma) b -> 0. It is carried here explicitly as hsepTailConst sigma b, and the amplitude of the resulting Gamma_{1-sigma} bound is hsepAmplitude sigma b, the paper's own C(sigma, b).

Main results

• hsep, hsepSet: the definition, with hsepSet_upward, one_le_hsep_iff, hsep_le_of_mem, mem_hsepSet_iff_hsep_le.
• badClusterDiam_lt_of_hsep_le: e.diameter.deterministic.
• badExtendedDensity_le_of_hsep_le: e.density.deterministic.
• measureReal_scaleSeparationFail_le_of_gates: the union bound of the proof from the exact raw probability gates.
• measureReal_hsepSet_not_nonempty_of_gates: hsep is a.s. well defined from the same gates.
• isBigOWith_gammaSigma_three_rpow_hsep_of_gates: e.hsep.tails at the explicit amplitude (departing from the printed 1, the escalation;: the amplitude C(σ,b) is adopted).
• The names without _of_gates are compatibility wrappers for the packaged preliminary admissibility.

Measurability and downstream use

The tex asserts hsep is a random variable. No Measurable statement is proved in this file. Every probability statement here goes through measure_mono / measure_iUnion_le / measure_union_le, which hold for arbitrary sets, so all proved bounds are valid (outer-measure bounds, if anything stronger) regardless. The downstream consumer Multiscale/BfaPerCube.lean supplies measurable_hsep before integrating functions of this threshold. This separation of providers is not a claim that the exact source proposition has been frozen and proved.

References

• ABK26, p.minimal.scale.separation.

Elementary numerics

The geometric tail sum

The doubly exponential per-scale bounds exp(-3^{alpha h}) are summed over h >= j against the geometric ratio exp(-alpha log 3).

The good-scale predicate

noncomputable def Algsuperdiff.Section3.Provider.Percolation.scaleSeparationDensityThreshold {d : ℕ} (M : ABKModel d) (E : ℝ) (h : ℕ) : ℝ

The threshold of e.density.deterministic at separation h, with the dimension-only witness c(d) = siteRateBase d / 2 supplied by the proved density conclusion measureReal_badExtendedDensity_gt_le_exp.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Percolation.scaleSeparationGood {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (h : ℕ) (omega : Cutoff.CutoffSample d) : Prop

A scale separation h is good for omega when both deterministic bounds of p.minimal.scale.separation hold at h: the diameter bound e.diameter.deterministic (in cube-side units) and the density bound e.density.deterministic.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Percolation.badClusterDiamFail {d : ℕ} (M : ABKModel d) (m : ℤ) (b : ℝ) (h : ℕ) : Set (Cutoff.CutoffSample d)

The event of e.diameter.bound.bad.clusters: the diameter bound fails at separation h.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Percolation.badExtendedDensityFail {d : ℕ} (M : ABKModel d) (m : ℤ) (E : ℝ) (h : ℕ) : Set (Cutoff.CutoffSample d)

The event of e.density.bound.bad.clusters: the density bound fails at separation h.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Percolation.notGood_subset_union {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (h : ℕ) : {omega : Cutoff.CutoffSample d | ¬scaleSeparationGood M m E b h omega} ⊆ badClusterDiamFail M m b h ∪ badExtendedDensityFail M m E h

The minimal scale separation

def Algsuperdiff.Section3.Provider.Percolation.hsepSet {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (omega : Cutoff.CutoffSample d) : Set ℕ

The set of admissible scale separations for omega: those j >= 1 above which every scale is good. It is upward closed (hsepSet_upward).

Equations

• Algsuperdiff.Section3.Provider.Percolation.hsepSet M m E b omega = {j : ℕ | 1 ≤ j ∧ ∀ (h : ℕ), j ≤ h → Algsuperdiff.Section3.Provider.Percolation.scaleSeparationGood M m E b h omega}

noncomputable def Algsuperdiff.Section3.Provider.Percolation.hsep {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (omega : Cutoff.CutoffSample d) : ℕ

On the null event where no such separation exists the sInf of the empty set gives the junk value 0; see measureReal_hsepSet_not_nonempty_of_gates.

Equations

• Algsuperdiff.Section3.Provider.Percolation.hsep M m E b omega = sInf (Algsuperdiff.Section3.Provider.Percolation.hsepSet M m E b omega)

theorem Algsuperdiff.Section3.Provider.Percolation.mem_hsepSet_iff {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} {j : ℕ} : j ∈ hsepSet M m E b omega ↔ 1 ≤ j ∧ ∀ (h : ℕ), j ≤ h → scaleSeparationGood M m E b h omega

theorem Algsuperdiff.Section3.Provider.Percolation.hsepSet_upward {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} {j k : ℕ} (hj : j ∈ hsepSet M m E b omega) (hjk : j ≤ k) : k ∈ hsepSet M m E b omega

theorem Algsuperdiff.Section3.Provider.Percolation.hsep_le_of_mem {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} {j : ℕ} (hj : j ∈ hsepSet M m E b omega) : hsep M m E b omega ≤ j

theorem Algsuperdiff.Section3.Provider.Percolation.hsep_mem {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} (hne : (hsepSet M m E b omega).Nonempty) : hsep M m E b omega ∈ hsepSet M m E b omega

theorem Algsuperdiff.Section3.Provider.Percolation.one_le_hsep_iff {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} : 1 ≤ hsep M m E b omega ↔ (hsepSet M m E b omega).Nonempty

hsep is meaningful exactly where it is positive.

theorem Algsuperdiff.Section3.Provider.Percolation.mem_hsepSet_iff_hsep_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} {j : ℕ} : j ∈ hsepSet M m E b omega ↔ 1 ≤ hsep M m E b omega ∧ hsep M m E b omega ≤ j

The defining characterization: for j >= 1, membership of j in the admissible set is exactly the assertion that hsep is meaningful and at most j.

theorem Algsuperdiff.Section3.Provider.Percolation.badClusterDiam_lt_of_hsep_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} (hne : (hsepSet M m E b omega).Nonempty) {h : ℕ} (hh : hsep M m E b omega ≤ h) {u : Fin d → ℤ} (hu : u ∈ cubeFinset h) : ↑(badClusterDiam M m h omega u) < 3 ^ (b * ↑h)

ABK26 e.diameter.deterministic, in cube-side units: max_{z} diam(B^*_{m-h}(z;2)) < 3^{bh} for every h >= hsep.

theorem Algsuperdiff.Section3.Provider.Percolation.badExtendedDensity_le_of_hsep_le {d : ℕ} {M : ABKModel d} {m : ℤ} {E b : ℝ} {omega : Cutoff.CutoffSample d} (hne : (hsepSet M m E b omega).Nonempty) {h : ℕ} (hh : hsep M m E b omega ≤ h) : badExtendedDensity M m h omega ≤ scaleSeparationDensityThreshold M E h

ABK26 e.density.deterministic: avsum_{z} 1_{B^*(z + cu_{m-h})} <= exp(-c E^{-2} gamma^{-1}) + 3^{-h/2} for every h >= hsep.

The tail of hsep

def Algsuperdiff.Section3.Provider.Percolation.scaleSeparationFail {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (j : ℕ) : Set (Cutoff.CutoffSample d)

The failure event at level j: some scale h >= j is not good. For j >= 1 this is exactly the complement of {hsep is meaningful and <= j} (scaleSeparationFail_eq).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Percolation.scaleSeparationFail_eq {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) {j : ℕ} (hj : 1 ≤ j) : scaleSeparationFail M m E b j = {omega : Cutoff.CutoffSample d | ¬(1 ≤ hsep M m E b omega ∧ hsep M m E b omega ≤ j)}

noncomputable def Algsuperdiff.Section3.Provider.Percolation.hsepTailConst (sigma b : ℝ) : ℝ

The geometric constant of the union bound over h >= j. It is not dimension-only: it diverges as (1-sigma) b -> 0.

Equations

• Algsuperdiff.Section3.Provider.Percolation.hsepTailConst sigma b = (1 - Real.exp (-((1 - sigma) * b * Real.log 3)))⁻¹ + (1 - Real.exp (-(1 / 2 * Real.log 3)))⁻¹

theorem Algsuperdiff.Section3.Provider.Percolation.two_le_hsepTailConst {sigma b : ℝ} (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) : 2 ≤ hsepTailConst sigma b

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_scaleSeparationFail_le_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) {j : ℕ} (hj : 1 ≤ j) : (↑(Cutoff.cutoffSampleLaw M)).real (scaleSeparationFail M m E b j) ≤ hsepTailConst sigma b * Real.exp (-3 ^ ((1 - sigma) * b * ↑j))

The tail of the minimal scale separation (ABK26). The union bound over `h

= jof the two conclusions ofl.percolation.bad.clusters`:

P[ some scale h >= j fails ]  <=  C(sigma,b) exp(-3^{(1-sigma) b j}) ,

and, by scaleSeparationFail_eq, the left-hand side is exactly P[ not (hsep is meaningful and hsep <= j) ].

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_hsepSet_not_nonempty_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | ¬(hsepSet M m E b omega).Nonempty} = 0

hsep is almost surely well defined. The event on which no admissible scale separation exists — the event carrying the junk value sInf empty = 0 — is null. This is the well-definedness that the manuscript's max convention silently assumes.

e.hsep.tails

noncomputable def Algsuperdiff.Section3.Provider.Percolation.hsepAmplitude (sigma b : ℝ) : ℝ

The amplitude of the Gamma_{1-sigma} bound of e.hsep.tails. The manuscript prints the amplitude 1; the union bound of its own proof supports only a constant absorbing hsepTailConst.

Equations

• Algsuperdiff.Section3.Provider.Percolation.hsepAmplitude sigma b = 3 + 2 * (1 + Real.log (Algsuperdiff.Section3.Provider.Percolation.hsepTailConst sigma b)) ^ 2

The amplitude arithmetic

Two purely real-analytic steps, isolated so that neither elaboration exceeds the default heartbeat budget.

theorem Algsuperdiff.Section3.Provider.Percolation.isBigOWith_gammaSigma_three_rpow_hsep_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (1 - sigma)) (fun (omega : Cutoff.CutoffSample d) => 3 ^ (b * ↑(hsep M m E b omega))) (hsepAmplitude sigma b)

ABK26 e.hsep.tails at the explicit amplitude:

3^{b hsep}  <=  O_{Gamma_{1-sigma}}( hsepAmplitude sigma b ) ,

i.e. P[ 3^{b hsep} > hsepAmplitude sigma b * s ] <= exp(-s^{1-sigma}) for every s >= 1.