UpperBandMeanShiftProfile #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Deterministic shift profile for the tuned deep-band mean #
After the framed hsep factor is split, the literal deterministic 2 branch of
the tuned deep-band mean has a layer coefficient
10 * d^2 * sqrt(layerMass) * 3^(-gamma D) * waveBandMean^2, where
D = k + n + ceil_n + k₀. This file sums that numerical carrier and restores
the outer coefficient probeMeanGoodWaveConst M.
The frozen maximum gate supplies cstar M⁻¹ ≤ E; together with the fifth-root
gate this lets cstarInv_mul_waveBandMean_sq_le remove every model parameter.
The result is an explicit dimension-only deterministic-shift budget.
No theorem here proves the preceding random hsep split or identifies this carrier with the actual framed layer term. The hsep residual, centered deep-band tail, other wave terms, collar contribution, depth/grid aggregation, and cutoff observable are absent.
The dimension-only part of probeMeanGoodWaveConst, before its single
cstar⁻¹ factor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dimension-only one-coordinate budget after summing the deterministic band-mean branch over Whitney layers and restoring the outer coefficient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The dimension-only budget after the finite coordinate trace.