Consequences of the Gauss-Jacobi identities and cubic reciprocity

import Mathlib
import Definitions.Def_QRH_arith
import Definitions.Def_QRH_sums
import Definitions.Def_QRH_lfun

universe u

namespace QRH

/-- The consequences of the Gauss-Jacobi identities and cubic
reciprocity (Lemma 4.1 of the source), for squarefree primary elements
prime to S. The four conjuncts are the conversion identities between
Möbius coefficients and cubic Gauss sums (equations 4.7 and 4.8): the
Möbius factor combines with the Poisson γ₋₁ into the cubic coefficient,
and back; the quotient identity for the ray class factor G (equation
4.9); and the multiplicativity of the cubic Gauss-sum coefficients a_ξ
up to a sextic twist (equation 4.10). Each follows from the interface
axioms by complex algebra: the Gauss sums and the phase have modulus one,
Möbius squares to one on squarefree elements, and the reciprocity
bicharacter is real. -/
theorem gauss_jacobi_consequences (W : QRHWorld.{u}) (a b n : W.E)
    (hsn : W.IsSqf n) (hgn : W.Sgood n)
    (hsa : W.IsSqf a) (hga : W.Sgood a)
    (hsb : W.IsSqf b) (hgb : W.Sgood b)
    (hcop : ∀ d : W.E, d ∈ W.divs a → d ∈ W.divs b → d = W.one) :
    star (W.alpha n) * W.gamma 2 n * W.gamma 1 n
        = W.mu n * W.Gcl (W.cl n)
      ∧ W.mu n * W.gamma (-1) n
        = W.chiNeg n * (W.Gcl (W.cl n))⁻¹ * star (W.alpha n)
            * W.gamma 2 n
      ∧ W.chiNeg a * star (W.Gcl (W.cl a)) * W.Gcl (W.cl b)
            * W.Rcl (W.cl a) (W.cl b)
          = W.Gcl (W.mulC (W.cl b) (W.invC (W.cl a)))
      ∧ axi W (W.mul a b) = axi W a * axi W b * W.chi b a ^ 4 := by
  sorry

end QRH