Faithfulness of a nontrivial cyclotomic residue orbit

Assume that the total residue symbol of eta has the inverse-character Galois weight supplied by HasDirectCharacterSquareResidueWeightAt. A collision in the Galois orbit of the denominator prime then gives two distinct powers of the base residue symbol which are equal. Since that symbol is a p-th root of unity and p is prime, the symbol must be one.

Consequently, after the algebraic weight interface has been established, a nontrivial residue symbol can occur only when the finite prime has a faithful, full Galois orbit. No reciprocity law or Jacobi-sum factorization is used in this reduction.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_eq_one_of_orbit_collision {p : ℕ} [Fact (Nat.Prime p)] {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) {a b : (ZMod p)ˣ} (hab : a ≠ b) (horbit : (mapFinitePrime (galoisOfDirectCharacter a)) v = (mapFinitePrime (galoisOfDirectCharacter b)) v) : totalPthPowerResidueSymbolAtPrime eta v = 1

A collision between two distinct direct-character representatives in the orbit of v forces the base total residue symbol to be trivial.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.totalPthPowerResidueSymbolAtPrime_eq_one_of_not_injective_orbit {p : ℕ} [Fact (Nat.Prime p)] {eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)} {v : FinitePrime (PrimeCyclotomicField p)} (hweight : HasDirectCharacterSquareResidueWeightAt eta v) (horbit : ¬Function.Injective fun (a : (ZMod p)ˣ) => (mapFinitePrime (galoisOfDirectCharacter a)) v) : totalPthPowerResidueSymbolAtPrime eta v = 1

Under inverse-character residue weight, failure of injectivity of the direct-character orbit map forces the base total residue symbol to be one. Thus only the faithful/full-orbit case can retain a nontrivial symbol.