Taxicab numbers

Content created by Egbert Rijke.

Created on 2023-12-06.
Last modified on 2023-12-06.

module elementary-number-theory.taxicab-numbers where
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.cubes-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.nonzero-natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types


The n-th taxicab number taxicab n is the smallest natural number x such that x is a sum of two cubes in n distinct ways.

Note: The definition of taxicab numbers only considers sums of positive integers. Note that if n is a cube, i.e., if n = c³, then the only solutions to the equation

  a³ + b³ = c³

have either a = 0 or b = 0 by Fermat's last theorem. Therefore n can be written in at least two different ways as a sum of cubes of positive natural numbers if and only if it can be written in at least two different ways as a sum of cubes of arbitary natural numbers. However, the class of natural numbers that can be written in exactly one way as a sum of cubes is different when we consider sums of cubes of positive natural numbers or sums of cubes of arbitrary natural numbers.


The type of decompositions of a natural number as a sum of cubes

sum-of-cubes-decomposition-ℕ :   UU lzero
sum-of-cubes-decomposition-ℕ x =
  Σ ( nonzero-ℕ)
    ( λ y 
      Σ ( nonzero-ℕ)
        ( λ z 
          ( leq-ℕ (nat-nonzero-ℕ y) (nat-nonzero-ℕ z)) ×
          ( cube-ℕ (nat-nonzero-ℕ y) +ℕ cube-ℕ (nat-nonzero-ℕ z)  x)))

The predicate of being a sum of two cubes in exactly n distinct ways

A number x is a sum of cubes in n distinct ways if there is an equivalence

  Fin n ≃ sum-of-cubes-decomposition-ℕ x

from the standard finite type to the type sum-of-cubes-decomposition-ℕ x of ways of writing x as a sum of cubes.

is-sum-of-cubes-in-number-of-distinct-ways-ℕ :     UU lzero
is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x =
  Fin n  sum-of-cubes-decomposition-ℕ x

The predicate of being the n-th taxicab number

is-taxicab-number-ℕ :     UU lzero
is-taxicab-number-ℕ n x =
  is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x ×
  ((y : )  is-sum-of-cubes-in-number-of-distinct-ways-ℕ n y  leq-ℕ x y)

See also

Recent changes