BadClusterRate #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The amended bad-cluster admissibility and the gates it discharges #
ABK26's Lemma l.percolation.bad.clusters applies the abstract percolation
lemma at the rate T^2 = c E^{-2} gamma^{-1} under the printed admissibility
display e.percolation.admissibility.bad.clusters
E >= exp(C sigma^{-1}) or C c_star^{-1} and gamma <= E^{-5} .
The additional admissibility requirement #
E >= C b^{-1} ,
with C = C(d) still dimension-only, so the node contract'sC depends only on d stands unchanged. The reason is the diameter half: the conclusion needs a
union bound over ~3^{dh} lattice translates of the crossing event, uniformly
in h, and paying the entropy d h log 3 against the gain e^{-40/sigma} T^2 3^{(1-sigma) b h} for ALL h requires (through sup_h h 3^{-(1-sigma) b h} <= ((1-sigma) b log 3)^{-1}) a rate of strength T^2 >~ d e^{40/sigma} b^{-1}.
The printed display is b-free and cannot supply the b^{-1}.
Why the rate is not the sharp oscillation rate #
The site family of l.percolation.bad.clusters is a union over the
nine-generation descendant tree of two branches, so its honest per-scale rate
is badRateConst d / 2 = min(delta_osc^2/25, 1/512)/2
(SiteFamilyTails.lean), further discounted by the reindexing shift. This
module therefore re-derives every gate at the true rate siteRateSq, reusing
only the rate-agnostic lemmas densityThreshold_of_le and
one_le_densityExponent of BadClusterGates.lean.
Main definitions #
badClustersAmplitude: the dimension-only quantity all gates are measured against.badClustersConst: the explicitC(d)of the amended admissibility display.
Main results #
le_cube_of_admissible: the master arithmetic stepA e^{40/sigma} b^{-1} <= E^3.treeCountGate_of_admissible,four_le_siteRateSq,percolationGate_of_admissible',densityAmplitude_le_sqrt_siteRateSq,densityExponentAmplitude_le_siteRateSq,entropyGate_of_admissible: the six gates of the node, all atbadClustersConst d.
References #
- ABK26,
l.percolation.bad.clusters.
The dimension-only amplitude and constant #
The dimension-only quantity that every gate of the node is measured
against. The first summand is the descendant-tree count gate of
SiteFamilyTails; the second collects the five gates that are lower bounds on
the reindexed rate siteRateSq.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The explicit dimension-only C(d) of the amended admissibility display
e.percolation.admissibility.bad.clusters (as amended).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Positivity of the amplitude's ingredients #
The bracket of the second summand of badClustersAmplitude.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The master arithmetic step #
The master step. The amended admissibility at badClustersConst d
turns any dimension-only amplitude A into the bound
A e^{40/sigma} b^{-1} <= E^3. The e^{40/sigma} comes from E >= exp(C/sigma)
and sigma <= 1/2; the b^{-1} comes from the additional
requirement E >= C b^{-1}.
The master step with the b^{-1} slack discarded.
The master step with both slacks discarded.
The standing consequences of the amended display #
The six gates at the true rate #
Gate 1: the descendant-tree count. The gate hEabs of
measureReal_badScaleEvent_le.
Gate 2: the unit rate. The abstract percolation layer needs T >= 1;
the amended admissibility gives the stronger T^2 >= 4.
Gate 3: the percolation threshold, at the manuscript's own conclusion
exponent b = 1 - sigma of e.diameter.bound and at the T rate siteRateSq.
Gate 4: the density range. The amplitude of densityThreshold_of_le at
the manuscript's a = 3/2.
Gate 5: the exponent. The amplitude of one_le_densityExponent.
Gate 6: the entropy-versus-gain gate. This is the gate that the printed
b-free admissibility cannot supply and that the additional requirement `E
= C b^{-1}` does.