Kummer's Criterion and Regular Primes in Lean

9.3. The finite-set construction🔗

The escape argument starts from a finite set S and builds an even integer which is divisible by q-1 for every prime q\in S.

Definition9.3.1
uses 0used by 1✓L∃∀N

Divisor-closed base. For a finite set S\subset\mathbb{N}, set C(S)=2\cdot \bigl(\max(3,\sup S)\bigr)!.

Lean code for Definition9.3.1●1 definition
  • defdefined in BernoulliRegular/IrregularPrimes/DivisorClosedBase.lean
    complete
    def BernoulliRegular.irregularBase (S : Finset ℕ) : ℕ
    def BernoulliRegular.irregularBase
  (S : Finset ℕ) : ℕ
    The explicit even multiplier attached to a finite set of candidate primes.
Proof for Definition 9.3.1
uses 0

The factor 2 makes C(S) even, and the factorial makes q-1\mid C(S) for every prime q\in S. The stronger closure property used internally is that if a prime q divides C(S), then q-1\mid C(S) as well.

Theorem9.3.2
uses 1used by 1✓L∃∀N

A new numerator prime outside a finite set. For every finite set S\subset\mathbb{N}, there are natural numbers M and p such that p is prime, p\ne 2, M>0, M is even, \forall q\in S,\ q\text{ prime}\Longrightarrow q-1\mid M, p\mid \operatorname{num}\left(\frac{B_M}{M}\right), and p\notin S.

Definition 9.3.1

Lean code for Theorem9.3.2●1 theorem
  • theoremdefined in BernoulliRegular/IrregularPrimes/Infinitude.lean
    complete
    theorem BernoulliRegular.exists_numerator_prime_for_carlitz_base
  (S : Finset ℕ) :
  ∃ M p,
    Nat.Prime p ∧
      p ≠ 2 ∧
        Even M ∧
          0 < M ∧
            (∀ q ∈ S, Nat.Prime q → q - 1 ∣ M) ∧
              ↑p ∣ (bernoulli M / ↑M).num ∧ p ∉ S
    theorem BernoulliRegular.exists_numerator_prime_for_carlitz_base
  (S : Finset ℕ) :
  ∃ M p,
    Nat.Prime p ∧
      p ≠ 2 ∧
        Even M ∧
          0 < M ∧
            (∀ q ∈ S,
                Nat.Prime q → q - 1 ∣ M) ∧
              ↑p ∣
                  (bernoulli M / ↑M).num ∧
                p ∉ S
    Carlitz-facing wrapper around the constructed large multiple.  It packages
the index as a single even positive `M` divisible by `q - 1` for every prime
`q` in the finite input set.
Proof for Theorem 9.3.2
uses 0

Start with C=C(S). The growth theorem for divided Bernoulli numbers exists_large_even_multiple_abs_bernoulli_div_self_gt_one chooses t such that \left|\frac{B_{C2^t}}{C2^t}\right|>1. Set M=C2^t. This M is positive and even, and it is still divisible by q-1 for every prime q\in S.

Since the rational number B_M/M has absolute value greater than 1, its reduced numerator has absolute value greater than 1, hence has a prime divisor p, by the numerator-prime lemma exists_prime_dvd_num_of_one_lt_abs.

It remains to prove that this prime was not already in S. Suppose p\in S. Then p-1\mid M by construction. But von Staudt-Clausen gives the exclusion p-1\mid M \Longrightarrow p\nmid \operatorname{num}\left(\frac{B_M}{M}\right), namely the von Staudt numerator-exclusion lemma not_dvd_num_bernoulli_div_self_of_sub_one_dvd. This contradicts the choice of p. The same exclusion also proves p\ne 2, since p=2 would make p-1=1 divide M.