NormalizedGainBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reserve a uniform positive exponent for the two pencil-size cases of the regular-scale estimate. All fixed constants are absorbed at large depth.