CubicThetaPrimaryCoefficients.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The exact primary cube coefficients isolated in DR v3 (5.17). This connects the constructed theta expansion to the completed Gauss sum.

lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_primary line 12
Source documentation
The primary frequency lambda^-3*c*d^3 has no unit phase and has the normalized conjugate Gauss coefficient of the original cubic sum.
```
lemma cubicThetaArithmeticCoefficient_primary {c d : Eisenstein}
    (hc : primary c) (hd : primary d) (hs : Squarefree c) :
    cubicThetaArithmeticCoefficient (lambdaE*c*d^3) =
      ((81/(Real.sqrt (norm c)*norm d):ℝ):ℂ)*star (gauss c) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss
lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_primary_conj line 30
Source documentation
Conjugating the primary coefficient gives the original Gauss sum, with the exact real normalization retained.
```
lemma cubicThetaArithmeticCoefficient_primary_conj {c d : Eisenstein}
    (hc : primary c) (hd : primary d) (hs : Squarefree c) :
    star (cubicThetaArithmeticCoefficient (lambdaE*c*d^3)) =
      ((81/(Real.sqrt (norm c)*norm d):ℝ):ℂ)*gauss c := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss
def OAI.CubicFirstMoment.cubicThetaTau line 40
Source documentation
The source uses tau(mu), while our Whittaker coefficient is tau(mu)/|mu|.
```
def cubicThetaTau (n : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.cubicThetaFrequency_primary_norm line 43
theorem OAI.CubicFirstMoment.cubicThetaTau_primary_conj line 63
Source documentation
DR v3 (5.17), with the unnormalized theta coefficient restored.
```
theorem cubicThetaTau_primary_conj {c d : Eisenstein}
    (hc : primary c) (hd : primary d) (hs : Squarefree c) :
    star (cubicThetaTau (lambdaE*c*d^3)) =
      ((3^(5/2:ℝ)*Real.sqrt (norm d):ℝ):ℂ)*gauss c := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicThetaTau, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss