BadClusterDiameter

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

e.diameter.bound.bad.clusters: the diameter conclusion at the ruled adjacency

P[ max_{z in 3^{m-h} Z^d cap cu_m} diam( B^*_{m-h}(z;2) ) >= 3^{bh} 3^{m-h} ]
  <= exp( - 3^{(1-sigma) b h} ) .

The three ingredients are

• the distance-two abstract percolation layer of LatticeTwo, ClusterEventTwo, DiameterTwo (the ruled re-run of the diameter induction, at the same gate constant 16 d exp(40 (1-b)^{-1}) <= T^2 b as the proved distance-one layer);
• the 2-cluster definitions and the deterministic step of ClusterTwo;
• the proved site family, its tails and its finite-range independence (SiteFamily, SiteFamilyTails, SiteFamilyBridge) and the gate arithmetic of BadClusterRate.

Units

Everything is in cube-side units: the base lattice 3^{m-h} Z^d cap cu_m is the Finset cubeFinset h through z = 3^{m-h} u, and badClusterDiam is the sup-metric diameter of the union of the closed base cubes of the 2-cluster, divided by the cube side 3^{m-h}. The printed threshold 3^{bh} 3^{m-h} becomes 3^{bh}.

The scale of the crossing, and the constant that pays for it

The source says the diameter bound "follows from e.diameter.bound (rescaled)". That step is a gloss: a cluster of diameter D produces a crossing of the annulus cu_{k+1} \ cu_k only when 3^{k+1} <= 2 D, so the crossing scale k must sit strictly below b h, whereas the gain of e.diameter.bound at scale k is 3^{(1-sigma) k} and the target is 3^{(1-sigma) b h}. Here k is taken to be ceil(b h) - 2, which loses a factor at most 9 in the gain; the loss is paid for out of the admissibility display, not by weakening the conclusion: entropyGate₂_of_admissible extracts (3 + 18 d) / b <= exp(-40/sigma) T^2 / 2 from the same amended display e.percolation.admissibility.bad.clusters (E >= C b^{-1}) at the same dimension-only badClustersConst d, where the proved entropyGate_of_admissible extracts only 1 + 2 d / b. No constant of the node moves, and no hypothesis is added.

For b h <= 1 the crossing route is unavailable (a cluster of diameter < 3 crosses no annulus) and the bound is obtained instead by the plain union bound over the 3^{dh} base sites, which in that regime (h <= b^{-1}) is dominated by the same gate.

Main definitions

• badSiteFinset, badCluster₂, badClusterDiam: the random site set B^*_{m-h} of e.bad.cluster.def, its 2-clusters B^*_{m-h}(z;2) and their diameter in cube-side units.
• badClusterCrossingEvent₂: the union over the base lattice of the distance-two crossing events at a given scale.

Main results

• entropyGate₂_of_admissible: the sharpened entropy gate.
• measureReal_badClusterCrossingEvent₂_le_exp_of_gates: the crossing-union bound at any scale k whose gain is within a factor 9 of the target, from the exact raw probability gates.
• measureReal_maxBadClusterDiam_le_exp_of_gates: e.diameter.bound.bad.clusters from those gates.
• The names without _of_gates are compatibility wrappers for the packaged preliminary admissibility.

References

• ABK26, l.percolation.bad.clusters.

The sharpened entropy gate

theorem Algsuperdiff.Section3.Provider.Percolation.entropyGate₂_of_admissible {d : ℕ} (M : ABKModel d) {E sigma b : ℝ} (hd : 2 ≤ d) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hE : Real.exp (badClustersConst d / sigma) ≤ E) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : (6 + 36 * ↑d) * Real.exp (40 / sigma) / b ≤ siteRateSq M E

The proved entropyGate_of_admissible extracts 2 (1 + 2 d) e^{40/sigma} b^{-1} from the same display; the extra room is what pays for the bounded scale loss in the cluster-to-crossing step.

theorem Algsuperdiff.Section3.Provider.Percolation.gainGate₂_of_admissible {d : ℕ} (M : ABKModel d) {E sigma b : ℝ} (hd : 2 ≤ d) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hE : Real.exp (badClustersConst d / sigma) ≤ E) (hEb : badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : (3 + 18 * ↑d) / b ≤ Real.exp (-(40 / sigma)) * siteRateSq M E / 2

The gate in the form consumed by the union bound: the gain constant G = e^{-40/sigma} T^2 / 2 dominates (3 + 18 d) b^{-1}.

The entropy of the base lattice

The random site set and its 2-clusters

noncomputable def Algsuperdiff.Section3.Provider.Percolation.badSiteFinset {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (omega : Cutoff.CutoffSample d) : Finset (Fin d → ℤ)

ABK26 e.bad.cluster.def: the random set B^*_{m-h} = { z + cu_{m-h}: z in 3^{m-h} Z^d cap cu_m, B^*(z + cu_{m-h}) occurs }, in cube-side units z = 3^{m-h} u.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.mem_badSiteFinset_iff {d : ℕ} {M : ABKModel d} {m : ℤ} {h : ℕ} {omega : Cutoff.CutoffSample d} {u : Fin d → ℤ} : u ∈ badSiteFinset M m h omega ↔ u ∈ cubeFinset h ∧ omega ∈ BadEvents.badExtended M (siteCube (m - ↑h) u)

theorem Algsuperdiff.Section3.Provider.Percolation.badSiteFinset_subset {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (omega : Cutoff.CutoffSample d) : badSiteFinset M m h omega ⊆ cubeFinset h

noncomputable def Algsuperdiff.Section3.Provider.Percolation.badCluster₂ {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (omega : Cutoff.CutoffSample d) (u : Fin d → ℤ) : Finset (Fin d → ℤ)

ABK26 e.bad.cluster.def: the 2-connected component B^*_{m-h}(z;2) of the bad base cubes containing z + cu_{m-h} if B^*(z + cu_{m-h}) occurs, and the empty set otherwise (the latter is cluster₂_eq_empty_of_notMem).

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Percolation.badClusterDiam {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (omega : Cutoff.CutoffSample d) (u : Fin d → ℤ) : ℕ

diam(B^*_{m-h}(z;2)) in units of the cube side 3^{m-h}: the sup-metric diameter of the union of the closed base cubes of the 2-cluster.

Equations

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

The crossing-union bound at a general scale

def Algsuperdiff.Section3.Provider.Percolation.badClusterCrossingEvent₂ {d : ℕ} (M : ABKModel d) (m : ℤ) (h k : ℕ) : Set (Cutoff.CutoffSample d)

The union over the base lattice 3^{m-h} Z^d cap cu_m of the distance-two crossing events of e.diameter.bound at scale k.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_badClusterCrossingEvent₂_le_exp_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} (h : ℕ) {E sigma b : ℝ} (hd : 2 ≤ d) (hh : 1 ≤ h) (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)) (k : ℕ) (hk : 3 ^ ((1 - sigma) * b * ↑h) ≤ 9 * 3 ^ ((1 - sigma) * ↑k)) : (↑(Cutoff.cutoffSampleLaw M)).real (badClusterCrossingEvent₂ M m h k) ≤ Real.exp (-3 ^ ((1 - sigma) * b * ↑h))

The crossing-union bound for distance-two crossings.

At any scale k whose gain 3^{(1-sigma) k} is within a factor 9 of the target 3^{(1-sigma) b h}, the probability that some base site starts a distance-two crossing of its own annulus at scale k is at most exp(-3^{(1-sigma) b h}), uniformly in h.

The diameter conclusion

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_maxBadClusterDiam_le_exp_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} (h : ℕ) {E sigma b : ℝ} (hd : 2 ≤ d) (hh : 1 ≤ h) (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 | ∃ u ∈ cubeFinset h, 3 ^ (b * ↑h) ≤ ↑(badClusterDiam M m h omega u)} ≤ Real.exp (-3 ^ ((1 - sigma) * b * ↑h))

ABK26 e.diameter.bound.bad.clusters, at the AUTHOR-adjacency and from the raw single-cube probability gates:

P[ max_{z in 3^{m-h} Z^d cap cu_m} diam( B^*_{m-h}(z;2) ) >= 3^{bh} 3^{m-h} ]
  <= exp( - 3^{(1-sigma) b h} ) ,

in cube-side units (badClusterDiam is diam(B^*_{m-h}(z;2)) / 3^{m-h}), where diam is the sup metric and the 2-cluster is the one of e.bad.cluster.def read at lattice sup distance <= 2.

The manuscript's own a = 3/2 in the companion density bound forces d >= 2, and h >= 1 is ABK's N convention; both are carried as disclosed binders.