9.1. The divided Kummer congruence
The Carlitz argument needs a Kummer congruence for the divided Bernoulli numbers
B_m/m with no upper bound on the exponents.
Full divided Kummer congruence. Let p be an odd prime. Let m,n>0 be even
natural numbers such that m \equiv n \pmod {p-1} and (p-1)\nmid n. Then there
exists z\in \mathbb{Z}_p with \frac{B_m}{m} - \frac{B_n}{n} = pz in
\mathbb{Q}_p.
Lean code for Theorem9.1.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/IrregularPrimes/KummerCongruenceFull.leancomplete
theorem BernoulliRegular.bernoulli_div_sModEq_of_modEq_full {p m n : ℕ} [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (hm_pos : 0 < m) (hn_pos : 0 < n) (hm_even : Even m) (hn_even : Even n) (hnot : ¬p - 1 ∣ n) (hmn : m ≡ n [MOD p - 1]) : ∃ z, ↑(bernoulli m / ↑m) - ↑(bernoulli n / ↑n) = ↑p * ↑z
theorem BernoulliRegular.bernoulli_div_sModEq_of_modEq_full {p m n : ℕ} [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (hm_pos : 0 < m) (hn_pos : 0 < n) (hm_even : Even m) (hn_even : Even n) (hnot : ¬p - 1 ∣ n) (hmn : m ≡ n [MOD p - 1]) : ∃ z, ↑(bernoulli m / ↑m) - ↑(bernoulli n / ↑n) = ↑p * ↑z
**Standard Kummer congruence for divided Bernoulli numbers.** This is the public full congruence used by the Carlitz route. The odd-prime case reduces to `p ≥ 5`: if `p = 3`, then `p - 1 = 2` divides every even non-boundary exponent, contradicting the hypotheses.
The proof first reduces to p\ge 5. If p=3, then p-1=2 divides every even
exponent n, contradicting the non-boundary hypothesis (p-1)\nmid n.
For p\ge 5, the proof is a strengthened elementary Voronoi argument. The first
input is the strong Faulhaber congruence
\sum_{x=0}^{p-1} x^h - pB_h \in h p^2\mathbb{Z}_p for positive even h with
(p-1)\nmid h. In Lean this is the strong Faulhaber lemma
sum_range_pow_sub_p_mul_bernoulli_strong. It expands the power sum by mathlib's
Faulhaber formula and proves that every non-leading summand contains the required
hp^2-factor. The delicate terms are handled with von Staudt-Clausen denominator
control and binomial divisibility.
The second input is the strong Voronoi congruence
(a^h-1)\frac{B_h}{h} - a^{h-1}\sum_{x=0}^{p-1} x^{h-1}\left\lfloor\frac{xa}{p}\right\rfloor \in p\mathbb{Z}_p
for every a prime to p, formalized as the strong Voronoi theorem
voronoi_congruence_mod_p_strong. This substitutes the strong Faulhaber congruence
into a higher-modulus Voronoi sum identity and cancels the nonzero rational factor
hp in \mathbb{Q}_p.
Next choose a generator g of (\mathbb{Z}/p\mathbb{Z})^\times, represented by a
natural number a. Since g has order p-1, the condition (p-1)\nmid h
implies a^h-1 is a p-adic unit. Dividing the strong Voronoi congruence by this
unit proves \frac{B_h}{h}\in \mathbb{Z}_p, recorded as the Voronoi integrality
lemma bernoulli_div_self_mem_padicInt_of_not_sub_one_dvd_voronoi.
Finally apply the strong Voronoi congruence to m and n. The factors a^m and
a^n agree because m\equiv n\pmod{p-1}, and the floor sums are congruent modulo
p because their predecessor exponents are congruent; this is the floor-sum
comparison voronoi_floor_sum_sModEq_of_pred_modEq. The already-proved
p-integrality of B_m/m and B_n/n lets the comparison be carried out inside
\mathbb{Z}_p, and the difference is a multiple of p in \mathbb{Q}_p.