General Structure of IFF

Stream: new members

[Jonas Whidden]

I'm working on a fairly small theorem to try and learn Lean 4, and I'm stuck exactly how to structure the translation of part of it. I have:

Note that if $p \equiv 0 \pmod{r}$, then $r = p$ as both are prime, but this is a contradiction as $r \nmid n$. And if $p \equiv 1 \pmod{r}$, trivially $p = q \equiv 1 \pmod{r}$, so we ignore these cases. Then we look at when $\sigma(p^{\alpha}) = (p^{\alpha+1}-1)/(p-1) = 0 \pmod{r}$. As $p - 1$ has an inverse mod $r$, this is when the numerator is $0$.

This implies:
$\sigma(p^{\alpha}) \equiv 0 \pmod{r} \iff p^{\alpha+1} \equiv 1 \pmod{r}$.

I've proven the first two parts to yield $p ≠ 0 \pmod r$ and $p ≠ 1 \pmod r$ as results using have hp_mod_r0 and have hp_mod_r1 respectively, and want to use the latter to show that $r | (p-1)$ must be false given hp_mod_r1, since:

1. $p ≠ 1 \pmod r$ ->
2. $(p-1) ≠ 0 \pmod r$ ->
3. $r ∤ (p-1)$ -> (I'm not really sure what to use to get from 3 to 4 to 5, but I think this plus $r$ and $p$ being distinct primes guarantees it...)
4. $(p-1)$ and $r$ are coprime ->
5. $gcd(p-1, r) = 1$ ->
6. $(p-1)$ has an inverse $\pmod r$ ->
7. $\sigma(p^{\alpha}) = (p^{\alpha+1}-1)/(p-1) = 0 \pmod r$ -> (assuming the definition for the rewrite of $\sigma(p^{\alpha})$ is already built in somewhere...)
8. $p^{\alpha+1}-1 = 0 \pmod r$ ->
9. $p^{\alpha+1} = 1 \pmod r$.

Are those the correct logical steps to take in Lean 4, or am I missing steps? Are there shortcuts I could be using? And then I assume I need to work backwards from $p^{\alpha+1} \equiv 1 \pmod{r}$ to reach $\sigma(p^{\alpha}) \equiv 0 \pmod{r}$ to close the if and only if. What's the general structure of proving an IFF as a single lemma to be referenced later on?

[Martin Dvořák]

This kind of question would better be asked together with some code.

[Jonas Whidden]

Martin Dvořák said:

This kind of question would better be asked together with some code.

This is what I have so far:

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Data.Nat.Basic
import Mathlib.NumberTheory.Divisors
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Divisibility.Units

open BigOperators ArithmeticFunction

/-- A number `n` is perfect if the sum of its positive divisors equals `2 * n`. -/
def isPerfect (n : ℕ) : Prop := ArithmeticFunction.sigma 1 n  = 2 * n

/-- Euler's form of an odd perfect number: `n = p^a * m^2`, with constraints on `p`, `a`, and `m`. -/
def oddPerfectForm (n : ℕ) : Prop :=
  ∃ (p a m : ℕ), p.Prime ∧ a % 4 = 1 ∧ Nat.gcd p m = 1 ∧ n = p^a * m^2

-- Assuming p is a natural number and a is a natural number (with a ≥ 1)
lemma pow_mul_pow_sub_one (p a : ℕ) (ha : a ≥ 1) :
  p^a = p * p^(a - 1) := by
  rw [← Nat.succ_pred_eq_of_pos ha, Nat.pow_succ, mul_comm]
  congr

/--
Key modular lemma: For any prime `r` not dividing `n`,
there exists a prime `q ∣ n` such that `q ≡ 1 mod r`.
-/
lemma keyModularLemma
    (n : ℕ)
    (h_perf : isPerfect n)
    (h_form : oddPerfectForm n)
    (r : ℕ) (hr : Nat.Prime r) (hrn : ¬ r ∣ n) (ho: r > 2) :
    ∃ q : ℕ, Nat.Prime q ∧ q ∣ n ∧ q % r = 1 := by

  rcases h_form with ⟨p, a, m, hp, ha, hcop, hn⟩
  have h_pa : n = p^a * m^2 := hn

  -- Show p ∣ n trivially from Euler form
  have hpn : p ∣ n := by
    have ha1 : a ≥ 1 := Nat.pos_of_ne_zero (by intro h; rw [h, Nat.zero_mod] at ha; exact zero_ne_one ha)
    rw [h_pa, pow_mul_pow_sub_one p a ha1, mul_assoc, mul_comm p (p^(a-1) * m^2)]
    exact Nat.dvd_mul_left p (p^(a-1) * m^2)

  -- Use definition of isPerfect
  have hsig : ArithmeticFunction.sigma 1 n = 2 * n := h_perf

  -- sigma(n) = sigma(p^a) * sigma(m^2) by multiplicativity
  have hcop' : Nat.Coprime (p^a) (m^2) := by
    apply Nat.Coprime.pow
    exact Nat.coprime_iff_gcd_eq_one.mpr hcop

  have sigma_n_eq : ArithmeticFunction.sigma 1 (p^a * m^2) =
                   (ArithmeticFunction.sigma 1 (p^a)) * (ArithmeticFunction.sigma 1 (m^2)) := by
    refine IsMultiplicative.map_mul_of_coprime ArithmeticFunction.isMultiplicative_sigma hcop'

  -- Now suppose no q ∣ n satisfies q ≡ 1 mod r
  by_contra! H
  -- That is: ∀ q, if q ∣ n and q is prime, then q % r ≠ 1

  -- Claim: Then for all such q, σ(q^e) ≡ 0 mod r
  -- Which implies r ∣ σ(n) = 2n ⇒ r ∣ n, contradiction
  -- So ∃ q ∣ n with q ≡ 1 mod r

  have r_not_div_sigma : ¬ r ∣ ArithmeticFunction.sigma 1 n := by
    rw [hsig]
    apply Nat.Prime.not_dvd_mul hr
    intro contra
    have hr2 : r = 2 := by
      have hle : r ≤ 2 := Nat.le_of_dvd (by norm_num) contra
      have hge : 2 ≤ r := Nat.Prime.two_le hr
      exact le_antisymm hle hge
    subst hr2
    linarith [ho]
    exact hrn

  -- If (p - 1) % r = 0, then r ∣ (p - 1) ⇒ r ∣ p ⇒ r = p ⇒ r ∣ n, contradiction
  have hp_mod_r0 : p % r ≠ 0 := by
    intro h
    have : r ∣ p := by rw [Nat.dvd_iff_mod_eq_zero]; exact h
    have : r ∣ n := Nat.dvd_trans this hpn
    exact hrn this

  -- We already assumed: ∀ q : ℕ, q.Prime → q ∣ n → q % r ≠ 1
  -- So in particular:
  have hp_mod_r1 : p % r ≠ 1 := H p hp hpn

  -- We now show σ(p^a) ≡ 0 mod r under this assumption
  -- Recall: σ(p^a) = (p^{a+1} - 1)/(p - 1)

  -- Since p % r ≠ 0 (as r ∤ n ⇒ r ≠ p), and p % r ≠ 1 by assumption, (p - 1) mod r ≠ 0
  -- So (p - 1) is invertible mod r

  have hndiv_r : ¬ r ∣ p-1 := by
    sorry

  have h_gcd : Nat.gcd (p-1) r = 1 := by
    -- If gcd(p-1, r) ≠ 1, then r ∣ (p-1) since r is prime
    sorry
  have : Nat.Coprime (p-1) r := h_gcd  -- already proved
  have sigma_pa := ArithmeticFunction.sigma 1 p^a
  have sigma_eq_closed : sigma_pa = (p^(a+1) - 1) / (p-1) := by
    sorry
  have sigma_eq_0 : (p^(a+1) - 1) / (p-1) = 0 % r := by
    sorry
  have sigma_eq_0_mul : (p^(a+1)-1) = 0 % r := by
    sorry

  -- Now conclude:
  have : r ∣ ArithmeticFunction.sigma 1 (p^a) := by
    sorry

  -- σ(p^a) ≡ 0 mod r ⇔ p^{a+1} ≡ 1 mod r
  -- So σ(p^a) ≡ 0 mod r under this assumption
  -- Similarly, all primes dividing m must satisfy q % r ≠ 1
  -- And so each σ(q^e) ≡ 0 mod r, making σ(m^2) ≡ 0 mod r

  -- Therefore: σ(p^a) * σ(m^2) ≡ 0 mod r ⇒ σ(n) ≡ 0 mod r
  -- But we previously proved r ∤ σ(n), contradiction
  have contradiction : r ∣ ArithmeticFunction.sigma 1 (p^a * m^2) := by
    rw [sigma_n_eq]
    apply dvd_mul_of_dvd_left
    -- We'll show σ(p^a) ≡ 0 mod r
    -- Since σ(p^a) = (p^{a+1} - 1)/(p - 1), and denom invertible mod r, numer ≡ 0 ⇒ whole ≡ 0
    -- So r ∣ (p^{a+1} - 1)
    have num_mod : (p^(a + 1) - 1) % r = 0 := by
      -- Use little Fermat or Z/nZ field properties
      -- We're assuming p^(a+1) ≡ 1 mod r from earlier
      sorry -- You could optionally prove this exponent congruence here
    -- Then r ∣ numerator, so r ∣ σ(p^a)
    have : r ∣ ArithmeticFunction.sigma 1 (p^a) := by
      -- Apply lemma: if numerator divisible and denom invertible mod r ⇒ entire expr divisible
      sorry
    expose_names; exact this_2

  rw [h_pa] at r_not_div_sigma

  exact absurd contradiction r_not_div_sigma

[Jonas Whidden]

have hp_mod_r1 : p % r ≠ 1 := H p hp hpn

  -- We now show σ(p^a) ≡ 0 mod r under this assumption
  -- Recall: σ(p^a) = (p^{a+1} - 1)/(p - 1)

  -- Since p % r ≠ 0 (as r ∤ n ⇒ r ≠ p), and p % r ≠ 1 by assumption, (p - 1) mod r ≠ 0
  -- So (p - 1) is invertible mod r

  have hndiv_r : ¬ r ∣ p-1 := by
    sorry

This part I feel should be trivial, but I can't ever find the correct functions to use to make the leaps. Lean search was helping a bit, but it's stopped giving any results since earlier today for some reason. Just searching the docs, I can find some things related to proving/disproving division based on mod zero and modular subtraction/adding/canceling, but I can't massage the form that I have it in to be able to apply any of them, because support for modular inequalities seems to be lacking. In a handful of cases I've used apply?/rw?/exact? to actually find what I need, but more often than not it can't figure it out or recommends unrelated stuff...

I'm sure it's all pretty simple when you have a firmer background in lean, but it's just absolutely defeating that google and AI are no help, and you just kind of stumble around blindly until you guess the right pattern (or not)... Just to subtract 1 from both sides I've lost like half a day and still didn't accomplish it, and I'm not even certain that will lead directly to the tiny goal that r does not divide (p-1) if I do manage to figure it out, or how long it'll take for me to find the exact function I need to show the next part...