The Hardy-Ramanujan number (#970)

~~We have exactly 1729 agda files in master right now.~~

For a brief moment in time, the library had exactly 1729 Agda files. In
celebration of this beautiful fact, I formalized taxicab numbers and the
two distinct decompositions of the Hardy-Ramanujan number into sums of
cubes of two positive natural numbers.

src/elementary-number-theory.lagda.md

@@ -27,6 +27,7 @@ open import elementary-number-theory.collatz-conjecture public
 open import elementary-number-theory.commutative-semiring-of-natural-numbers public
 open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
+open import elementary-number-theory.cubes-natural-numbers public
 open import elementary-number-theory.decidable-dependent-function-types public
 open import elementary-number-theory.decidable-total-order-natural-numbers public
 open import elementary-number-theory.decidable-total-order-standard-finite-types public
@@ -55,6 +56,7 @@ open import elementary-number-theory.greatest-common-divisor-integers public
 open import elementary-number-theory.greatest-common-divisor-natural-numbers public
 open import elementary-number-theory.group-of-integers public
 open import elementary-number-theory.half-integers public
+open import elementary-number-theory.hardy-ramanujan-number public
 open import elementary-number-theory.inequality-integer-fractions public
 open import elementary-number-theory.inequality-integers public
 open import elementary-number-theory.inequality-natural-numbers public
@@ -120,6 +122,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public
+open import elementary-number-theory.taxicab-numbers public
 open import elementary-number-theory.telephone-numbers public
 open import elementary-number-theory.triangular-numbers public
 open import elementary-number-theory.twin-prime-conjecture public

src/elementary-number-theory/cubes-natural-numbers.lagda.md

@@ -0,0 +1,58 @@
+# Cubes of natural numbers
+
+```agda
+module elementary-number-theory.cubes-natural-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.multiplication-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.squares-natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.fibers-of-maps
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The {{#concept "cube" Disambiguation="natural number"}} `n³` of a
+[natural number](elementary-number-theory.natural-numbers.md) `n` is the triple
+[product](elementary-number-theory.multiplication-natural-numbers.md)
+
+```text
+  n³ := n * n * n
+```
+
+of `n` with itself.
+
+## Definitions
+
+### Cubes of natural numbers
+
+```agda
+cube-ℕ : ℕ → ℕ
+cube-ℕ n = square-ℕ n *ℕ n
+```
+
+### The predicate of being a cube of natural numbers
+
+```agda
+is-cube-ℕ : ℕ → UU lzero
+is-cube-ℕ = fiber cube-ℕ
+```
+
+### The cubic root of cubic natural numbers
+
+```agda
+cubic-root-ℕ : (n : ℕ) → is-cube-ℕ n → ℕ
+cubic-root-ℕ n = pr1
+```
+
+## See also
+
+- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md)

src/elementary-number-theory/hardy-ramanujan-number.lagda.md

@@ -0,0 +1,73 @@
+# The Hardy-Ramanujan number
+
+```agda
+module elementary-number-theory.hardy-ramanujan-number where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.taxicab-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.unit-type
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176}}
+is the number `1729`. This number is the second
+[taxicab number](elementary-number-theory.taxicab-numbers.md), i.e., it is the
+least natural number that can be written as a sum of cubes of positive natural
+numbers in exactly two distinct ways. Specifically, we have the identifications
+
+```text
+  1³ + 12³ ＝ 1729    and    9³ + 10³ ＝ 1729.
+```
+
+## Definition
+
+### The Hardy-Ramanujan number
+
+```agda
+Hardy-Ramanujan-ℕ : ℕ
+Hardy-Ramanujan-ℕ = 1729
+```
+
+## Properties
+
+### Two decompositions of the Hardy-Ramanujan number into sums of cubes of two positive natural numbers
+
+```agda
+first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
+  sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
+pr1 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
+  (1 , is-nonzero-one-ℕ)
+pr1 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
+  (12 , is-nonzero-succ-ℕ 11)
+pr1 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
+  star
+pr2 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
+  refl
+
+second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
+  sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
+pr1 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
+  (9 , is-nonzero-succ-ℕ 8)
+pr1 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
+  (10 , is-nonzero-succ-ℕ 9)
+pr1 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
+  star
+pr2 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
+  refl
+```
+
+## External links
+
+- [1729 (number)](<https://en.wikipedia.org/wiki/1729_(number)>) at Wikipedia

src/elementary-number-theory/multiplication-natural-numbers.lagda.md

@@ -23,6 +23,19 @@ open import foundation.negated-equality
 
 </details>
 
+## Idea
+
+The {{#concept "multiplication" Disambiguation="natural numbers"}} operation on
+the [natural numbers](elementary-number-theory.natural-numbers.md) is defined by
+[iteratively](foundation.iterating-functions.md) applying
+[addition](elementary-number-theory.addition-natural-numbers.md) of a number to
+itself. More preciesly the number `m * n` is defined by adding the number `n` to
+itself `m` times:
+
+```text
+  m * n = n + ⋯ + n    (n added to itself m times).
+```
+
 ## Definition
 
 ### Multiplication
@@ -239,3 +252,8 @@ neq-mul-ℕ m n p =
       ( ( right-successor-law-mul-ℕ (succ-ℕ m) (succ-ℕ n)) ∙
         ( ap ((succ-ℕ m) +ℕ_) (left-successor-law-mul-ℕ m (succ-ℕ n)))))
 ```
+
+## See also
+
+- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md)
+- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md)

src/elementary-number-theory/squares-natural-numbers.lagda.md

@@ -28,18 +28,37 @@ open import foundation-core.transport-along-identifications
 
 </details>
 
+## Idea
+
+The {{#concept "square" Disambiguation="natural number"}} `n²` of a
+[natural number](elementary-number-theory.natural-numbers.md) `n` is the
+[product](elementary-number-theory.multiplication-natural-numbers.md)
+
+```text
+  n² := n * n
+```
+
+of `n` with itself.
+
 ## Definition
 
+### Squares of natural numbers
+
 ```agda
 square-ℕ : ℕ → ℕ
 square-ℕ n = mul-ℕ n n
+```
 
-cube-ℕ : ℕ → ℕ
-cube-ℕ n = (square-ℕ n) *ℕ n
+### The predicate of being a square of a natural number
 
+```agda
 is-square-ℕ : ℕ → UU lzero
 is-square-ℕ n = Σ ℕ (λ x → n ＝ square-ℕ x)
+```
+
+### The square root of a square natural number
 
+```agda
 square-root-ℕ : (n : ℕ) → is-square-ℕ n → ℕ
 square-root-ℕ _ (root , _) = root
 ```
@@ -153,3 +172,7 @@ is-decidable-is-square-ℕ n =
     ( λ x → has-decidable-equality-ℕ n (square-ℕ x))
     ( is-decidable-big-root n)
 ```
+
+## See also
+
+- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md)

src/elementary-number-theory/taxicab-numbers.lagda.md

@@ -0,0 +1,104 @@
+# Taxicab numbers
+
+```agda
+module elementary-number-theory.taxicab-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The `n`-th
+{{#concept "taxicab number" Agda=is-taxicab-number-ℕ WD="taxicab number" WDID=Q1462591}}
+`taxicab n` is the smallest
+[natural number](elementary-number-theory.natural-numbers.md) `x` such that `x`
+is a [sum](elementary-number-theory.addition-natural-numbers.md) of two
+[cubes](elementary-number-theory.cubes-natural-numbers.md) in `n`
+[distinct](foundation.negated-equality.md) ways.
+
+**Note:** The definition of taxicab numbers only considers sums of
+[positive integers](elementary-number-theory.nonzero-natural-numbers.md). Note
+that if `n` is a cube, i.e., if `n ＝ c³`, then the only solutions to the
+equation
+
+```text
+  a³ + b³ = c³
+```
+
+have either `a ＝ 0` or `b ＝ 0` by
+[Fermat's last theorem](https://en.wikipedia.org/wiki/Fermat%27s_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.
+
+## Definitions
+
+### The type of decompositions of a natural number as a sum of cubes
+
+```agda
+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
+
+```text
+  Fin n ≃ sum-of-cubes-decomposition-ℕ x
+```
+
+from the
+[standard finite type](univalent-combinatorics.standard-finite-types.md) to the
+type `sum-of-cubes-decomposition-ℕ x` of ways of writing `x` as a sum of cubes.
+
+```agda
+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
+
+```agda
+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
+
+- [The Hardy-Ramanujan number](elementary-number-theory.hardy-ramanujan-number.md)
+
+## External links
+
+- [Taxicab numbers](https://en.wikipedia.org/wiki/Taxicab_number) at Wikipedia
+- [Taxicab nubmers](https://oeis.org/A011541) at the OEIS.