Mathoverflow 75792

Various questions about integer complexity, which is the minimum number of 1s needed to express a natural number using addition, multiplication, and parentheses.

Let ‖n‖ denote the integer complexity of n > 0.

• It is known that ‖3^n‖ = 3n for n > 0.
• Is it true that ‖2^n‖ = 2n for n > 0?
• The corresponding conjecture for 5 is false, because 5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

We have chosen to formalise this using an inductive type.

References:

• mathoverflow/75792 by user Harry Altman
• http://arxiv.org/abs/1203.6462 by Jānis Iraids, Kaspars Balodis, Juris Čerņenoks, Mārtiņš Opmanis, Rihards Opmanis, Kārlis Podnieks
• http://arxiv.org/abs/1207.4841 by Harry Altman, Joshua Zelinsky
• https://oeis.org/A005245 : Mahler-Popken complexity.

inductive Mathoverflow75792.Reachable : ℕ → ℕ → Prop

The inductively defined predicate that m is reachable in n steps.

• 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 Mathoverflow75792.Reachable.self (n : ℕ) (hn : 0 < n) : Reachable n n

theorem Mathoverflow75792.not_reachable_zero_fst (n : ℕ) : ¬Reachable 0 n

theorem Mathoverflow75792.not_reachable_zero_snd (m : ℕ) : ¬Reachable m 0

theorem Mathoverflow75792.Reachable.dec {m n : ℕ} (h : Reachable m n) : ∃ (m' : ℕ) (n' : ℕ), m' + 1 = m ∧ n' + 1 = n

theorem Mathoverflow75792.Reachable.le {m n₁ n₂ : ℕ} (hn : n₁ ≤ n₂) (hm : Reachable m n₁) : Reachable m n₂

theorem Mathoverflow75792.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)

@[irreducible]

instance Mathoverflow75792.Reachable.decide (m n : ℕ) : Decidable (Reachable m n)

Equations

• One or more equations did not get rendered due to their size.
• Mathoverflow75792.Reachable.decide 0 x✝ = isFalse ⋯
• Mathoverflow75792.Reachable.decide 1 0 = isFalse Mathoverflow75792.Reachable.decide._proof_1
• Mathoverflow75792.Reachable.decide 1 n.succ = isTrue ⋯

def Mathoverflow75792.complexity (n : ℕ) : ℕ

The (Mahler-Popken) complexity of n: the minimum number of 1s needed to express a given number using only addition and multiplication. E.g. 2 = 1 + 1, so complexity 2 = 2.

Equations

• Mathoverflow75792.complexity n = if h : n = 0 then 0 else Nat.find ⋯

theorem Mathoverflow75792.Reachable.complexity_le {m n : ℕ} (h : Reachable m n) : Mathoverflow75792.complexity m ≤ n

theorem Mathoverflow75792.Reachable.complexity_eq {m n : ℕ} (h : Reachable m n) (min : ∀ n' < n, ¬Reachable m n') : Mathoverflow75792.complexity m = n

theorem Mathoverflow75792.Reachable.complexity {n : ℕ} (hn : 0 < n) : Reachable n (Mathoverflow75792.complexity n)

theorem Mathoverflow75792.complexity_zero : complexity 0 = 0

theorem Mathoverflow75792.complexity_one : complexity 1 = 1

theorem Mathoverflow75792.complexity_two : complexity 2 = 2

theorem Mathoverflow75792.Reachable.pow (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : Reachable (m ^ n) (m * n)

theorem Mathoverflow75792.Reachable.pow' (m n : ℕ+) : Reachable (↑m ^ ↑n) (↑m * ↑n)

theorem Mathoverflow75792.Reachable.five_pow_six : Reachable (5 ^ 6) 29

5^6 = 15625 = 1 + 2^3 * 3^2 * (1 + 2^3 * 3^3)!

theorem Mathoverflow75792.complexity_five_pow : (∀ (n : ℕ), 0 < n → complexity (5 ^ n) = 5 * n) ↔ False

Is 5n the complexity of 5^n for 0 < n? Answer: No.

theorem Mathoverflow75792.complexity_three_pow : (∀ (n : ℕ), 0 < n → complexity (3 ^ n) = 3 * n) ↔ True

Is 3n the complexity of 3^n for 0 < n? Answer: Yes, by John Selfridge.

Reference: https://arxiv.org/abs/1207.4841

theorem Mathoverflow75792.complexity_two_pow : (∀ (n : ℕ), 0 < n → complexity (2 ^ n) = 2 * n) ↔ sorry

Is 2n the complexity of 2^n for 0 < n?