SharpFramedWaveTailOrlicz

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

Orlicz split for the framed random-depth wave tail

This file applies the upper-profile separation split to the literal squared random-depth wave-tail term in one good-cell Whitney lane. Unlike the after-band and centered deep-band squares, the unframed input is not Gamma_1: at the profile parameters it has the exact exponent upperProfileTailSigma sigma = (1 + sigma / 4)^{-1}. The bounded hsep witness retains that exponent, while the product with the hsep residual has the target exceptional exponent Gamma_((1 - sigma) / 3).

Only the normalized inner good-mass wave-tail lane is treated. The outer probeMeanGoodWaveConst M * vecNormSq p, all other good/collar lanes, root row, layer/grid/depth aggregation, and cutoff observable are absent.

Literal carriers

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpWaveTailGoodMassCoeff (d n : ℕ) : ℝ

The common sharp coefficient and good-layer mass square root for the random-depth wave-tail square.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSharpWaveTailGoodMassCoeff d n = 5 * ↑d ^ 2 * √(Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope d n)

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpWaveTailGoodMassCoeff_nonneg (d n : ℕ) : 0 ≤ probeSharpWaveTailGoodMassCoeff d n

Exact descendant identity

Profile-tail input and explicit split