Machine Logic

For the holidays, some problems about prime divisors

23 Dec 2024

Just in time for the holiday break, here are some small exercises to build your skills. The subject matter is the prime numbers: specifically, the maximum exponent of a prime divisor of a number. A skeleton Isabelle theory file is available, containing all statements of the theorems and necessary definitions or boilerplate, but no proofs. Your task – when not eating, drinking, or watching movies – is to do the proofs, Some are harder than others.

Defining the notion of index

First, a simple fact: if $p$ is prime and $p^k$ divides $mn$, then we can write $k=i+j$ where $p^i$ divides $m$ and $p^j$ divides $n$. It is trivial because a similar proof is built-in and sledgehammer will find it for you.

lemma primepow_divides_prod:
  fixes p::nat
  assumes "prime p" "(p^k) dvd (m * n)"
  shows "∃i j. (p^i) dvd m ∧ (p^j) dvd n ∧ k = i + j"
  sorry

To reason about the maximum exponent of a prime divisor, we need to show that this maximum exists. It might be helpful to consider the set of all $k$ such that $p^k$ divides $n$. A structured proof that establishes a natural series of basic facts about this set leads to the conclusion.

lemma maximum_index:
  fixes n::nat
  assumes "n > 0" "2 ≤ p"
  shows "∃k. p^k dvd n ∧ (∀l>k. ¬ p^l dvd n)"
  sorry

Having proved that the maximum index exists, we could refer to the maximum directly, using the function Max. Instead, the definition below refers to the cardinality of the set of possible non-zero indices. The practical effect of this choice is probably insignificant.

definition index :: "nat ⇒ nat ⇒ nat" where
  "index p n 
    ≡ if p ≤ 1 ∨ n = 0 then 0 else card {j. 1 ≤ j ∧ p^j dvd n}"

Simple consequences of the definition

The next task is to show that our definition satisfies its objective, characterising $p^k \mid n$. It would make sense to consider carefully the form of the definition, dealing with the degenerate cases separately.

proposition pow_divides_index:
  "p^k dvd n ⟷ n = 0 ∨ p = 1 ∨ k ≤ index p n"
  sorry

From that key result, a couple of corollaries follow directly:

corollary le_index:
  "k ≤ index p n ⟷ (n = 0 ∨ p = 1 ⟶ k = 0) ∧ p^k dvd n"
  sorry

corollary exp_index_divides: "p^(index p n) dvd n"
  sorry

And some slightly more difficult problems

The following upper bound for the index of a prime divisor isn’t difficult to prove, but again the degenerate case needs to be treated separately.

lemma index_trivial_bound: "index p n ≤ n"
  sorry

Next, you can prove the following natural law for the index of a product.

proposition index_mult:
  assumes "prime p" "m > 0" "n > 0"
  shows "index p (m * n) = index p m + index p n"
  sorry

To conclude, the analogous law for the index of a power.

corollary index_exp:
  assumes "prime p"
  shows "index p (n^k) = k * index p n"
  sorry

To get started, simply download the theory file, which also contained the necessary Isabelle boilerplate. If anybody sends me a particularly nice solution to this problem set, I will happily upload it here.