SiteFamilyTails

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

The per-scale tails of the site family of l.percolation.bad.clusters

ABK26's proof of l.percolation.bad.clusters asserts, for the scale-resolved bad events B_L(z + cu_{m-h}) of SiteFamily.lean, the probability bounds

P[ B_L(z + cu_{m-h}) ] <= exp( - T^2 3^{(3/2) L} )    for all L in N_0 ,

with the manuscript's own rate T^2 = c_{e.BoscL.prob} E^{-2} gamma^{-1}.

c_{e.BoscL.prob}  ->  badRateConst d / 2 ,
badRateConst d = min( delta_osc(d)^2 / 25 , 1 / 512 ) ,

the halving being the absorption of the <= 10 * 3^{9d} descendant-tree count of e.Bext.def (exactly the absorption already performed by measureReal_badExtended_le_exp, at the same explicit gate hEabs).

What each level uses

• Level 0 is the union of B_loc over the nine-generation tree; each member obeys e.Bloc.prob at rate 1/512 (measureReal_badLoc_le), and badRateConst d <= 1/512.
• Level l + 1 is the union of the single-shell oscillation events B_{osc, R.scale + l + 1}(R) over the same tree; each member obeys e.BoscL.prob at rate delta_osc(d)^2/25 with shell offset l + 1 independently of the generation i (this is the manuscript's own indexing m - h - i + L), and badRateConst d <= delta_osc(d)^2 / 25.

The count is absorbed once, uniformly in l, because the per-scale exponent 3^{(3/2) l} is at least one.

The reindexed family

SiteFamilyBridge.siteBadEvent shifts the levels by sepShift d = d in order to meet the literal separation hypothesis of the proved cutoff range lemma. The shift costs exactly the factor 3 ^ (-(3/2) * sepShift d) in the tail parameter, and nothing else; the resulting parameter is siteRateSq.

Main definitions

• siteRateBase: the dimension-only prefactor badRateConst d / 2 * 3 ^ (-(3/2) sepShift d).
• siteRateSq: the tail parameter T'^2 of the reindexed family.

Main results

• measureReal_badScaleEvent_le_of_gates: the manuscript's per-scale display at the corrected rate from the exact four probability gates.
• measureReal_siteBadEvent_le_of_gates: the same after the reindexing, in exactly the shape htail of the abstract percolation layer.
• The names without _of_gates are compatibility wrappers for the packaged preliminary admissibility.

References

• ABK26, l.percolation.bad.clusters.
• ABK26, l.bad.event.probabilities.

Absorbing the descendant-tree count

The scale restriction of the admissibility

theorem Algsuperdiff.Section3.Provider.Percolation.cube_le_invSq_mul_gammaInv {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 1 ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : E ^ 3 ≤ E⁻¹ ^ 2 * M.gamma⁻¹

The printed scale restriction gamma <= E^{-5} upgrades the manuscript's rate factor E^{-2} gamma^{-1} to E^3.

The per-scale tails

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_badScaleEvent_le_of_gates {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {m : ℤ} {E : ℝ} (hE : 1 ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hj : Q.scale ≤ m - 1) (hgamma : M.gamma ≤ E ^ (-5)) (hEabs : 2 * (Real.log 20 + 9 * ↑d * Real.log 3) ≤ BadEvents.badRateConst d * E ^ 3) (l : ℕ) : (↑(Cutoff.cutoffSampleLaw M)).real (badScaleEvent M Q l) ≤ Real.exp (-(BadEvents.badRateConst d / 2 * E⁻¹ ^ 2 * M.gamma⁻¹ * 3 ^ (3 / 2 * ↑l)))

P[ B_l(z + cu_j) ] <= exp( - (badRateConst d / 2) E^{-2} gamma^{-1} 3^{(3/2) l} ) .

This direct form exposes exactly the four proof-side gates used by the two single-cube probability bounds. In particular it does not package them into the stronger preliminary admissibility C <= E * cstar.

The reindexed tail parameter

noncomputable def Algsuperdiff.Section3.Provider.Percolation.siteRateBase (d : ℕ) : ℝ

The dimension-only prefactor of the reindexed tail parameter: the corrected rate badRateConst d / 2, discounted by the disclosed reindexing shift sepShift d.

Equations

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

theorem Algsuperdiff.Section3.Provider.Percolation.siteRateBase_pos (d : ℕ) : 0 < siteRateBase d

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

The tail parameter T'^2 of the reindexed site family. This is the manuscript's T^2 = c E^{-2} gamma^{-1} at the corrected constant, discounted by the factor 3 ^ (-(3/2) sepShift d) that the disclosed reindexing costs.

Equations

• Algsuperdiff.Section3.Provider.Percolation.siteRateSq M E = Algsuperdiff.Section3.Provider.Percolation.siteRateBase d * (E⁻¹ ^ 2 * M.gamma⁻¹)

theorem Algsuperdiff.Section3.Provider.Percolation.measureReal_siteBadEvent_le_of_gates {d : ℕ} (M : ABKModel d) (base : ℤ) {m : ℤ} {E : ℝ} (hE : 1 ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hbase : base ≤ m - 1) (hgamma : M.gamma ≤ E ^ (-5)) (hEabs : 2 * (Real.log 20 + 9 * ↑d * Real.log 3) ≤ BadEvents.badRateConst d * E ^ 3) (l : ℕ) (u : Fin d → ℤ) : (↑(Cutoff.cutoffSampleLaw M)).real (siteBadEvent M base l u) ≤ Real.exp (-(siteRateSq M E * 3 ^ (3 / 2 * ↑l)))

The tail hypothesis of l.percolation.bound.general, discharged for the reindexed site family at the exponent a = 3/2 of the manuscript, from the raw proof-side gates.