10.2. The unproved reciprocity input🔗

Theorem10.2.1

uses 0used by 1⚠L∃∀N

One-sided Kummer principal reciprocity. Let \alpha,\beta\in\mathcal{O}_K be nonzero, coprime, and prime to p. Assume that \alpha is a p-th power in the (\zeta_p-1)-adic completion of K. Then the canonical p-th-power residue symbols satisfy \left(\frac{\alpha}{(\beta)}\right)_p = \left(\frac{\beta}{(\alpha)}\right)_p.

Lean code for Theorem10.2.1●1 theorem, incomplete

theoremdefined in BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/OneSidedKummerReciprocity.lean

contains sorry

theorem BernoulliRegular.Furtwaengler.oneSidedKummerPrincipalReciprocity_canonical.{u}
  (p : ℕ) [Fact (Nat.Prime p)] (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  {α β : NumberField.RingOfIntegers K} (hα_ne : α ≠ 0) (hβ_ne : β ≠ 0)
  (hcop : IsCoprime (Ideal.span {α}) (Ideal.span {β}))
  (hα_prime_to_p : IsCoprime (Ideal.span {α}) (Ideal.span {↑p}))
  (hβ_prime_to_p : IsCoprime (Ideal.span {β}) (Ideal.span {↑p}))
  (hα_local : BernoulliRegular.Furtwaengler.IsLambdaLocalPthPower α) :
  BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical α
      (Ideal.span {β}) =
    BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical β
      (Ideal.span {α})

theorem BernoulliRegular.Furtwaengler.oneSidedKummerPrincipalReciprocity_canonical.{u}
  (p : ℕ) [Fact (Nat.Prime p)]
  (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  {α β : NumberField.RingOfIntegers K}
  (hα_ne : α ≠ 0) (hβ_ne : β ≠ 0)
  (hcop :
    IsCoprime (Ideal.span {α})
      (Ideal.span {β}))
  (hα_prime_to_p :
    IsCoprime (Ideal.span {α})
      (Ideal.span {↑p}))
  (hβ_prime_to_p :
    IsCoprime (Ideal.span {β})
      (Ideal.span {↑p}))
  (hα_local :
    BernoulliRegular.Furtwaengler.IsLambdaLocalPthPower
      α) :
  BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical
      α (Ideal.span {β}) =
    BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical
      β (Ideal.span {α})

**One-sided Kummer principal reciprocity, canonical additive form.**

Let `K = ℚ(ζ_p)` and `λ = (ζ_p - 1)`.  If `α β : 𝓞 K` are nonzero,
their principal ideals are coprime, both are prime to `p`, and `α` is a
`p`-th power in the `λ`-adic completion, then

`(α / (β))_p = (β / (α))_p`.

Here both sides are written as the canonical additive `ZMod p` residue
symbol `pthSymbolAtIdeal_canonical`.

This is the single missing mathematical input for the reflection route as recorded here. It is intentionally stated as a concrete reciprocity theorem, not as a packaged reflection principle.

The immediate consequence needed below is the following principal-denominator vanishing statement. If \eta is locally a p-th power at \zeta_p-1, prime to p, and (\eta)=\mathfrak b^p, then for every admissible principal denominator (\gamma) one has \left(\frac{\eta}{(\gamma)}\right)_p=1. Indeed, reciprocity gives \left(\frac{\eta}{(\gamma)}\right)_p = \left(\frac{\gamma}{(\eta)}\right)_p, and the denominator (\eta)=\mathfrak b^p makes the right hand side trivial by multiplicativity in the denominator.