Challenge: one-sided Kummer reciprocity for locally-primary pseudo-units

The destination proves that the canonical Kummer radicand has p-divisible finite divisor and is a p-th power in the completion at the cyclotomic prime. It also checks the comparison between Kummer/Frobenius coordinates, clears prime-to-cyclotomic fractional denominators to integral ones, and removes the cyclotomic-prime factor itself. The sole remaining arithmetic contract is therefore integral one-sided Kummer reciprocity for a locally-primary pseudo-unit.

The checked bridges then prove prime-to-cyclotomic and full principal reciprocity, the Kummer product formula, and the required surjective inverse-cyclotomic ideal-class quotient. The separate Herbrand--Kummer assertion that this quotient cannot exist is not part of this contract.

theorem MazurTheorem.Challenge.cyclotomic_locallyPrimaryPseudoUnitKummerReciprocityPrinciple (p : ℕ) [Fact (Nat.Prime p)] (_hp : 5 ≤ p) : NumberTheory.CyclotomicCharacter.LocallyPrimaryPseudoUnitKummerReciprocityPrinciple p

One-sided Kummer reciprocity kills every integral principal Kummer symbol away from the cyclotomic prime when the radicand is a locally-primary pseudo-unit.

theorem MazurTheorem.Challenge.cyclotomic_primeToCyclotomicPrincipalReciprocityPrinciple (p : ℕ) [Fact (Nat.Prime p)] (hp : 5 ≤ p) : NumberTheory.CyclotomicCharacter.PrimeToCyclotomicPrincipalReciprocityPrinciple p

Checked reduction from the locally-primary pseudo-unit contract to prime-to-cyclotomic principal Artin reciprocity.

theorem MazurTheorem.Challenge.cyclotomic_kummerArtinProductFormulaPrinciple (p : ℕ) [Fact (Nat.Prime p)] (hp : 5 ≤ p) : NumberTheory.CyclotomicCharacter.KummerArtinProductFormulaPrinciple p

Checked reduction from prime-to-cyclotomic reciprocity to the full Kummer product formula.

theorem MazurTheorem.Challenge.cyclotomic_classFieldTheoryPrinciple (p : ℕ) [Fact (Nat.Prime p)] (hp : 5 ≤ p) : NumberTheory.CyclotomicCharacter.ClassFieldTheoryPrinciple p

Checked bridge from the exact Kummer product-formula contract to the roadmap-facing class-field-theory principle.