The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$

The factorial. By the recursion theorem (The recursion theorem) applied to the set $\mathbb{N}\times\mathbb{N}$, the starting element $(0,1)$ and the function $f(k, v) = (\sigma(k),\, v \cdot \sigma(k))$, and by the same induction on the first coordinate as in Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$, there is a unique $F : \mathbb{N} \to \mathbb{N}$ with

$F(0) = 1, \qquad F(\sigma(n)) = F(n)\cdot\sigma(n) \quad (n \in \mathbb{N}).$

We write $n! := F(n)$. Thus $0! = 1$, $1! = 0!\cdot 1 = 1$, $2! = 1!\cdot 2 = 2$, $3! = 6$, $4! = 24$, $5! = 120$, $6! = 720$.

$0! = 1$ is the base clause of this recursion, not a convention imported from elsewhere. Nothing about empty products is presupposed; the agreement with the empty product is proved below, in clause (a), rather than assumed.

Truncated difference. Throughout, $n - k$ is the operation fixed in Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$: the unique $j$ with $k + j = n$ when $k \le n$, and $0$ when $n < k$.

The falling factorial. For $n \in \mathbb{N}$ define $n^{\underline{k}}$ by recursion on $k$, by the recursion theorem applied to $\mathbb{N}\times\mathbb{N}$ with starting element $(0,1)$ and $f(k, v) = (\sigma(k),\, v \cdot (n-k))$:

$n^{\underline{0}} = 1, \qquad n^{\underline{\sigma(k)}} = n^{\underline{k}}\cdot(n-k) .$

So $n^{\underline{1}} = 1\cdot(n-0) = n$ and $n^{\underline{2}} = n\,(n-1)$, and for $k \le n$ the value is the product $n(n-1)\cdots(n-k+1)$ of the $k$ topmost factors.

Four facts, proved here because the page uses each of them.

(a) The factorial is the product of the first $n$ positive naturals. $n! = \prod_{j<n}\sigma(j) = \prod_{j<n}(j+1)$, the $\mathbb{N}$-valued product of Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$. Induction (The principle of mathematical induction): at $n = 0$ both sides are $1$, the empty product and the base clause agreeing; and $\prod_{j<\sigma(n)}\sigma(j) = \big(\prod_{j<n}\sigma(j)\big)\cdot\sigma(n) = n!\cdot\sigma(n) = \sigma(n)!$. So the empty-product reading and the base-clause reading are the same reading, and neither was assumed.

(b) $n! \ne 0$, and $\iota(n!) = \prod^{\mathbb{R}}_{j<n}\iota(j+1)$. For the first, $0! = 1 \ne 0$ (The von Neumann naturals form a Peano system) and $\sigma(n)! = n!\cdot\sigma(n)$ is a product of two nonzero naturals, which is nonzero: if $xy = 0$ with $y \ne 0$ then $xy = 0\cdot y$ (Zero and one under multiplication) and cancellation gives $x = 0$ (Cancellation for multiplication by a nonzero factor). So $n! \ne 0$ for every $n$ by induction. For the second, apply the bridge clause 6 of that lemma to clause (a) above. This is what makes the factorial of this page and the real-valued product $\prod_{j<n}(j+1)$ used elsewhere in the library one object seen twice, rather than two unrelated notions.

(c) $n^{\underline{k}}\cdot(n-k)! = n!$ for $k \le n$. Induction on $k$, for all $n$ at once. At $k = 0$ this reads $1 \cdot n! = n!$. Assume it at $k$ and let $\sigma(k) \le n$; then $k \le n$, and writing $d := n - k$ we have $k + d = n$ and $d \ne 0$, since $k + 0 = k \ne n$; so $d = \sigma(e)$ for a unique $e$ (Every nonzero natural number is a successor), and $\sigma(k) + e = n$, that is $e = n - \sigma(k)$ (Addition is cancellative). Therefore $n^{\underline{\sigma(k)}}\cdot\big(n-\sigma(k)\big)! = n^{\underline{k}}\cdot(n-k)\cdot e! = n^{\underline{k}}\cdot\big(e!\cdot\sigma(e)\big) = n^{\underline{k}}\cdot\sigma(e)! = n^{\underline{k}}\cdot(n-k)! = n!$, using commutativity and associativity of multiplication (Multiplication is associative, Multiplication is commutative) and the recursion clause for the factorial.

(d) Boundary values. $n^{\underline{0}} = 1$ for every $n$, by the base clause; $n^{\underline{n}} = n!$, since clause (c) at $k = n$ gives $n^{\underline{n}}\cdot 0! = n!$ and $0! = 1$; and $n^{\underline{k}} = 0$ whenever $k > n$. For the last, $n - n = 0$ gives $n^{\underline{\sigma(n)}} = n^{\underline{n}}\cdot 0 = 0$, the clause $x \cdot 0 = 0$ being definitional (Multiplication of natural numbers), and if $n^{\underline{k}} = 0$ then $n^{\underline{\sigma(k)}} = 0$ as well, so $n^{\underline{k}} = 0$ for every $k \ge \sigma(n)$ by induction.

• Why $0! = 1$ is not imported. The empty-product convention of an arbitrary monoid is fixed in The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity ↗, which comes later in the reading order, so citing it here would be a dependency pointing the wrong way. Taking $0! = 1$ as the base clause of the factorial's own recursion costs nothing and owes nothing, and clause (a) then records the agreement.

• The library's other factorial. For every real $x$, $x^k/k! \to 0$ ↗, later in the reading order, works with a real-valued factorial defined as the product $\prod_{j<n}(j+1)$ in $\mathbb{R}$. Clause (b) says that this is exactly $\iota(n!)$, so the two agree and no second notion has been created. That pointer is orientation only.

• Check every clause at $k = 0$ and at $k = n$. The falling factorial is defined by two regimes, one for $k \le n$ and one beyond, and the recursion above covers both because the truncated difference is $0$ past the end. The two values that get used constantly are $n^{\underline{0}} = 1$ and $n^{\underline{n}} = n!$, and both are clause (d).