Integer complexity

InductiveExpressions built from one, addition and multiplication#✓fully proved

An expression is either the constant \(1\), or a sum \(e_1 + e_2\) of two expressions, or a product \(e_1 \times e_2\) of two expressions. Expressions are formal syntax trees, so the tree structure plays the role of parentheses.

inductive Expr where
  | one : Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr
  deriving DecidableEq, Repr
Sources
  • C2.
Used by 11
Used byInteger complexity · Integer complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · Number of ones in an expression · Value of an expression · Every positive integer is the value of an expression · The \(1\)-ary complexity is the integer complexity · Integer-complexity expressions as \(1\)-ary Mahler–Popken expressions · Achievable numbers of ones · \(1\)-ary Mahler–Popken expressions as integer-complexity expressions

DefinitionValue of an expression#✓fully proved

The value of an expression is the natural number obtained by evaluating it: the constant \(1\) has value \(1\), the value of \(e_1 + e_2\) is the sum of the values of \(e_1\) and \(e_2\), and the value of \(e_1 \times e_2\) is the product of their values.

def eval : Expr → ℕ
  | .one => 1
  | .add a b => a.eval + b.eval
  | .mul a b => a.eval * b.eval
Sources
  • C2.
Uses 1 · Used by 7
Statement usesExpressions built from one, addition and multiplication
Used byInteger complexity · Integer complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · Every positive integer is the value of an expression · The \(1\)-ary complexity is the integer complexity · Achievable numbers of ones

DefinitionNumber of ones in an expression#✓fully proved

The number of ones of an expression is the number of occurrences of the constant \(1\) in it: the constant \(1\) has one, and both \(e_1 + e_2\) and \(e_1 \times e_2\) have as many as \(e_1\) and \(e_2\) together.

def count : Expr → ℕ
  | .one => 1
  | .add a b => a.count + b.count
  | .mul a b => a.count + b.count
Sources
  • C3.
Uses 1 · Used by 6
Statement usesExpressions built from one, addition and multiplication
Used byInteger complexity · Integer complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · The \(1\)-ary complexity is the integer complexity · Achievable numbers of ones

TheoremEvery positive integer is the value of an expression#✓fully proved

For every natural number \(n > 0\) there is an expression whose value is \(n\).

theorem exists_expr_of_pos {n : ℕ} (h : 0 < n) : ∃ e : Expr, e.eval = n
Sources
  • C2/C4 existence side.
Uses 2 · Used by 5
Statement usesExpressions built from one, addition and multiplication · Value of an expression
Used byInteger complexity · Integer complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · The \(1\)-ary complexity is the integer complexity

DefinitionAchievable numbers of ones#✓fully proved

For a positive integer \(n\) and a natural number \(c\), the predicate holds when some expression has value \(n\) and exactly \(c\) ones.

def Pred (n : ℕ+) (c : ℕ) : Prop := ∃ e : Expr, e.eval = (n : ℕ) ∧ e.count = c
Sources
  • replaces Set S.
Uses 3 · Used by 5
Statement usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression
Used byInteger complexity · Integer complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · The \(1\)-ary complexity is the integer complexity

DefinitionInteger complexity#✓fully proved

The integer complexity of a positive integer \(n\) is the least number of ones in an expression whose value is \(n\), that is, the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses.

noncomputable def complexity (n : ℕ+) : ℕ := by
  classical
  exact Nat.find (Pred_nonempty n)
Sources
  • C4. Implemented via Nat.find on proved existential predicate.
Uses 5 · Used by 5
Statement usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression · Achievable numbers of ones · Every positive integer is the value of an expression
Used byInteger complexity of a sum · Expressions bound the integer complexity from above · Integer complexity of a product · Integer complexity extended to all natural numbers · The \(1\)-ary complexity is the integer complexity

TheoremExpressions bound the integer complexity from above#✓fully proved

Let \(n\) be a positive integer. If an expression \(e\) has value \(n\), then the integer complexity of \(n\) is at most the number of ones of \(e\).

theorem complexity_le {n : ℕ+} {e : Expr} (he : e.eval = (n : ℕ)) : complexity n ≤ e.count
Sources
  • C4.
Uses 6 · Used by 3
Statement usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression · Integer complexity
Proof usesAchievable numbers of ones · Every positive integer is the value of an expression
Used byInteger complexity of a sum · Integer complexity of a product · The \(1\)-ary complexity is the integer complexity

TheoremInteger complexity of a sum#✓fully proved

For all positive integers \(a\) and \(b\), the integer complexity of \(a + b\) is at most the sum of the integer complexities of \(a\) and \(b\).

theorem complexity_add_le (a b : ℕ+) : complexity (a + b) ≤ complexity a + complexity b
Uses 7
Statement usesInteger complexity
Proof usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression · Achievable numbers of ones · Expressions bound the integer complexity from above · Every positive integer is the value of an expression

TheoremInteger complexity of a product#✓fully proved

For all positive integers \(a\) and \(b\), the integer complexity of \(ab\) is at most the sum of the integer complexities of \(a\) and \(b\).

theorem complexity_mul_le (a b : ℕ+) : complexity (a * b) ≤ complexity a + complexity b
Uses 7
Statement usesInteger complexity
Proof usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression · Achievable numbers of ones · Expressions bound the integer complexity from above · Every positive integer is the value of an expression

DefinitionInteger complexity extended to all natural numbers#✓fully proved

For a natural number \(n\), the value \(\lVert n \rVert\) is the integer complexity of \(n\) when \(n\) is positive, that is, the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses, and \(\lVert 0 \rVert = 0\).

noncomputable def cx (n : ℕ) : ℕ :=
  if h : 0 < n then IntegerComplexity.complexity ⟨n, h⟩ else 0
Uses 1 · Used by 11
Statement usesInteger complexity
Used byThe set \(T_0\) built from stable numbers · The set \(T_0\) is nonnegative · Stable numbers for integer complexity · Stable complexity · Stable complexity of a stable number · Integer complexity as a minimum over factorizations and sums · The function \(g\) bounds integer complexity from below · Integers above \(2^a 3^b\) have complexity above \(2a + 3b\) when \(a \le 2\) and \(2a + 3b \ge 2\) · Integer complexity of \(2^a 3^b\) for \(a \le 2\) · A criterion for lower bounds on integer complexity · Logarithmic lower bound for integer complexity

DefinitionLower-bound function for integer complexity#✓fully proved

For a natural number \(n\), let \(a\) be the largest natural number with \(3^a \le n\) when \(n \ge 1\), and let \(a = 0\) when \(n = 0\). The function \(g\) on the natural numbers is given by \(g(n) = 3a\) if \(n < \frac{4}{3} \cdot 3^a\), \(g(n) = 3a + 1\) if \(\frac{4}{3} \cdot 3^a \le n < 2 \cdot 3^a\), and \(g(n) = 3a + 2\) if \(n \ge 2 \cdot 3^a\).

def complexityLowerBoundG (n : ℕ) : ℕ :=
  let a := Nat.log 3 n
  if 3 * (n - 3 ^ a) < 3 ^ a then 3 * a
  else if n < 2 * 3 ^ a then 3 * a + 1
  else 3 * a + 2
Used by 1
Used byThe function \(g\) bounds integer complexity from below

TheoremInteger complexity as a minimum over factorizations and sums#●ready to prove

Write \(\lVert m \rVert\) for the integer complexity of a positive integer \(m\), the least number of ones needed to write \(m\) using \(1\), \(+\), \(\times\) and parentheses. For every integer \(n \ge 2\), \(\lVert n \rVert\) is the least element of the set consisting of the numbers \(\lVert d \rVert + \lVert n/d \rVert\) for the divisors \(d \ge 2\) of \(n\) and the numbers \(\lVert j \rVert + \lVert n - j \rVert\) for the integers \(j\) with \(1 \le j \le n/2\).

theorem_wanted complexity_eq_min (n : ℕ) (hn : 2 ≤ n) :
    IsLeast {k | (∃ d : ℕ, 2 ≤ d ∧ d ∣ n ∧
        k = cx d + cx (n / d)) ∨
      (∃ j : ℕ, 1 ≤ j ∧ j ≤ n / 2 ∧ k = cx j + cx (n - j))}
      (cx n)
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Proposition 1.
Uses 1
Statement usesInteger complexity extended to all natural numbers

TheoremA criterion for lower bounds on integer complexity#●ready to prove

Write \(\lVert n \rVert\) for the integer complexity of a positive integer \(n\), the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses. Let \(P\) be a real-valued function on the natural numbers with \(P(1) = 1\) such that \(P(n + m) \le P(n) + P(m)\) and \(P(nm) \le P(n) + P(m)\) for all positive integers \(n\) and \(m\). Then \(P(n) \le \lVert n \rVert\) for every positive integer \(n\).

theorem_wanted le_complexity_of_subadditive (P : ℕ → ℝ)
    (h1 : P 1 = 1)
    (hadd : ∀ n m : ℕ, 1 ≤ n → 1 ≤ m → P (n + m) ≤ P n + P m)
    (hmul : ∀ n m : ℕ, 1 ≤ n → 1 ≤ m → P (n * m) ≤ P n + P m)
    (n : ℕ) (hn : 1 ≤ n) :
    P n ≤ (cx n : ℝ)
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Proposition 2.
Uses 1
Statement usesInteger complexity extended to all natural numbers

TheoremLogarithmic lower bound for integer complexity#●ready to prove

Write \(\lVert n \rVert\) for the integer complexity of a positive integer \(n\), the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses. For every positive integer \(n\), \(\log_2(1 + n) \le \lVert n \rVert\).

theorem_wanted logb_two_add_one_le (n : ℕ) (hn : 1 ≤ n) :
    Real.logb 2 (1 + n) ≤ (cx n : ℝ)
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Corollary 1.
Uses 1
Statement usesInteger complexity extended to all natural numbers

TheoremInteger complexity of \(2^a 3^b\) for \(a \le 2\)#●ready to prove

Write \(\lVert n \rVert\) for the integer complexity of a positive integer \(n\), the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses. For all natural numbers \(a \le 2\) and \(b\), not both zero, \(\lVert 2^a 3^b \rVert = 2a + 3b\).

theorem_wanted complexity_two_pow_mul_three_pow (a b : ℕ)
    (ha : a ≤ 2) (hab : 1 ≤ 2 * a + 3 * b) :
    cx (2 ^ a * 3 ^ b) = 2 * a + 3 * b
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Corollary 2.
Uses 1
Statement usesInteger complexity extended to all natural numbers

TheoremIntegers above \(2^a 3^b\) have complexity above \(2a + 3b\) when \(a \le 2\) and \(2a + 3b \ge 2\)#●ready to prove

Write \(\lVert m \rVert\) for the integer complexity of a positive integer \(m\), the least number of ones needed to write \(m\) using \(1\), \(+\), \(\times\) and parentheses. Let \(a \le 2\) and \(b\) be natural numbers with \(2a + 3b \ge 2\). Then every natural number \(m > 2^a 3^b\) satisfies \(\lVert m \rVert > 2a + 3b\).

theorem_wanted complexity_lt_of_gt_extremal (a b m : ℕ)
    (ha : a ≤ 2) (hab : 2 ≤ 2 * a + 3 * b)
    (hm : 2 ^ a * 3 ^ b < m) :
    2 * a + 3 * b < cx m
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Corollary 2.
Uses 1
Statement usesInteger complexity extended to all natural numbers

TheoremThe function \(g\) bounds integer complexity from below#●ready to prove

Write \(\lVert n \rVert\) for the integer complexity of a positive integer \(n\), the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses. For a positive integer \(n\), let \(a\) be the largest natural number with \(3^a \le n\), and let \(g(n) = 3a\) if \(n < \frac{4}{3} \cdot 3^a\), \(g(n) = 3a + 1\) if \(\frac{4}{3} \cdot 3^a \le n < 2 \cdot 3^a\), and \(g(n) = 3a + 2\) if \(n \ge 2 \cdot 3^a\). Then \(g(n) \le \lVert n \rVert\) for every positive integer \(n\).

theorem_wanted complexityLowerBoundG_le (n : ℕ) (hn : 1 ≤ n) :
    complexityLowerBoundG n ≤ cx n
Sources
  • Juan Arias de Reyna, "Complexity of Natural Numbers", Corollary 2.
Uses 2
Statement usesLower-bound function for integer complexity · Integer complexity extended to all natural numbers

InductiveMahler–Popken expressions#✓fully proved

For a natural number \(m\), the \(m\)-ary Mahler–Popken expressions are the formal expressions built from leaves using the binary operations \(+\) and \(\times\); the tree structure plays the role of brackets. Each leaf carries a label \(i \in \{0, \dots, m - 1\}\) (so there are \(m\) kinds of leaf), and a leaf with label \(i\) stands for the number \(i + 1 \in \{1, \dots, m\}\).

inductive MahlerPopkenExpr (m : ℕ) where
  | leaf : Fin m → MahlerPopkenExpr m
  | add : MahlerPopkenExpr m → MahlerPopkenExpr m → MahlerPopkenExpr m
  | mul : MahlerPopkenExpr m → MahlerPopkenExpr m → MahlerPopkenExpr m
  deriving DecidableEq, Repr
Used by 12
Used byNumber of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Every positive integer has an \(m\)-ary expression · Mahler–Popken complexity · Subadditivity of the \(m\)-ary complexity under addition · Expressions bound the \(m\)-ary complexity from above · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity · The \(m\)-ary complexity is positive · The Mahler–Popken complexity is attained · Integer-complexity expressions as \(1\)-ary Mahler–Popken expressions · \(1\)-ary Mahler–Popken expressions as integer-complexity expressions

DefinitionValue of an \(m\)-ary expression#✓fully proved

The natural number expressed by an \(m\)-ary Mahler–Popken expression: the leaf with index \(i \in \{0, \dots, m-1\}\) has value \(i + 1\), and the value of a sum or of a product of two expressions is the sum or the product of their values.

def eval {m : ℕ} : MahlerPopkenExpr m → ℕ
  | .leaf i => i.val + 1
  | .add a b => a.eval + b.eval
  | .mul a b => a.eval * b.eval
Uses 1 · Used by 8
Statement usesMahler–Popken expressions
Used byEvery positive integer has an \(m\)-ary expression · Mahler–Popken complexity · Subadditivity of the \(m\)-ary complexity under addition · Expressions bound the \(m\)-ary complexity from above · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity · The \(m\)-ary complexity is positive · The Mahler–Popken complexity is attained

DefinitionNumber of leaves of an \(m\)-ary expression#✓fully proved

The number of leaf selections of an \(m\)-ary Mahler–Popken expression, counting repetitions: a leaf counts \(1\), and the count of a sum or of a product of two expressions is the sum of their counts.

def count {m : ℕ} : MahlerPopkenExpr m → ℕ
  | .leaf _ => 1
  | .add a b => a.count + b.count
  | .mul a b => a.count + b.count
Uses 1 · Used by 7
Statement usesMahler–Popken expressions
Used byMahler–Popken complexity · Subadditivity of the \(m\)-ary complexity under addition · Expressions bound the \(m\)-ary complexity from above · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity · The \(m\)-ary complexity is positive · The Mahler–Popken complexity is attained

DefinitionMahler–Popken complexity#✓fully proved

For natural numbers \(m\) and \(n\), the \(m\)-ary Mahler–Popken complexity \(\lVert n \rVert_m\) is the smallest number of leaves (counted with repetition) of an \(m\)-ary Mahler–Popken expression whose value is \(n\): the smallest number of possibly repeated selections from \(\{1, \dots, m\}\) needed to express \(n\) with addition, multiplication and legal bracketing. If no expression has value \(n\) (which happens exactly when \(m = 0\) or \(n = 0\)), the value is \(0\).

noncomputable def mahlerPopkenComplexity (m n : ℕ) : ℕ :=
  sInf {k : ℕ | ∃ e : MahlerPopkenExpr m, e.eval = n ∧ e.count = k}
Uses 3 · Used by 11
Statement usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression
Used byLogarithmic lower bound for the binary Mahler–Popken complexity · Subadditivity of the \(m\)-ary complexity under addition · The \(m\)-ary complexity eventually satisfies its recursion · Expressions bound the \(m\)-ary complexity from above · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity · The \(m\)-ary complexity is positive · The Mahler–Popken complexity is attained · Recursion for the binary Mahler–Popken complexity · Upper bound for the binary Mahler–Popken complexity · Right-hand side of the Mahler–Popken recursion

TheoremEvery positive integer has an \(m\)-ary expression#✓fully proved

For natural numbers \(m \ge 1\) and \(n \ge 1\), there is an \(m\)-ary Mahler–Popken expression whose value is \(n\) (for instance a sum of ones).

theorem exists_mahlerPopkenExpr_eval {m n : ℕ} (hm : 1 ≤ m)
    (hn : 1 ≤ n) : ∃ e : MahlerPopkenExpr m, e.eval = n
Uses 2 · Used by 1
Statement usesMahler–Popken expressions · Value of an \(m\)-ary expression
Used byThe Mahler–Popken complexity is attained

TheoremThe Mahler–Popken complexity is attained#✓fully proved

For all natural numbers \(m \ge 1\) and \(n \ge 1\), there is an \(m\)-ary Mahler–Popken expression whose value is \(n\) and whose number of leaves (counted with repetition) equals the \(m\)-ary Mahler–Popken complexity \(\lVert n \rVert_m\).

theorem mahlerPopkenComplexity_spec {m n : ℕ} (hm : 1 ≤ m)
    (hn : 1 ≤ n) :
    ∃ e : MahlerPopkenExpr m, e.eval = n ∧
      e.count = mahlerPopkenComplexity m n
Uses 5 · Used by 4
Statement usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Mahler–Popken complexity
Proof usesEvery positive integer has an \(m\)-ary expression
Used bySubadditivity of the \(m\)-ary complexity under addition · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity · The \(m\)-ary complexity is positive

TheoremExpressions bound the \(m\)-ary complexity from above#✓fully proved

For natural numbers \(m\) and \(n\) and every \(m\)-ary Mahler–Popken expression \(e\) whose value is \(n\), the \(m\)-ary Mahler–Popken complexity \(\|n\|_m\) is at most the number of leaves of \(e\).

theorem mahlerPopkenComplexity_min_le {m n : ℕ}
    (e : MahlerPopkenExpr m) (he : e.eval = n) :
    mahlerPopkenComplexity m n ≤ e.count
Uses 4 · Used by 3
Statement usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Mahler–Popken complexity
Used bySubadditivity of the \(m\)-ary complexity under addition · Subadditivity of the \(m\)-ary complexity under multiplication · The \(1\)-ary complexity is the integer complexity

TheoremThe \(m\)-ary complexity is positive#✓fully proved

For natural numbers \(m \ge 1\) and \(n \ge 1\), the \(m\)-ary Mahler–Popken complexity \(\|n\|_m\) is positive.

theorem mahlerPopkenComplexity_pos {m n : ℕ} (hm : 1 ≤ m)
    (hn : 1 ≤ n) : 0 < mahlerPopkenComplexity m n
Uses 5
Statement usesMahler–Popken complexity
Proof usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · The Mahler–Popken complexity is attained

TheoremSubadditivity of the \(m\)-ary complexity under addition#✓fully proved

For natural numbers \(m \ge 1\), \(a \ge 1\) and \(b \ge 1\), the \(m\)-ary Mahler–Popken complexity \(\|\cdot\|_m\) satisfies \(\|a + b\|_m \le \|a\|_m + \|b\|_m\).

This is the analogue of subadditivity under addition for the classical integer complexity.

theorem mahlerPopkenComplexity_add_le {m a b : ℕ} (hm : 1 ≤ m)
    (ha : 1 ≤ a) (hb : 1 ≤ b) :
    mahlerPopkenComplexity m (a + b) ≤
      mahlerPopkenComplexity m a + mahlerPopkenComplexity m b
Uses 6
Statement usesMahler–Popken complexity
Proof usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Expressions bound the \(m\)-ary complexity from above · The Mahler–Popken complexity is attained

TheoremSubadditivity of the \(m\)-ary complexity under multiplication#✓fully proved

For natural numbers \(m \ge 1\), \(a \ge 1\) and \(b \ge 1\), the \(m\)-ary Mahler–Popken complexity \(\|\cdot\|_m\) satisfies \(\|a b\|_m \le \|a\|_m + \|b\|_m\).

This is the analogue of subadditivity under multiplication for the classical integer complexity.

theorem mahlerPopkenComplexity_mul_le {m a b : ℕ} (hm : 1 ≤ m)
    (ha : 1 ≤ a) (hb : 1 ≤ b) :
    mahlerPopkenComplexity m (a * b) ≤
      mahlerPopkenComplexity m a + mahlerPopkenComplexity m b
Uses 6
Statement usesMahler–Popken complexity
Proof usesMahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Expressions bound the \(m\)-ary complexity from above · The Mahler–Popken complexity is attained

DefinitionInteger-complexity expressions as \(1\)-ary Mahler–Popken expressions#✓fully proved

The translation of an expression built from one, addition and multiplication into a \(1\)-ary Mahler–Popken expression replaces each occurrence of \(1\) by the leaf standing for \(1\) and keeps every addition and multiplication, so the expression tree is unchanged.

def MahlerPopkenExpr.ofIntegerComplexityExpr :
    IntegerComplexity.Expr → MahlerPopkenExpr 1
  | .one => .leaf 0
  | .add a b => .add (MahlerPopkenExpr.ofIntegerComplexityExpr a)
      (MahlerPopkenExpr.ofIntegerComplexityExpr b)
  | .mul a b => .mul (MahlerPopkenExpr.ofIntegerComplexityExpr a)
      (MahlerPopkenExpr.ofIntegerComplexityExpr b)
Uses 2 · Used by 1
Statement usesExpressions built from one, addition and multiplication · Mahler–Popken expressions
Used byThe \(1\)-ary complexity is the integer complexity

Definition\(1\)-ary Mahler–Popken expressions as integer-complexity expressions#✓fully proved

The translation of a \(1\)-ary Mahler–Popken expression into an expression built from one, addition and multiplication replaces each leaf (the only leaf stands for \(1\)) by \(1\) and keeps every addition and multiplication, so the expression tree is unchanged.

def MahlerPopkenExpr.toIntegerComplexityExpr :
    MahlerPopkenExpr 1 → IntegerComplexity.Expr
  | .leaf _ => .one
  | .add a b => .add a.toIntegerComplexityExpr
      b.toIntegerComplexityExpr
  | .mul a b => .mul a.toIntegerComplexityExpr
      b.toIntegerComplexityExpr
Uses 2 · Used by 1
Statement usesExpressions built from one, addition and multiplication · Mahler–Popken expressions
Used byThe \(1\)-ary complexity is the integer complexity

TheoremThe \(1\)-ary complexity is the integer complexity#✓fully proved

For every natural number \(n \ge 1\), the \(1\)-ary Mahler–Popken complexity \(\|n\|_1\) equals the classical integer complexity of \(n\), the least number of ones needed to write \(n\) using \(1\), \(+\), \(\times\) and parentheses.

This is the case \(m = 1\) of Definition 1 in Campbell's paper (its Example 2).

theorem mahlerPopkenComplexity_one_eq {n : ℕ} (hn : 1 ≤ n) :
    mahlerPopkenComplexity 1 n =
      IntegerComplexity.complexity ⟨n, hn⟩
Uses 15
Statement usesInteger complexity · Mahler–Popken complexity
Proof usesExpressions built from one, addition and multiplication · Number of ones in an expression · Value of an expression · Achievable numbers of ones · Expressions bound the integer complexity from above · Every positive integer is the value of an expression · Mahler–Popken expressions · Number of leaves of an \(m\)-ary expression · Value of an \(m\)-ary expression · Integer-complexity expressions as \(1\)-ary Mahler–Popken expressions · \(1\)-ary Mahler–Popken expressions as integer-complexity expressions · Expressions bound the \(m\)-ary complexity from above · The Mahler–Popken complexity is attained

DefinitionRight-hand side of the Mahler–Popken recursion#✓fully proved

For natural numbers \(m\) and \(n\), write \(\lVert k \rVert_m\) for the \(m\)-ary Mahler–Popken complexity of \(k\). The recursion value of \(n\) is the smallest of the sums \(\lVert d \rVert_m + \lVert n/d \rVert_m\) over the divisors \(d\) of \(n\) with \(d \ne 1\) and \(d \ne n\), and of the sums \(\lVert \eta \rVert_m + \lVert n - \eta \rVert_m\) over \(0 < \eta < n\); it is \(0\) when there are no such sums. This is the right-hand side of the recursion (9) in Campbell's paper.

noncomputable def mahlerPopkenRecursionValue (m n : ℕ) : ℕ :=
  sInf {k : ℕ |
    (∃ d : ℕ, d ∣ n ∧ d ≠ 1 ∧ d ≠ n ∧
      k = mahlerPopkenComplexity m d +
        mahlerPopkenComplexity m (n / d)) ∨
    (∃ η : ℕ, 0 < η ∧ η < n ∧
      k = mahlerPopkenComplexity m η +
        mahlerPopkenComplexity m (n - η))}
Uses 1 · Used by 2
Statement usesMahler–Popken complexity
Used byThe \(m\)-ary complexity eventually satisfies its recursion · Recursion for the binary Mahler–Popken complexity

TheoremThe \(m\)-ary complexity eventually satisfies its recursion#●ready to prove

For every natural number \(m \ge 1\) there is \(N\) such that for every \(n \ge N\), the \(m\)-ary Mahler–Popken complexity \(\|n\|_m\) equals the right-hand side of the recursion (9), that is, the least of the values \(\|d\|_m + \|n/d\|_m\) over divisors \(d\) of \(n\) with \(d \ne 1\) and \(d \ne n\), and the values \(\|\eta\|_m + \|n - \eta\|_m\) over \(0 < \eta < n\).

theorem_wanted mahlerPopkenComplexity_eq_recursionValue_eventually
    (m : ℕ) (hm : 1 ≤ m) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      mahlerPopkenComplexity m n = mahlerPopkenRecursionValue m n
Sources
  • John M. Campbell, "A Binary Version of the Mahler-Popken Complexity Function", Proposition 1.
Uses 2
Statement usesMahler–Popken complexity · Right-hand side of the Mahler–Popken recursion

TheoremRecursion for the binary Mahler–Popken complexity#●ready to prove

For every natural number \(n \ge 3\), the binary (\(2\)-ary) Mahler–Popken complexity \(\lVert n \rVert_2\) equals the minimum of the sums \(\lVert d \rVert_2 + \lVert n/d \rVert_2\) over the divisors \(d\) of \(n\) with \(d \ne 1\) and \(d \ne n\), and of the sums \(\lVert \eta \rVert_2 + \lVert n - \eta \rVert_2\) over \(0 < \eta < n\). This is the recursion (9) for \(m = 2\).

theorem_wanted mahlerPopkenComplexity_two_eq_recursionValue
    (n : ℕ) (hn : 3 ≤ n) :
    mahlerPopkenComplexity 2 n = mahlerPopkenRecursionValue 2 n
Sources
  • John M. Campbell, "A Binary Version of the Mahler-Popken Complexity Function", Proposition 1.
Uses 2
Statement usesMahler–Popken complexity · Right-hand side of the Mahler–Popken recursion

TheoremLogarithmic lower bound for the binary Mahler–Popken complexity#●ready to prove

For every natural number \(n \ge 1\), the \(2\)-ary (binary) Mahler–Popken complexity \(\|n\|_2\) satisfies \(\log_2 n \le \|n\|_2\).

theorem_wanted logb_two_le_mahlerPopkenComplexity_two
    (n : ℕ) (hn : 1 ≤ n) :
    Real.logb 2 (n : ℝ) ≤ (mahlerPopkenComplexity 2 n : ℝ)
Sources
  • John M. Campbell, "A Binary Version of the Mahler-Popken Complexity Function", Theorem 1.
Uses 1
Statement usesMahler–Popken complexity

TheoremUpper bound for the binary Mahler–Popken complexity#●ready to prove

For every natural number \(n \ge 2\), the binary (\(2\)-ary) Mahler–Popken complexity \(\lVert n \rVert_2\) is at most \(\lfloor \log_2 n \rfloor + \nu_2(n) - 1\), where \(\nu_2(n)\) is the number of ones in the base-\(2\) expansion of \(n\).

theorem_wanted mahlerPopkenComplexity_two_le_log_add_digitCount_sub_one
    (n : ℕ) (hn : 2 ≤ n) :
    mahlerPopkenComplexity 2 n ≤
      Nat.log 2 n + (Nat.digits 2 n).count 1 - 1
Sources
  • John M. Campbell, "A Binary Version of the Mahler-Popken Complexity Function", Theorem 2.
Uses 1
Statement usesMahler–Popken complexity

InductiveNumbers built from copies of \(l\)#✓fully proved

For natural numbers \(l\), \(k\) and \(n\), the number \(n\) can be built from \(k\) copies of \(l\) when \(n\) is the value of an expression that uses exactly \(k\) copies of \(l\), combined by addition and multiplication with arbitrary parentheses. Inductively, \(l\) is built from \(1\) copy, and if \(x\) is built from \(a\) copies and \(y\) from \(b\) copies, then \(x + y\) and \(x y\) are built from \(a + b\) copies.

inductive CanBuild (l : ℕ) : ℕ → ℕ → Prop
  | base : CanBuild l 1 l
  | add {a b x y : ℕ} : CanBuild l a x → CanBuild l b y →
      CanBuild l (a + b) (x + y)
  | mul {a b x y : ℕ} : CanBuild l a x → CanBuild l b y →
      CanBuild l (a + b) (x * y)
Used by 6
Used byThe largest number built from \(m\) copies of \(l\) · The \(l\)-complexity of a natural number · The \(l\)-complexity vanishes exactly on numbers that cannot be built · The \(l\)-complexity is at most the size of any build · A buildable number is built from as many copies as its \(l\)-complexity · Every build uses at least one copy

DefinitionThe \(l\)-complexity of a natural number#✓fully proved

For natural numbers \(l\) and \(n\), the \(l\)-complexity \(\|n\|_l\) of \(n\) is the least number \(k\) such that \(n\) can be built from \(k\) copies of \(l\) using addition and multiplication (with arbitrary parentheses), and \(\|n\|_l = 0\) if \(n\) cannot be built from copies of \(l\) at all.

noncomputable def complexityL (l n : ℕ) : ℕ := by
  classical
  exact if h : ∃ k, CanBuild l k n then Nat.find h else 0
Uses 1 · Used by 19
Statement usesNumbers built from copies of \(l\)
Used byAdding a small multiple of \(l\) to a multiple of \(l^2\) · Even \(n\) with \(2^m < n \le 2^{m+1}\) and 2-complexity \(m + 1\) · Even numbers in \((2^m, 2^{m+1})\) with 2-complexity \(m + 2\) · Four forms of even numbers with 2-complexity \(m + 2\) · The \(l\)-complexity vanishes exactly on numbers that cannot be built · The \(l\)-complexity is at most the size of any build · The \(l\)-complexity of \(l^m + l^{m'}\) · A buildable number is built from as many copies as its \(l\)-complexity · An upper bound for the 2-complexity of a sum of distinct powers of two · The 2-complexity of a power of two and of a sum of two powers of two · Bounds for the 2-complexity of \(2^m \cdot 6^r\) when \(8 \le r \le 9\) · The 2-complexity of \(2^m \cdot 6^r\) for \(1 \le r \le 7\) · The 2-complexity of \(2^m \cdot 10^r\) for \(1 \le r \le 4\) · Bounds for the 2-complexity of \(2^m \cdot 10^5\) · Logarithmic bounds for the \(l\)-complexity · A lower bound for the 2-complexity outside sums of two powers of two · Lower bound \(\log_2 n + 2\) for the 2-complexity (Zhang's Corollary 4) · Lower bound for the 2-complexity of even sums of five or more distinct powers of two · Logarithmic bounds for the 2-complexity (Zhang's Lemma 3(3))

TheoremEvery build uses at least one copy#✓fully proved

If \(n\) can be obtained from \(k\) copies of \(l\) using addition and multiplication, then \(k \ge 1\).

theorem CanBuild.one_le {l k n : ℕ} (h : CanBuild l k n) : 1 ≤ k
Uses 1 · Used by 1
Statement usesNumbers built from copies of \(l\)
Used byThe \(l\)-complexity vanishes exactly on numbers that cannot be built

TheoremA buildable number is built from as many copies as its \(l\)-complexity#✓fully proved

For natural numbers \(l\) and \(n\), if \(n\) can be built from some number of copies of \(l\) using addition and multiplication, then \(n\) can be built in this way from \(c\) copies of \(l\), where \(c\) is the \(l\)-complexity of \(n\).

theorem complexityL_spec {l n : ℕ} (h : ∃ k, CanBuild l k n) :
    CanBuild l (complexityL l n) n
Uses 2 · Used by 1
Statement usesNumbers built from copies of \(l\) · The \(l\)-complexity of a natural number
Used byThe \(l\)-complexity vanishes exactly on numbers that cannot be built

TheoremThe \(l\)-complexity is at most the size of any build#✓fully proved

For natural numbers \(l\), \(k\) and \(n\), if \(n\) can be built from \(k\) copies of \(l\) using addition and multiplication, then the \(l\)-complexity of \(n\) is at most \(k\).

theorem complexityL_min_le {l n k : ℕ} (h : CanBuild l k n) :
    complexityL l n ≤ k
Uses 2
Statement usesNumbers built from copies of \(l\) · The \(l\)-complexity of a natural number

TheoremThe \(l\)-complexity vanishes exactly on numbers that cannot be built#✓fully proved

For natural numbers \(l\) and \(n\), the \(l\)-complexity of \(n\) is \(0\) if and only if there is no \(k\) such that \(n\) can be built from \(k\) copies of \(l\) using addition and multiplication.

theorem complexityL_eq_zero_iff {l n : ℕ} :
    complexityL l n = 0 ↔ ¬ ∃ k, CanBuild l k n
Uses 4
Statement usesNumbers built from copies of \(l\) · The \(l\)-complexity of a natural number
Proof usesEvery build uses at least one copy · A buildable number is built from as many copies as its \(l\)-complexity

DefinitionZhang's four exceptional forms#✓fully proved

For natural numbers \(m\) and \(n\), \(n\) has one of the four exceptional forms for \(m\) when one of the following holds: (a) \(n = 2^m + 2^{m_2} + 2^{m_3}\) for some natural numbers \(m > m_2 > m_3 \ge 1\); (b) \(n = 2^m + 2^{m_2} + 2^{m_3} + 2^{m_4}\) for some natural numbers \(m > m_2 > m_3 > m_4 \ge 2\) with \(m + m_4 = m_2 + m_3\); (c) \(n = 2^m + 2^{m-3} + 2^{m_2} + 2^{m_2 - 1}\) for some natural number \(m_2\) with \(m \ge m_2 + 3 \ge 6\); (d) \(m \ge 10\) and \(n = 2^m + 2^{m-5} + 2^{m-6} + 2^{m-7}\).

These are the forms of Corollary 3 and Theorem 1(2) of Zhang's paper, which concern even \(n\) with \(2^m < n \le 2^{m+1}\) and 2-complexity \(m + 2\).

def twoComplexityAddTwoForm (m n : ℕ) : Prop :=
  (∃ m2 m3 : ℕ, m2 < m ∧ m3 < m2 ∧ 1 ≤ m3 ∧
    n = 2 ^ m + 2 ^ m2 + 2 ^ m3) ∨
  (∃ m2 m3 m4 : ℕ, m2 < m ∧ m3 < m2 ∧ m4 < m3 ∧ 2 ≤ m4 ∧
    m + m4 = m2 + m3 ∧
    n = 2 ^ m + 2 ^ m2 + 2 ^ m3 + 2 ^ m4) ∨
  (∃ m2 : ℕ, m2 + 3 ≤ m ∧ 6 ≤ m2 + 3 ∧
    n = 2 ^ m + 2 ^ (m - 3) + 2 ^ m2 + 2 ^ (m2 - 1)) ∨
  (10 ≤ m ∧
    n = 2 ^ m + 2 ^ (m - 5) + 2 ^ (m - 6) + 2 ^ (m - 7))
Used by 3
Used byEven numbers in \((2^m, 2^{m+1})\) with 2-complexity \(m + 2\) · Four forms of even numbers with 2-complexity \(m + 2\) · Lower bound \(\log_2 n + 2\) for the 2-complexity (Zhang's Corollary 4)

TheoremThe largest number built from \(m\) copies of \(l\)#●ready to prove

Let \(l > 1\) and \(m \ge 1\) be natural numbers. Then \(l^m\) can be built from exactly \(m\) copies of \(l\) using addition and multiplication, and every natural number that can be built from \(m\) copies of \(l\) in this way is at most \(l^m\).

theorem_wanted canBuild_max (l m : ℕ) (hl : 1 < l)
    (hm : 1 ≤ m) :
    CanBuild l m (l ^ m) ∧
      ∀ n : ℕ, CanBuild l m n → n ≤ l ^ m
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Lemma 1.
Uses 1
Statement usesNumbers built from copies of \(l\)

TheoremLogarithmic bounds for the \(l\)-complexity#●ready to prove

Write \(\|n\|_l\) for the \(l\)-complexity of \(n\). Let \(l > 1\) be a natural number and let \(n\) be a positive multiple of \(l\). Then \(\log_l n \le \|n\|_l \le l \log_l n - 1\), where \(\log_l\) is the real logarithm to base \(l\).

theorem_wanted logb_le_complexityL_le (l n : ℕ) (hl : 1 < l)
    (hln : l ∣ n) (hn : 1 ≤ n) :
    Real.logb l n ≤ (complexityL l n : ℝ) ∧
      (complexityL l n : ℝ) ≤ l * Real.logb l n - 1
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 1.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremThe \(l\)-complexity of \(l^m + l^{m'}\)#●ready to prove

Write \(\|n\|_l\) for the \(l\)-complexity of \(n\). For natural numbers \(l > 1\) and \(m \ge m' \ge 1\), \(\|l^m + l^{m'}\|_l = m + 1\).

theorem_wanted complexityL_pow_add_pow (l m m' : ℕ)
    (hl : 1 < l) (h : m' ≤ m) (hm' : 1 ≤ m') :
    complexityL l (l ^ m + l ^ m') = m + 1
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Corollary 1.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremThe 2-complexity of a power of two and of a sum of two powers of two#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). For all natural numbers \(m_1\) and \(m_2\) with \(m_1 > m_2 \ge 1\), one has \(\|2^{m_1}\|_2 = m_1\) and \(\|2^{m_1} + 2^{m_2}\|_2 = m_1 + 1\).

theorem_wanted complexityL_two_pow_and_add (m1 m2 : ℕ)
    (h : m2 < m1) (hm2 : 1 ≤ m2) :
    complexityL 2 (2 ^ m1) = m1 ∧
      complexityL 2 (2 ^ m1 + 2 ^ m2) = m1 + 1
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Lemma 3.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremAn upper bound for the 2-complexity of a sum of distinct powers of two#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). Let \(S\) be a nonempty finite set of positive integers with \(k\) elements and largest element \(m_1\). Then \(\|\sum_{e \in S} 2^e\|_2 \le m_1 + k - 1\).

theorem_wanted complexityL_sum_two_pow_le (s : Finset ℕ)
    (hs : ∀ e ∈ s, 1 ≤ e) (hne : s.Nonempty) :
    complexityL 2 (∑ e ∈ s, 2 ^ e) ≤ s.max' hne + s.card - 1
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Lemma 3.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremLogarithmic bounds for the 2-complexity (Zhang's Lemma 3(3))#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\): the least number of copies of \(2\) from which \(n\) can be built using addition and multiplication, and \(0\) if \(n\) cannot be built. For every even natural number \(n \ge 1\), \(\log_2 n \le \|n\|_2 \le 2 \log_2 n - 1\), where \(\log_2\) is the real base-2 logarithm.

theorem_wanted logb_two_bounds (n : ℕ) (h2n : 2 ∣ n)
    (hn : 1 ≤ n) :
    Real.logb 2 n ≤ (complexityL 2 n : ℝ) ∧
      (complexityL 2 n : ℝ) ≤ 2 * Real.logb 2 n - 1
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Lemma 3.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremA lower bound for the 2-complexity outside sums of two powers of two#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). Let \(n\) be a positive even integer that cannot be written as \(2^a + 2^b\) with natural numbers \(a \le b\). Then \(\log_2 n + 1 \le \|n\|_2\).

Since \(n\) is even, the hypothesis says that \(n\) is neither a power of \(2\) nor a sum of two distinct powers of \(2\).

theorem_wanted logb_two_add_one_le (n : ℕ) (h2n : 2 ∣ n)
    (hn : 1 ≤ n)
    (hform : ¬ ∃ a b : ℕ, a ≤ b ∧ n = 2 ^ a + 2 ^ b) :
    Real.logb 2 n + 1 ≤ (complexityL 2 n : ℝ)
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Corollary 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremAdding a small multiple of \(l\) to a multiple of \(l^2\)#●ready to prove

Write \(\|n\|_l\) for the \(l\)-complexity of \(n\). Let \(l > 1\), let \(b \ge 1\) be a multiple of \(l^2\), let \(a\) be a natural number with \(a \le l - 1\), and let \(n = b + a l\). Then \(\|n\|_l = \|b\|_l + a\).

theorem_wanted complexityL_decomp (l n b a : ℕ) (hl : 1 < l)
    (hn : n = b + a * l) (hb : l ^ 2 ∣ b) (hb0 : 1 ≤ b)
    (ha : a ≤ l - 1) :
    complexityL l n = complexityL l b + a
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremEven \(n\) with \(2^m < n \le 2^{m+1}\) and 2-complexity \(m + 1\)#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\). Let \(m \ge 1\) and let \(n\) be an even natural number with \(2^m < n \le 2^{m+1}\). Then \(\|n\|_2 = m + 1\) if and only if \(n = 2^m + 2^t\) for some natural number \(t\) with \(1 \le t \le m\).

The case \(t = m\) gives \(n = 2^{m+1}\).

theorem_wanted complexityL_eq_add_one_iff (m n : ℕ)
    (hm : 1 ≤ m) (h2n : 2 ∣ n) (hn1 : 2 ^ m < n)
    (hn2 : n ≤ 2 ^ (m + 1)) :
    complexityL 2 n = m + 1 ↔
      ∃ t : ℕ, 1 ≤ t ∧ t ≤ m ∧ n = 2 ^ m + 2 ^ t
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 3 and Theorem 1.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremFour forms of even numbers with 2-complexity \(m + 2\)#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\). Let \(m \ge 3\) and let \(n\) be an even natural number with \(2^m < n \le 2^{m+1}\). Suppose that \(n\) has one of the following forms, where all exponents are natural numbers: (a) \(n = 2^m + 2^{m_2} + 2^{m_3}\) with \(m > m_2 > m_3 \ge 1\); (b) \(n = 2^m + 2^{m_2} + 2^{m_3} + 2^{m_4}\) with \(m > m_2 > m_3 > m_4 \ge 2\) and \(m + m_4 = m_2 + m_3\); (c) \(n = 2^m + 2^{m-3} + 2^{m_2} + 2^{m_2-1}\) with \(m \ge m_2 + 3 \ge 6\); (d) \(n = 2^m + 2^{m-5} + 2^{m-6} + 2^{m-7}\) with \(m \ge 10\). Then \(\|n\|_2 = m + 2\).

theorem_wanted complexityL_eq_add_two_of_form (m n : ℕ)
    (hm : 3 ≤ m) (h2n : 2 ∣ n) (hn1 : 2 ^ m < n)
    (hn2 : n ≤ 2 ^ (m + 1))
    (hform : twoComplexityAddTwoForm m n) :
    complexityL 2 n = m + 2
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Corollary 3.
Uses 2
Statement usesThe \(l\)-complexity of a natural number · Zhang's four exceptional forms

TheoremEven numbers in \((2^m, 2^{m+1})\) with 2-complexity \(m + 2\)#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\). Let \(m \ge 3\) and let \(n\) be an even natural number with \(2^m < n \le 2^{m+1}\). Then \(\|n\|_2 = m + 2\) if and only if \(n\) has one of the following forms, where all exponents are natural numbers: (a) \(n = 2^m + 2^{m_2} + 2^{m_3}\) with \(m > m_2 > m_3 \ge 1\); (b) \(n = 2^m + 2^{m_2} + 2^{m_3} + 2^{m_4}\) with \(m > m_2 > m_3 > m_4 \ge 2\) and \(m + m_4 = m_2 + m_3\); (c) \(n = 2^m + 2^{m-3} + 2^{m_2} + 2^{m_2-1}\) with \(m \ge m_2 + 3 \ge 6\); (d) \(n = 2^m + 2^{m-5} + 2^{m-6} + 2^{m-7}\) with \(m \ge 10\).

theorem_wanted complexityL_eq_add_two_iff (m n : ℕ)
    (hm : 3 ≤ m) (h2n : 2 ∣ n) (hn1 : 2 ^ m < n)
    (hn2 : n ≤ 2 ^ (m + 1)) :
    complexityL 2 n = m + 2 ↔ twoComplexityAddTwoForm m n
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 4 and Theorem 1.
Uses 2
Statement usesThe \(l\)-complexity of a natural number · Zhang's four exceptional forms

TheoremLower bound \(\log_2 n + 2\) for the 2-complexity (Zhang's Corollary 4)#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\): the least number of copies of \(2\) from which \(n\) can be built using addition and multiplication, and \(0\) if \(n\) cannot be built. Let \(m\) and \(n\) be natural numbers with \(n\) even, \(n \ge 1\) and \(2^m < n \le 2^{m+1}\). Suppose that \(n \ne 2^a + 2^b\) for all natural numbers \(a \le b\), and that \(n\) has none of Zhang's four exceptional forms for \(m\). Then \(\log_2 n + 2 \le \|n\|_2\), where \(\log_2\) is the real base-2 logarithm.

theorem_wanted logb_two_add_two_le (m n : ℕ) (h2n : 2 ∣ n)
    (hn : 1 ≤ n) (hn1 : 2 ^ m < n) (hn2 : n ≤ 2 ^ (m + 1))
    (hpow : ¬ ∃ a b : ℕ, a ≤ b ∧ n = 2 ^ a + 2 ^ b)
    (hform : ¬ twoComplexityAddTwoForm m n) :
    Real.logb 2 n + 2 ≤ (complexityL 2 n : ℝ)
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Corollary 4.
Uses 2
Statement usesThe \(l\)-complexity of a natural number · Zhang's four exceptional forms

TheoremLower bound for the 2-complexity of even sums of five or more distinct powers of two#●ready to prove

Write \(\|n\|_2\) for the 2-complexity of \(n\). Let \(n \ge 1\) be an even natural number and let \(S\) be a finite set of natural numbers with at least five elements such that \(n = \sum_{e \in S} 2^e\). Then \(\log_2 n + 2 \le \|n\|_2\), where \(\log_2\) is the real base-2 logarithm.

This is a particular case of Corollary 4 of the source.

theorem_wanted logb_two_add_two_le_of_five_powers (n : ℕ)
    (s : Finset ℕ) (h2n : 2 ∣ n) (hn : 1 ≤ n)
    (hs : n = ∑ e ∈ s, 2 ^ e) (hcard : 5 ≤ s.card) :
    Real.logb 2 n + 2 ≤ (complexityL 2 n : ℝ)
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Corollary 4.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremThe 2-complexity of \(2^m \cdot 6^r\) for \(1 \le r \le 7\)#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). For all natural numbers \(m\) and \(r\) with \(1 \le r \le 7\), one has \(\|2^m \cdot 6^r\|_2 = m + 3r\).

theorem_wanted complexityL_two_pow_mul_six_pow_eq (m r : ℕ)
    (hr1 : 1 ≤ r) (hr2 : r ≤ 7) :
    complexityL 2 (2 ^ m * 6 ^ r) = m + 3 * r
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 5 and Theorem 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremBounds for the 2-complexity of \(2^m \cdot 6^r\) when \(8 \le r \le 9\)#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). For all natural numbers \(m\) and \(r\) with \(8 \le r \le 9\), one has \(m + 3r - 1 \le \|2^m \cdot 6^r\|_2 \le m + 3r\).

theorem_wanted complexityL_two_pow_mul_six_pow_bounds
    (m r : ℕ) (hr1 : 8 ≤ r) (hr2 : r ≤ 9) :
    m + 3 * r - 1 ≤ complexityL 2 (2 ^ m * 6 ^ r) ∧
      complexityL 2 (2 ^ m * 6 ^ r) ≤ m + 3 * r
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 5 and Theorem 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremThe 2-complexity of \(2^m \cdot 10^r\) for \(1 \le r \le 4\)#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). For all natural numbers \(m\) and \(r\) with \(1 \le r \le 4\), one has \(\|2^m \cdot 10^r\|_2 = m + 4r\).

theorem_wanted complexityL_two_pow_mul_ten_pow_eq (m r : ℕ)
    (hr1 : 1 ≤ r) (hr2 : r ≤ 4) :
    complexityL 2 (2 ^ m * 10 ^ r) = m + 4 * r
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 6 and Theorem 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number

TheoremBounds for the 2-complexity of \(2^m \cdot 10^5\)#●ready to prove

Write \(\|n\|_2\) for the \(2\)-complexity of \(n\). For every natural number \(m\), one has \(m + 19 \le \|2^m \cdot 10^5\|_2 \le m + 20\).

theorem_wanted complexityL_two_pow_mul_ten_pow_five_bounds
    (m : ℕ) :
    m + 19 ≤ complexityL 2 (2 ^ m * 10 ^ 5) ∧
      complexityL 2 (2 ^ m * 10 ^ 5) ≤ m + 20
Sources
  • Pengcheng Zhang, "The 2-Complexity of Even Positive Integers", Proposition 6 and Theorem 2.
Uses 1
Statement usesThe \(l\)-complexity of a natural number
32 fully proved27 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.