UpperWaveTailBoundedGrid

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

The bounded good-mass wave-tail lane through the triadic grid

This file weakens the literal bounded wave-tail Whitney sum to the terminal exceptional exponent, restores the exact outer mean and one-coordinate factor, translates the centered witness to each descendant cube, and applies the strict-descendant triadic maximum. The resulting scale keeps the profile-tail triangle constant, the squared sigma pole, the tuned exponential decay, and exactly one outer mean coefficient.

The root row, rare and collar witnesses, terminal absorption, other named lanes, and cutoff observable are not treated here. These declarations are conditional internal A for the bounded good-mass wave-tail lane.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma_le_tailSigma {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : upperProfileTargetSigma sigma ≤ upperProfileTailSigma sigma

The terminal exceptional exponent is weaker than the exponent of the bounded wave-tail witness throughout the profile window.