Bonza functions: the 2-power case implies the sharp bound f(n) ≤ 4n (Lean, via 2-adic LTE and a ZMod 4 parity obstruction)

Summary

Let $f:\mathbb N\to\mathbb N$ be bonza, i.e. $f(a)$ divides $b^a-f(b)^{f(a)}$ for all positive integers $a,b$.

This note proves the following partial upper bound in Lean:

If $f(p)=1$ for every odd prime $p$, then $f(n)\le 4n$ for all $n\ge 1$.

This is one of the two natural branches expected in a full solution $c=4$.

The proof combines:

• the standard “no odd prime divides $f(n)$, hence $f(n)=2^k$” argument (also used in /[vk9j9i]/);
• a divisibility specialization at $b=3$;
• the 2-adic/LTE bound for $3^n-1$ from /[xhgjfh/];
• an elementary parity obstruction modulo $4$ (using ZMod 4) to control the odd-$n$ case.

Lean formalization

The attached file BonzaTwoPowerBound.lean compiles with no sorry.

Main declaration:

• Bonza.linear_bound_of_all_odd_primes_eq_one.

File contents

-- BonzaTwoPowerBound.lean
import Mathlib.NumberTheory.Multiplicity
import Mathlib.NumberTheory.Padics.PadicVal.Basic
import Mathlib.Data.Nat.Factors
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic

/-!
# Bonza functions: the 2-power case gives the sharp bound $f(n) \le 4n$

We consider functions $f : \mathbb{N} \to \mathbb{N}$ intended to be defined on positive integers.
Because the bonza difference can be negative, we express divisibility in $\mathbb{Z}$.

Main result of this file:

* If $f$ is bonza and $f(p)=1$ for every odd prime $p$, then $f(n) \le 4n$ for all $n>0$.

This uses the 2-adic LTE bound for $3^n - 1$ from /[xhgjfh]/ and basic bonza lemmas from /[vk9j9i]/.
-/

/-- 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 : ℕ → ℕ}

lemma pos (hf : Bonza f) {n : ℕ} (hn : 0 < n) : 0 < f n := hf.2 n hn

/-- If all odd primes map to `1`, then no odd prime divides any `f(n)`. -/
lemma no_odd_prime_dvd (hf : Bonza f)
    (hodd : ∀ p : ℕ, p.Prime → p ≠ 2 → f p = 1)
    {n : ℕ} (hn : 0 < n) :
    ∀ p : ℕ, p.Prime → p ≠ 2 → ¬ p ∣ f n := by
  intro p hp hp2 hpn
  have hb : 0 < p := hp.pos
  have hdiv := hf.1 n p hn hb
  have hfp : f p = 1 := hodd p hp hp2
  have hdiv1 : (f n : ℤ) ∣ (p : ℤ) ^ n - (1 : ℤ) := by
    simpa [hfp] using hdiv
  have hpnZ : (p : ℤ) ∣ (f n : ℤ) := by
    exact_mod_cast hpn
  have hp_div : (p : ℤ) ∣ (p : ℤ) ^ n - 1 := dvd_trans hpnZ hdiv1
  have hp_pow : (p : ℤ) ∣ (p : ℤ) ^ n := by
    exact dvd_pow_self (p : ℤ) (Nat.ne_of_gt hn)
  have hone : (p : ℤ) ∣ (1 : ℤ) := by
    have : (p : ℤ) ∣ (p : ℤ) ^ n - ((p : ℤ) ^ n - 1) := dvd_sub hp_pow hp_div
    simpa using this
  have : p ∣ 1 := by
    exact_mod_cast hone
  exact hp.not_dvd_one this

/-- If all odd primes map to `1`, then each `f(n)` is a power of `2`. -/
lemma exists_eq_two_pow (hf : Bonza f)
    (hodd : ∀ p : ℕ, p.Prime → p ≠ 2 → f p = 1)
    {n : ℕ} (hn : 0 < n) :
    ∃ k : ℕ, f n = 2 ^ k := by
  rcases Nat.eq_two_pow_or_exists_odd_prime_and_dvd (f n) with h | h
  · exact ⟨h.choose, h.choose_spec⟩
  · rcases h with ⟨p, hp, hpdvd, hpodd⟩
    have hp2 : p ≠ 2 := by
      intro h2
      subst h2
      have : ¬ Odd (2 : ℕ) := by decide
      exact this hpodd
    exact False.elim ((no_odd_prime_dvd (f := f) hf hodd hn p hp hp2) hpdvd)

end Bonza

namespace TwoAdicBound

open Nat

/-- From /[xhgjfh]/: for positive even `n`, any `2^k ∣ 3^n-1` satisfies `2^k ≤ 4n`. -/
theorem two_pow_le_four_mul (n k : ℕ) (hn : 0 < n) (hneven : Even n)
    (hk : 2^k ∣ 3^n - 1) : 2^k ≤ 4*n := by
  have hn0 : n ≠ 0 := Nat.ne_of_gt hn

  have h3n : 3^n - 1 ≠ 0 := by
    rcases Nat.exists_eq_succ_of_ne_zero hn0 with ⟨m, rfl⟩
    have h1 : 1 ≤ 3^m := Nat.one_le_pow m 3 (by decide)
    have hge : 3 ≤ 3^m * 3 := by
      simpa [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using (Nat.mul_le_mul_right 3 h1)
    have : 3 ≤ 3^m.succ := by
      simpa [pow_succ] using hge
    exact Nat.sub_ne_zero_of_lt (lt_of_lt_of_le (by decide : 1 < 3) this)

  have hk_le : k ≤ padicValNat 2 (3^n - 1) := by
    haveI : Fact (Nat.Prime 2) := ⟨by decide⟩
    exact (padicValNat_dvd_iff_le (p := 2) (a := 3^n - 1) (n := k) h3n).1 (by
      simpa using hk)

  have hv2 : padicValNat 2 (3^n - 1) = padicValNat 2 n + 2 := by
    have hxy : 2 ∣ (3:ℕ) - 1 := by decide
    have hx : ¬ 2 ∣ (3:ℕ) := by decide
    have h := padicValNat.pow_two_sub_pow (x := 3) (y := 1)
      (hyx := by decide) (hxy := hxy) (hx := hx) (hn := hn0) (hneven := hneven)
    have h1 : padicValNat 2 (3^n - 1) + 1 = padicValNat 2 4 + padicValNat 2 2 + padicValNat 2 n := by
      simpa using h
    haveI : Fact (Nat.Prime 2) := ⟨by decide⟩
    have h4 : padicValNat 2 4 = 2 := by
      simpa [pow_two] using (padicValNat.prime_pow (p := 2) 2)
    have h2 : padicValNat 2 2 = 1 := by
      simpa using (padicValNat.prime_pow (p := 2) 1)
    have h3 : padicValNat 2 (3^n - 1) + 1 = padicValNat 2 n + 3 := by
      simpa [h4, h2, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using h1
    have hs : Nat.succ (padicValNat 2 (3^n - 1)) = Nat.succ (padicValNat 2 n + 2) := by
      simpa [Nat.succ_eq_add_one, Nat.add_assoc] using h3
    exact Nat.succ_inj.1 hs

  have hpowle : 2^k ≤ 2^(padicValNat 2 n + 2) := by
    have : k ≤ padicValNat 2 n + 2 := by
      calc
        k ≤ padicValNat 2 (3^n - 1) := hk_le
        _ = padicValNat 2 n + 2 := hv2
    exact pow_le_pow_right' (by decide : (1:ℕ) ≤ 2) this

  have hpow : 2^(padicValNat 2 n + 2) = 4 * 2^(padicValNat 2 n) := by
    simp [pow_add, pow_two, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

  have hdiv : 2^(padicValNat 2 n) ∣ n := pow_padicValNat_dvd (p := 2) (n := n)
  have hle : 2^(padicValNat 2 n) ≤ n := le_of_dvd hn hdiv

  calc
    2^k ≤ 2^(padicValNat 2 n + 2) := hpowle
    _ = 4 * 2^(padicValNat 2 n) := hpow
    _ ≤ 4 * n := by gcongr
    _ = 4*n := by ring

end TwoAdicBound

namespace Bonza

open Nat

/-- If `n` is odd, then `4 ∤ 3^n - 1`. -/
lemma four_not_dvd_three_pow_sub_one_of_odd {n : ℕ} (hnodd : Odd n) : ¬ 4 ∣ 3^n - 1 := by
  have hle : 1 ≤ 3 ^ n := one_le_pow_of_one_le' (a := 3) (by decide : (1:ℕ) ≤ 3) n
  have hcast : ((3^n - 1 : ℕ) : ZMod 4) = (3 : ZMod 4)^n - 1 := by
    simpa [Nat.cast_pow, Nat.cast_sub hle]
  have h3 : (3 : ZMod 4) = (-1 : ZMod 4) := by decide
  have hpow : (3 : ZMod 4)^n = -1 := by
    have : ((-1 : ZMod 4) ^ n) = (-1 : ZMod 4) := hnodd.neg_one_pow
    simpa [h3] using this
  have hneq : ((3^n - 1 : ℕ) : ZMod 4) ≠ 0 := by
    have : ((3^n - 1 : ℕ) : ZMod 4) = (2 : ZMod 4) := by
      -- compute: `(-1) - 1 = 2` in `ZMod 4`
      calc
        ((3^n - 1 : ℕ) : ZMod 4) = (3 : ZMod 4)^n - 1 := hcast
        _ = (-1 : ZMod 4) - 1 := by simpa [hpow]
        _ = (2 : ZMod 4) := by decide
    simpa [this] using (by decide : (2 : ZMod 4) ≠ 0)
  intro hdiv
  have : ((3^n - 1 : ℕ) : ZMod 4) = 0 := (ZMod.natCast_eq_zero_iff _ _).2 hdiv
  exact hneq this

/--
The 2-power case bound: if `f` is bonza and `f(p)=1` for every odd prime `p`, then
`f(n) ≤ 4*n` for all `n>0`.
-/
theorem linear_bound_of_all_odd_primes_eq_one {f : ℕ → ℕ} (hf : Bonza f)
    (hodd : ∀ p : ℕ, p.Prime → p ≠ 2 → f p = 1) :
    ∀ n : ℕ, 0 < n → f n ≤ 4 * n := by
  intro n hn
  rcases Bonza.exists_eq_two_pow (f := f) hf hodd hn with ⟨k, hk⟩
  have h3prime : (3:ℕ).Prime := by decide
  have h3 : f 3 = 1 := hodd 3 h3prime (by decide)
  have hdivZ : (f n : ℤ) ∣ (3 : ℤ)^n - (f 3 : ℤ)^(f n) := hf.1 n 3 hn (by decide)
  have hdivZ' : (f n : ℤ) ∣ (3 : ℤ)^n - 1 := by
    simpa [h3] using hdivZ
  have hle : 1 ≤ 3 ^ n := one_le_pow_of_one_le' (a := 3) (by decide : (1:ℕ) ≤ 3) n
  have hz : (3 : ℤ) ^ n - 1 = ((3 ^ n - 1 : ℕ) : ℤ) := by
    have hz1 : ((3 : ℤ) ^ n) = (3 ^ n : ℤ) := by
      simpa [Nat.cast_pow]
    calc
      (3 : ℤ) ^ n - 1 = (3 ^ n : ℤ) - (1 : ℤ) := by simpa [hz1]
      _ = ((3 ^ n - 1 : ℕ) : ℤ) := by
            simpa using (Int.ofNat_sub hle).symm
  have hdivZ'' : (f n : ℤ) ∣ ((3 ^ n - 1 : ℕ) : ℤ) := by
    rw [← hz]
    exact hdivZ'
  have hdivN : f n ∣ 3 ^ n - 1 := Int.ofNat_dvd.mp (by simpa using hdivZ'')
  have hdivPow : 2^k ∣ 3^n - 1 := by simpa [hk] using hdivN

  rcases Nat.even_or_odd n with hneven | hnodd
  · have hlePow : 2^k ≤ 4*n := TwoAdicBound.two_pow_le_four_mul n k hn hneven hdivPow
    simpa [hk, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm] using hlePow
  · have h4ndiv : ¬ 4 ∣ 3^n - 1 := four_not_dvd_three_pow_sub_one_of_odd (n := n) hnodd
    have hk_le1 : k ≤ 1 := by
      by_contra hk2
      have hk2' : 2 ≤ k := by
        exact (Nat.succ_le_iff.2 (Nat.lt_of_not_ge hk2))
      have : 4 ∣ 3^n - 1 := by
        have h4 : 4 ∣ 2^k := pow_dvd_pow 2 hk2'
        exact dvd_trans h4 hdivPow
      exact h4ndiv this
    have hpowle2 : 2^k ≤ 2 := by
      have : 2^k ≤ 2^1 := pow_le_pow_right' (by decide : (1:ℕ) ≤ 2) hk_le1
      simpa using this
    have h2le4n : 2 ≤ 4*n := by
      have hn1 : 1 ≤ n := Nat.succ_le_iff.2 hn
      have : 4 ≤ 4*n := Nat.mul_le_mul_left 4 hn1
      exact le_trans (by decide : 2 ≤ 4) this
    have : 2^k ≤ 4*n := le_trans hpowle2 h2le4n
    simpa [hk] using this

end Bonza

Mathematical proof sketch

Assume $f(p)=1$ for all odd primes $p$.

1. For any $n\ge 1$, if an odd prime $p$ divides $f(n)$, then applying bonza with $(a,b)=(n,p)$ gives $f(n)\mid p^n-1$; but also $p\mid p^n$, hence $p\mid 1$, contradiction. Therefore $f(n)$ has no odd prime factor, so $f(n)=2^k$.
2. Apply bonza with $(a,b)=(n,3)$ (and $f(3)=1$) to get $2^k \mid 3^n-1$.
3. If $n$ is even, apply /[xhgjfh]/ to obtain $2^k\le 4n$.
4. If $n$ is odd, then $3\equiv -1\pmod 4$ implies $3^n-1\equiv -2\equiv 2\pmod 4$, so $4\nmid 3^n-1$; hence $k\le 1$ and $2^k\le 2\le 4n$.

Thus $f(n)=2^k\le 4n$ for all $n\ge 1$.

Notes

• This is not yet a full solution of the original problem (we still need the complementary branch when some odd prime has $f(p)>1$).
• Together with the extremal construction /[aytljc]/ (showing $c\ge 4$), this makes $c=4$ very plausible.