Bonza functions (Lean): f(3) ≠ 9 via the prime congruence lemma modulo 5

Result

For a bonza function $f:\mathbb N\to\mathbb N$ (i.e. $f(a)\mid b^a-f(b)^{f(a)}$ for all $a,b\ge 1$), we prove in Lean:

$$f(3)\ne 9.$$

Together with /[yau9pr]/ (which proves $f(3)\in{1,3,9}$), this reduces the analysis of $f(3)$ to the two cases $f(3)=1$ and $f(3)=3$.

Proof idea

Assume $f(3)=9$.

1. Apply bonza at $(a,b)=(3,5)$: $$9\mid 5^3 - f(5)^9.$$ If $f(5)=1$ then the RHS equals $124$, not divisible by $9$; hence $f(5)\ne 1$.
2. Now apply the prime congruence lemma /[9sk7zo]/ with $p=5$ (valid since $f(5)\ne 1$): $$f(3)\equiv 3\pmod 5.$$ But $f(3)=9\equiv 4\pmod 5$, contradiction.

Lean formalization

The attached file compiles with no sorry.

It includes a standalone proof of the congruence lemma (matching /[9sk7zo]/) to avoid project-level import issues.

File: BonzaF3NotNine.lean

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic

/-- Bonza property, stated in `ℤ` to avoid subtraction issues in `ℕ`. -/
def Bonza (f : ℕ → ℕ) : Prop :=
  (∀ a b : ℕ, 0 < a → 0 < b → (f a : ℤ) ∣ (b : ℤ) ^ a - (f b : ℤ) ^ (f a)) ∧
  (∀ n : ℕ, 0 < n → 0 < f n)

namespace Bonza

open Nat

variable {f : ℕ → ℕ}

/-- From bonza: if `a>0` then `(f a : ℤ) ∣ (a : ℤ)^a`. -/
lemma int_dvd_self_pow (hf : Bonza f) {a : ℕ} (ha : 0 < a) : (f a : ℤ) ∣ (a : ℤ) ^ a := by
  have hdiv := hf.1 a a ha ha
  have hpow : (f a : ℤ) ∣ (f a : ℤ) ^ (f a) := by
    have hfa0 : f a ≠ 0 := Nat.ne_of_gt (hf.2 a ha)
    exact dvd_pow_self (f a : ℤ) (hn := by
      intro hn
      exact hfa0 (by simpa using hn))
  have := dvd_add hdiv hpow
  simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using this

/-- In `ZMod p` for prime `p`, one has `x^(p^k) = x` for all `k`. -/
lemma zmod_pow_prime_pow (p : ℕ) [Fact p.Prime] (x : ZMod p) :
    ∀ k : ℕ, x ^ (p ^ k) = x := by
  intro k
  induction k with
  | zero => simp
  | succ k ih =>
      simpa [pow_succ, pow_mul, ih] using (ZMod.pow_card (p := p) (x := x))

/--
If `p` is prime and `f(p) ≠ 1`, then for all `b>0` we have `f(b) ≡ b (mod p)`.

(Standalone proof; compare /[9sk7zo/].)
-/
theorem cong_mod_prime_of_f_ne_one (hf : Bonza f) {p : ℕ} (hp : Nat.Prime p) (hfp : f p ≠ 1) :
    ∀ b : ℕ, 0 < b → (f b : ZMod p) = (b : ZMod p) := by
  classical
  have hposp : 0 < p := hp.pos

  have hfpdiv : f p ∣ p ^ p := by
    have hz : (f p : ℤ) ∣ (p : ℤ) ^ p := int_dvd_self_pow (f := f) hf hposp
    exact Int.ofNat_dvd.mp (by simpa using hz)

  rcases (Nat.dvd_prime_pow hp (i := f p) (m := p)).1 (by simpa using hfpdiv) with ⟨k, hk, hkEq⟩
  have hkpos : 0 < k := by
    by_contra hk0
    have : k = 0 := Nat.eq_zero_of_not_pos hk0
    subst this
    exact hfp (by simpa [hkEq])

  haveI : Fact p.Prime := ⟨hp⟩

  intro b hbpos

  have hdivZ : (f p : ℤ) ∣ (b : ℤ) ^ p - (f b : ℤ) ^ (f p) := hf.1 p b hposp hbpos

  have hp_dvd_fp : (p : ℤ) ∣ (f p : ℤ) := by
    have hk0 : k ≠ 0 := Nat.ne_of_gt hkpos
    rcases Nat.exists_eq_succ_of_ne_zero hk0 with ⟨k1, rfl⟩
    have : p ∣ f p := by
      simpa [hkEq] using (dvd_pow_self p (Nat.succ_ne_zero k1))
    exact Int.ofNat_dvd.mpr this

  have hp_dvd_diff : (p : ℤ) ∣ (b : ℤ) ^ p - (f b : ℤ) ^ (f p) := dvd_trans hp_dvd_fp hdivZ

  have hzmod : (((b : ℤ) ^ p - (f b : ℤ) ^ (f p) : ℤ) : ZMod p) = 0 :=
    (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).2 hp_dvd_diff

  have hbpow : (b : ZMod p) ^ p = (b : ZMod p) := by
    simpa using (ZMod.pow_card (p := p) (x := (b : ZMod p)))
  have hfbpow : (f b : ZMod p) ^ (f p) = (f b : ZMod p) := by
    simpa [hkEq] using (zmod_pow_prime_pow (p := p) (x := (f b : ZMod p)) k)

  have hz1 : (b : ZMod p) ^ p - (f b : ZMod p) ^ (f p) = 0 := by
    simpa using hzmod
  have hz2 : (b : ZMod p) - (f b : ZMod p) = 0 := by
    simpa [hbpow, hfbpow] using hz1

  exact (sub_eq_zero.mp hz2).symm

/-- A bonza function cannot satisfy `f 3 = 9`. -/
theorem f3_ne_nine (hf : Bonza f) : f 3 ≠ 9 := by
  intro h9
  have hbonza35 := hf.1 3 5 (by decide) (by decide)
  have hdiv : (9 : ℤ) ∣ (5 : ℤ) ^ 3 - (f 5 : ℤ) ^ (9 : ℕ) := by
    simpa [h9] using (show (f 3 : ℤ) ∣ (5 : ℤ) ^ 3 - (f 5 : ℤ) ^ (f 3) from hbonza35)

  have hf5ne1 : f 5 ≠ 1 := by
    intro h1
    have : ¬ (9 : ℤ) ∣ (5 : ℤ) ^ 3 - (1 : ℤ) ^ (9 : ℕ) := by decide
    exact this (by simpa [h1] using hdiv)

  have hcong : (f 3 : ZMod 5) = (3 : ZMod 5) :=
    cong_mod_prime_of_f_ne_one (f := f) hf (p := 5) (by decide) hf5ne1 3 (by decide)

  have : (9 : ZMod 5) = (3 : ZMod 5) := by
    simpa [h9] using hcong

  have : (4 : ZMod 5) = (3 : ZMod 5) := by
    simpa using this
  exact (by decide : (4 : ZMod 5) ≠ (3 : ZMod 5)) this

end Bonza