Residue weight of a normalized cyclotomic Kummer radicand

A Kummer radicand transforms through the square of the direct cyclotomic character only up to a p-th power in the fraction field. This file clears that field-valued witness at one finite prime and proves the resulting direct-character-square identity for total power-residue symbols.

The clearance uses Mathlib's IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer. No external reciprocity theorem is invoked here.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.hasDirectCharacterSquareResidueWeightAt_of_normalization {p : ℕ} [Fact (Nat.Prime p)] {L : Type u} [Field L] [NumberField L] [Algebra (PrimeCyclotomicField p) L] [IsScalarTower ℚ (PrimeCyclotomicField p) L] (E : InverseExtension p L) (P : E.KummerPresentation) (eta : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (c : (PrimeCyclotomicField p)ˣ) (hnormalization : (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) eta = P.radicand * ↑c ^ p) (v : FinitePrime (PrimeCyclotomicField p)) (horbit : ∀ (sigma : Gal(PrimeCyclotomicField p/ℚ)), eta ∉ ((mapFinitePrime sigma) v).asIdeal) (hpv : ↑p ∉ v.asIdeal) : HasDirectCharacterSquareResidueWeightAt eta v

A normalized integral Kummer radicand has direct-character-square residue weight at a finite prime when its whole Galois orbit avoids the numerator.

The orbitwise support condition is essential. A field-valued Kummer witness can have a denominator at a conjugate prime even when the original prime avoids eta; clearing it locally needs both integral representatives to be units at the transported prime.