CubicThetaRadialMainConstant.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact comparison of the constructed radial residue with the printed main-term constant. The remaining arithmetic normalization is explicit.

lemma OAI.CubicFirstMoment.cubicThetaRadial_uncompletion_pole line 10
lemma OAI.CubicFirstMoment.cubicThetaRadial_level_pole_power line 27
lemma OAI.CubicFirstMoment.cubicThetaSeriesConstant_mul_base line 41
lemma OAI.CubicFirstMoment.cubicThetaRadial_scale_pole line 46
lemma OAI.CubicFirstMoment.cubicThetaRadial_real_main line 55
theorem OAI.CubicFirstMoment.cubicThetaActualCompletedRadialMain_mul_base line 76
Source documentation
This comparison isolates the exact outstanding normalization: the constructed main term times the conjugate base scalar is the printed one.
```
theorem cubicThetaActualCompletedRadialMain_mul_base {r : Eisenstein} (hr : primary r)
    (W : ℝ→ℂ) {X : ℝ} (hX : 0<X) :
    cubicThetaActualCompletedRadialMain r W X*star cubicThetaArithmeticBaseScalar=
      metaplecticMain r 0 W X := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicThetaActualCompletedRadialMain, OAI.CubicFirstMoment.cubicThetaArithmeticBaseScalar, OAI.CubicFirstMoment.metaplecticMain