9.2. From divided Bernoulli numerators to irregularity🔗

The finite-set construction produces a prime divisor of the numerator of B_M/M, not directly a Kummer-range numerator B_{2k}. The next result is the bridge from that unbounded witness to the usual definition of an irregular prime.

Theorem9.2.1

Statement uses 2

Statement dependency previews

Preview

Theorem 8.4.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Carlitz divisor criterion. Let q be an odd prime. Then q is not regular if and only if there is a positive even integer m such that q \mid \operatorname{num}\left(\frac{B_m}{m}\right).

Theorem 9.1.1 Theorem 8.4.1

Lean code for Theorem9.2.1●1 theorem

theoremdefined in BernoulliRegular/IrregularPrimes/Infinitude.lean

complete

theorem BernoulliRegular.not_isRegularPrime_iff_exists_dvd_bernoulli_div_self_num
  {q : ℕ} (hq : Nat.Prime q) (hq_odd : q ≠ 2) :
  ¬IsRegularPrime q ↔ ∃ m, 0 < m ∧ Even m ∧ ↑q ∣ (bernoulli m / ↑m).num

theorem BernoulliRegular.not_isRegularPrime_iff_exists_dvd_bernoulli_div_self_num
  {q : ℕ} (hq : Nat.Prime q)
  (hq_odd : q ≠ 2) :
  ¬IsRegularPrime q ↔
    ∃ m,
      0 < m ∧
        Even m ∧
          ↑q ∣ (bernoulli m / ↑m).num

Carlitz divisor criterion from the full Kummer congruence.

Proof for Theorem 9.2.1

uses 0

If q is not regular, Kummer's criterion gives a Kummer-range index k with 1\le k, 2k\le q-3, q\mid (B_{2k})_{\mathrm{num}}. Set m=2k. The range bound implies q\nmid m, so m is a unit in \mathbb{Z}_q. Dividing by this unit preserves numerator divisibility, giving q\mid \operatorname{num}\left(\frac{B_m}{m}\right). The Lean helper is the divisibility-through-division lemma dvd_bernoulli_div_self_num_of_dvd_bernoulli_num.

Conversely assume q\mid\operatorname{num}(B_m/m) for some positive even m. Von Staudt-Clausen excludes the boundary: (q-1)\nmid m, because if q-1\mid m, then q cannot divide the reduced numerator of B_m/m. This is the boundary-exclusion lemma sub_one_not_dvd_of_dvd_num_bernoulli_div_self. Let m' be the least nonnegative residue of m modulo q-1. The boundary exclusion makes m'>0, and parity gives that m' is even. It also satisfies m'<q-1, hence 1\le m'/2, 2(m'/2)\le q-3.

Apply Theorem 9.1.1 to m and m'. Since B_m/m\equiv B_{m'}/m'\pmod q, the numerator divisibility transfers from B_m/m to B_{m'}/m', and then to B_{m'}. The transfer is formalized by the p-adic numerator-transfer lemma dvd_bernoulli_num_of_padic_congruent_residue. Now m'=2(m'/2) lies in Kummer's range, so Kummer's criterion gives that q is not regular.