UnionBounds #

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

Union bounds for the bad events of ABK26, Section 3.3 #

This module assembles the two per-event probability bounds of l.bad.event.probabilities (ABK26) into bounds for the three composite events of sss.bad.cubes:

B_osc(z + square_j) — the scale union union_{L > j} B_{osc,L}(z+square_j) of e.Bosc.decomp;
B(z + square_j) = B_osc union B_loc of e.B.def;
B^*(z + square_j) — the nine-generation extension of e.Bext.def.

The last is the object whose probability enters the density threshold of l.percolation.bad.clusters (e.density.bound.bad.clusters, ABK26).

The oscillation union bound #

The summation is elementary: writing kappa = delta_osc(d)^2 c_star gamma^{-1} / 25 for the rate of measureReal_badOscAt_le, the manuscript's admissibility gate unitGate (supplied by unitGate_of_admissible) says exactly 1 <= kappa, and

sum_{n >= 1} exp(- kappa 3^{2(4/5 - gamma) n}) <= sum_{n >= 1} exp(- 3 kappa n)
                                              <= exp(- kappa) .

No hypothesis beyond the gate that measureReal_badOscAt_le already carries is used.

Gates carried #

Every statement below that consumes the local branch carries the same gate verbatim and adds nothing else. The bound E^{-2} <= c_star, used to express the oscillation rate through E, is the manuscript's own admissibility E >= C c_star^{-1} at C >= 1 together with E >= 1.