The faithful-orbit factorization of the second Jacobi sum

For a finite prime with faithful cyclotomic Galois orbit, this file proves the exact ideal factorization of the conjugate diagonal Jacobi sum. The orientation is forced by the convention that the canonical residue character reduces to the positive power x ^ ((Nv - 1) / p): the raw Jacobi sum is supported on the lower half, so its complex conjugate is supported on the upper half selected by stickelbergerTwoCoefficient.

The proof uses only finite-field binomial-sum vanishing, faithfulness of the prime orbit, and the checked identity J * conj J = Nv. No reciprocity law or assumed Jacobi factorization is used.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.span_cyclotomicJacobiSumTwo_complexConj_eq_orbitProduct {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) (horbit : Function.Injective fun (a : (ZMod p)ˣ) => (mapFinitePrime (galoisOfDirectCharacter a)) v) : Ideal.span {(cyclotomicIntegerComplexConj p ⋯) (cyclotomicJacobiSumTwo v hpv)} = ∏ a : (ZMod p)ˣ, ((mapFinitePrime (galoisOfDirectCharacter a⁻¹)) v).asIdeal ^ stickelbergerTwoCoefficient p a

Exact integral-ideal factorization of the conjugate second Jacobi sum at a finite prime with faithful cyclotomic Galois orbit.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.toPrincipalIdeal_cyclotomicJacobiSumTwo_complexConj_eq_stickelbergerTwoPrimeIdeal {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (v : FinitePrime (PrimeCyclotomicField p)) (hpv : ↑p ∉ v.asIdeal) (horbit : Function.Injective fun (a : (ZMod p)ˣ) => (mapFinitePrime (galoisOfDirectCharacter a)) v) : (toPrincipalIdeal (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) (Units.mk0 ((algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) ((cyclotomicIntegerComplexConj p ⋯) (cyclotomicJacobiSumTwo v hpv))) ⋯) = stickelbergerTwoPrimeIdeal v

Fractional-ideal form of the faithful-orbit Jacobi factorization. The principal fractional ideal of the conjugate Jacobi sum is exactly the corrected Stickelberger-two prime product.