3.4. Congruences with classical Bernoulli numbers
The remaining results in this chapter concern the classical Bernoulli numbers
B_n \in \mathbb{Q} and their p-adic behaviour. They are needed in two ways: to
control the ordinary Bernoulli numbers below the boundary p-1, and to handle the
exceptional contribution of the boundary character \omega^{p-2} to the product
side of the analytic formula for \hminus.
3.4.1. Integrality below the boundary
p-integrality of B_k for k < p - 1. Let p be an odd prime and let
0 \le k < p - 1. Then B_k \in \mathbb{Q} lies in \mathbb{Z}_p; equivalently,
there exists z \in \mathbb{Z}_p with B_k = z in \mathbb{Q}_p.
Lean code for Theorem3.4.1.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.bernoulli_mem_padicInt_of_lt_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (k : ℕ) (hk : k < p - 1) : ∃ z, ↑(bernoulli k) = ↑z
theorem BernoulliRegular.bernoulli_mem_padicInt_of_lt_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (k : ℕ) (hk : k < p - 1) : ∃ z, ↑(bernoulli k) = ↑z
Bernoulli numbers below the boundary `p - 1` are `p`-adic integers. Stated as: `(bernoulli k : ℚ_[p])` equals the image of some `z : ℤ_[p]` under the natural coercion `ℤ_[p] → ℚ_[p]`. **Proof approach:** strong induction on `k`. Base cases `k = 0` (equals `1`) and `k = 1` (equals `-1/2`, a `p`-unit in `ℤ_[p]` since `p` is odd) are direct. Odd `k ≥ 3` have `bernoulli k = 0` and are trivial. For even `k ≥ 2` with `k < p - 1`, use `sum_bernoulli (k + 1)` to get `(k + 1) · bernoulli k = -∑_{j ∈ range k} C(k + 1, j) · bernoulli j`; since `k + 1 < p`, the scalar is a `p`-unit, and each summand is a `p`-adic integer by the induction hypothesis.
Strong induction on k. The base case k = 0 is B_0 = 1 \in \mathbb{Z}_p. For
the inductive step assume k \ge 1 and that B_j \in \mathbb{Z}_p for all j < k.
The recursion \sum_{j=0}^{k} \binom{k+1}{j} B_j = 0 extracts the top term, and
after rearrangement, (k + 1)\,B_k = -\sum_{j = 0}^{k - 1} \binom{k+1}{j}\,B_j. By
the induction hypothesis each B_j is a p-adic integer. The binomial
coefficients \binom{k+1}{j} are integers, hence are also p-adic integers. So
the right-hand side is in \mathbb{Z}_p. Finally k + 1 \le p - 1 < p means
p \nmid (k+1), so k + 1 is a unit in \mathbb{Z}_p and we may divide. Hence
B_k \in \mathbb{Z}_p.
Denominator coprimality. For p an odd prime and 0 \le n < p - 1,
p \nmid (B_n)_{\mathrm{den}}.
Lean code for Corollary3.4.1.2●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.prime_not_dvd_bernoulli_den_of_lt_sub_one {p n : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (hn : n < p - 1) : ¬p ∣ (bernoulli n).den
theorem BernoulliRegular.prime_not_dvd_bernoulli_den_of_lt_sub_one {p n : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (hn : n < p - 1) : ¬p ∣ (bernoulli n).den
For indices strictly below the boundary `p - 1`, the denominator of the classical Bernoulli number is prime to `p`. This is the denominator form of the p-integrality statement used in the proof of Diekmann Theorem 42: if `n < p - 1`, then `p ∤ (bernoulli n).den`.
By Theorem 3.4.1.1 the p-adic absolute value of B_n is
at most 1, so the denominator of B_n is a p-unit. Equivalently, the cast
((B_n)_{\mathrm{den}} : \mathbb{Z}_p) is a unit, which is equivalent to
p \nmid (B_n)_{\mathrm{den}}.
3.4.2. Von Staudt–Clausen at the boundary
The recursion that pushes B_k into \mathbb{Z}_p for k < p - 1 breaks down at
k = p - 1: the scalar k + 1 = p is no longer a p-unit. The Bernoulli number
B_{p-1} has p in its denominator, and the classical Von Staudt–Clausen theorem
pins this denominator down exactly.
Von Staudt–Clausen, p-local form at n = p - 1. For p an odd prime,
B_{p-1} + \frac{1}{p} \;\in\; \mathbb{Z}_p.
Equivalently, p \cdot B_{p-1} \equiv -1 \pmod{p} as p-adic integers.
Lean code for Theorem3.4.2.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.bernoulli_pSubOne_add_inv_p_mem_padicInt {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) : ∃ z, ↑(bernoulli (p - 1)) + (↑p)⁻¹ = ↑z
theorem BernoulliRegular.bernoulli_pSubOne_add_inv_p_mem_padicInt {p : ℕ} [hp : Fact (Nat.Prime p)] (hp_odd : p ≠ 2) : ∃ z, ↑(bernoulli (p - 1)) + (↑p)⁻¹ = ↑z
**Von Staudt–Clausen at `n = p-1` (p-local form).** For an odd prime `p`, `bernoulli (p-1) + 1/p` is a `p`-adic integer. Equivalently, `p · bernoulli (p-1) ≡ -1 (mod p)` in `ℤ_[p]`. **Proof sketch.** Specialise `sum_bernoulli` at `n = p`: `∑_{k < p} C(p, k) · bernoulli k = 0`. Extract `k = p - 1`: `p · bernoulli (p-1) = -∑_{k < p - 1} C(p, k) · bernoulli k`. Expanding: the `k = 0` term is `1`; the `k = 1` term is `-p/2`; odd `k ≥ 3` terms vanish; the remaining even `k ∈ [2, p-3]` terms have `C(p, k)` divisible by `p` (Nat.Prime.dvd_choose_self) and `bernoulli k` a `p`-adic integer (by `bernoulli_mem_padicInt_of_lt_sub_one`). Collecting terms: `p · bernoulli (p-1) + 1 = p/2 + (p-divisible stuff)`, hence `/p` lands in `ℤ_[p]`.
Specialise the Bernoulli recursion at n = p:
\sum_{k = 0}^{p - 1} \binom{p}{k}\,B_k = 0. The top index k = p - 1 contributes
\binom{p}{p - 1} \cdot B_{p-1} = p \cdot B_{p-1}. Isolating this and splitting off
k = 0 (which contributes B_0 = 1) gives
p \cdot B_{p-1} + 1 = -\sum_{k = 1}^{p - 2} \binom{p}{k}\,B_k. For each
1 \le k \le p - 2, the binomial coefficient \binom{p}{k} is divisible by p;
write \binom{p}{k} = p \cdot c_k for some c_k \in \mathbb{N}. By
Theorem 3.4.1.1, each B_k for 1 \le k \le p - 2 is a
p-adic integer (note that p - 2 < p - 1). Therefore the right-hand side is p
times an element of \mathbb{Z}_p, and dividing by p (cancellable in
\mathbb{Q}_p) yields
B_{p - 1} + \frac{1}{p} = -\sum_{k=1}^{p-2} c_k \cdot B_k \in \mathbb{Z}_p, as
claimed.
3.4.3. The boundary character omega-to-the-minus-one
The product side of the analytic formula for \hminus runs over odd Dirichlet
characters \chi modulo p; identifying characters with powers of the Teichmüller
character \omega, every odd \chi has the form \omega^j for some odd
j \in \{1, 3, \dots, p - 2\}. The contribution B_{1,\omega^j} is p-integral
for j \in \{1, 3, \dots, p - 4\} (by the same recursion-based analysis used above,
extended to character twists); the exceptional case is j = p - 2 — the
"inverse Teichmüller" character \omega^{-1}, which is the one boundary character
that sees the Von Staudt–Clausen pole. We use the \mathbb{Q}_p-valued Teichmüller
character \omega : (\mathbb{Z}/p\mathbb{Z})^\times \to \mathbb{Q}_p^\times.
Boundary character contribution. For p an odd prime there exists
z \in \mathbb{Z}_p with
B_{1,\omega^{p-2}} \;=\; \frac{p - 1}{p} \;+\; z.
In particular, B_{1,\omega^{-1}} shares the p-adic pole of the classical
B_{p-1} from Theorem 3.4.2.1, with residue (p - 1)/p.
Lean code for Theorem3.4.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in BernoulliRegular/BernoulliGeneralized.leancomplete
theorem BernoulliRegular.bernoulliGen_teichmuller_inverse_eq_p_sub_one_div_p_add_padicInt {p : ℕ} [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) : ∃ z, BernoulliRegular.BernoulliGen (BernoulliRegular.teichmullerCharQp p ^ (p - 2)) 1 = (↑p - 1) / ↑p + ↑z
theorem BernoulliRegular.bernoulliGen_teichmuller_inverse_eq_p_sub_one_div_p_add_padicInt {p : ℕ} [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) : ∃ z, BernoulliRegular.BernoulliGen (BernoulliRegular.teichmullerCharQp p ^ (p - 2)) 1 = (↑p - 1) / ↑p + ↑z
**Diekmann eq. 29** (T008): for an odd prime `p`, the boundary character `ω^{-1}` contributes the exceptional term `(p - 1) / p`, up to a `p`-adic integer. We realise `ω^{-1}` as `ω^(p - 2)`.
Set \chi := \omega^{p - 2} regarded as a Dirichlet character modulo p valued in
\mathbb{Q}_p, with underlying \mathbb{Z}_p-valued lift
\chi_{\mathbb{Z}_p} := \omega_{\mathbb{Z}_p}^{p - 2}. Since p is odd,
p - 2 \in \{1, \dots, p - 2\} is not divisible by p - 1, so
\chi \ne \mathbf{1}; the cleared form Lemma 3.3.2
gives
p \cdot B_{1,\chi} \;=\; \sum_{a \in \mathbb{Z}/p\mathbb{Z}} \chi(a)\,a \;=:\; S \;\in\; \mathbb{Z}_p,
the last identity because each summand is the product of a \mathbb{Z}_p-valued
character value and an integer representative. We compute S modulo p. For
a = 0, the summand is 0 because \chi_{\mathbb{Z}_p}(0) = 0. For a \ne 0,
the Teichmüller character lifts the identity modulo p:
\omega_{\mathbb{Z}_p}(a) \equiv a \pmod{p}. Therefore
\chi_{\mathbb{Z}_p}(a) \equiv a^{p - 2} \pmod{p}, and hence
\chi_{\mathbb{Z}_p}(a) \cdot a \equiv a^{p - 1} \equiv 1 \pmod{p} by Fermat's
little theorem. Summing, S \equiv \sum_{a \ne 0} 1 = p - 1 \pmod{p}. So
S - (p - 1) \in p \cdot \mathbb{Z}_p; write S - (p - 1) = p \cdot z with
z \in \mathbb{Z}_p. Then
p \cdot B_{1,\chi} = S = (p - 1) + p \cdot z = p \cdot \bigl(\frac{p - 1}{p} + z\bigr),
and cancelling the unit p \in \mathbb{Q}_p^{\times} gives the claim.
The remaining bridge to the analytic formula for \hminus is Euler's identity
expressing L(1 - n, \chi) in terms of B_{n,\chi}; this is the subject of the
next chapter.