OAI/Analysis/RieszRectifiability/Foundations/UniformBilateralExcessPropagation.lean

Uniform bilateral excess propagation

The conclusion combines a squared-excess estimate with bilateral beta smallness. A contradiction sequence first yields bilateral convergence and then a further subsequence with vanishing normalized excess, producing one propagation index that works uniformly for all measures satisfying the stated bounds.