CubicThetaRadialLow.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform low-height bounds after subtracting the actual radial residue. The normalization of that residue is not needed for this remainder bound.

theorem OAI.CubicFirstMoment.uniform_cubicTheta_radial_remainder_low line 12