PrimaryCharacterNonprincipal.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nonprincipality of the actual mixed character. The zero-frequency Gauss identity and an explicit primary Chinese-remainder lift supply the witness; nonprincipality is not imposed as an extra hypothesis.

lemma OAI.CubicFirstMoment.exists_primary_residue_lift line 14
lemma OAI.CubicFirstMoment.mixedResidueChar_ne_one line 26
theorem OAI.CubicFirstMoment.mixedCubic_nonprincipal line 45
Source documentation
A primary witness for nonprincipality, on the actual prime-to-conductor ideal character used in the finite-order Hecke input.
```
theorem mixedCubic_nonprincipal {a b : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (hnu : ¬ IsUnit (a*b)) : MixedCubicNonprincipal a b := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MixedCubicNonprincipal
lemma OAI.CubicFirstMoment.primaryMixedResidueChar_witness line 61

theorem OAI.CubicFirstMoment.mixed_primitive_conductor line 72

Source documentation

The actual nonprincipal primitive character inducing the mixed cubic symbol, with the exact norm and unit-invariance guarantees needed by the published Hecke functional equation.

theorem mixed_primitive_conductor {a b : Eisenstein}
    (ha : primary a) (hb : primary b) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (hnu : ¬ IsUnit (a*b)) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ),
      d ≠ 0 ∧ PrimitiveResidueCharacter d ψ ∧ ψ ≠ 1 ∧
      normNat d ≤ normNat (3*(a*b)) ∧
      (∀ u : Eisensteinˣ, ψ (Ideal.Quotient.mk (modulus d) u) = 1) ∧
      ResidueCharacterInduces (3*(a*b)) d (primaryMixedResidueChar a b ha hb) ψ ∧
      (∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
        ψ (Ideal.Quotient.mk (modulus d) x) = mixedCubic a b x) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.primaryMixedResidueChar, OAI.CubicFirstMoment.mixedCubic