# Factorial: uniqueness of the recursive definition, the product form and computing 5!

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-factorial/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-factorial-01 · production-20261019-adopted-96



## Goal and scope

Using only F(0)=1 and F(n+1)=(n+1)F(n) (n∈ℕ, with 0∈ℕ): (1) prove that at most one function ℕ→ℕ satisfies these two equations; (2) prove F(n)=∏_{k=1}^{n} k for every n (the empty product being 1), so that for n>0, n! is the product of all integers from 1 to n; (3) prove F(n)≥1 for every n, in particular 0!=1≠0; (4) compute 5!=120 step by step from the recursion.

Inside the MKO's scope: natural numbers including 0 (assumption a1) and the recursively defined function F. Existence of F is taken from the MKO statement (the recursion theorem is not proved here); this guide proves uniqueness, the product form and positivity. It does not prove that n! counts the permutations of an n-element set (the MKO says that is a separate theorem), and it does not change the canonical MKO or its English edition.





## Givens and symbols


- nat_induction
- function_def
- eq_replace
- mul_comm
- order_basics
- numeric_evaluation


- G1 — ℕ includes 0, and n is a natural number (MKO assumption a1).
- G2 — F:ℕ→ℕ satisfies F(0)=1 and F(n+1)=(n+1)F(n) for every n∈ℕ; write n!=F(n). That such an F exists is taken from the MKO statement.


- F,\ n! — the factorial function and its notation n!=F(n)
- G — any function satisfying the same two equations
- \mathbb{N} — the natural numbers, including 0
- \prod_{k=1}^{n} k — the product of the integers from 1 to n, equal to 1 when n=0
- P(n) — the product ∏_{k=1}^{n} k as a function of n





## Rules and sources


- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_factorial_def · cited — The function F:ℕ→ℕ is uniquely determined recursively by F(0)=1 and F(n+1)=(n+1)F(n). Its customary notation is n!. · mko-factorial
- prod_def · prerequisite — Finite products: ∏_{k=1}^{0} a_k=1 (the empty product) and ∏_{k=1}^{n+1} a_k=(∏_{k=1}^{n} a_k)·a_{n+1}.
- nat_closure · prerequisite — Sums and products of natural numbers are natural numbers; for every n∈ℕ, n+1≥1>0.
- L_pos · lemma — For every n∈ℕ, F(n)≥1.





## Main derivation

S01 · definitionBefore

n!

After

F(0)=1,\ \ F(n+1)=(n+1)F(n)\ \ (n\in\mathbb{N})

Conditions: 0\in\mathbb{N}

Rule: mko_factorial_def · Uses: G1, G2, mko_factorial_def

Leaf basis: mko_factorial_def + def_unfold

By the MKO, n! means F(n), and F is fixed by two equations only: the start F(0)=1, and 'next value = the new factor n+1 times the previous value'. From here on the guide uses only these two equations and no formula remembered in advance.



S02 · definitionBefore

G:\mathbb{N}\to\mathbb{N},\ G(0)=1,\ G(n+1)=(n+1)G(n)

After

Q(n):\ G(n)=F(n)

Conditions: none

Rule: def_intro · Uses: S01

Leaf basis: def_intro

To prove uniqueness, take an arbitrary function G:ℕ→ℕ assumed only to satisfy the same two equations. For each n, name the statement 'G(n)=F(n)' as Q(n); the aim is Q(n) for every n.



S03 · induction_baseBefore

G(0),\ F(0)

After

G(0)=1=F(0)

Conditions: none

Rule: eq_refl_symm_trans · Uses: S01, S02

Leaf basis: eq_refl_symm_trans

Base case: G(0)=1 by the assumption on G and F(0)=1 by definition, so symmetry and transitivity of equality give G(0)=F(0), that is Q(0).



S04 · induction_stepBefore

G(n)=F(n)

After

G(n+1)=F(n+1)

Conditions: n\in\mathbb{N}\ \text{arbitrary}

Rule: eq_replace · Uses: S01, S02

Leaf basis: eq_replace + eq_refl_symm_trans + forall_elim

Suppose G(n)=F(n) for some n. Then G(n+1)=(n+1)G(n) by the recursion for G, =(n+1)F(n) by replacing equals using the induction hypothesis, =F(n+1) by the recursion for F. So Q(n)⇒Q(n+1).



S05 · impliesBefore

Q(0),\ \ Q(n)\Rightarrow Q(n+1)

After

G=F\ \text{for every such}\ G

Conditions: n_0=0

Rule: nat_induction · Uses: S03, S04, nat_induction, function_def

Leaf basis: nat_induction + function_def + forall_intro

By induction from n₀=0, G(n)=F(n) for every n∈ℕ. G and F both have domain ℕ and codomain ℕ and agree at every point, so G=F by function_def. Since G was arbitrary, generalization shows that at most one function satisfies the two equations. This is the content of 'uniquely' in the MKO.



S06 · definitionBefore

P(n)=\prod_{k=1}^{n} k

After

P:\mathbb{N}\to\mathbb{N}

Conditions: none

Rule: prod_def · Uses: prod_def, nat_closure

Leaf basis: prod_def + nat_closure + nat_induction

With a_k=k, let P(n)=∏_{k=1}^{n} k. Each P(n) is a natural number: P(0)=1∈ℕ, and if P(n)∈ℕ then P(n+1)=P(n)·(n+1)∈ℕ by nat_closure, so by induction this holds for every n. Hence P is a function ℕ→ℕ.



S07 · equivalentBefore

P(0)=\prod_{k=1}^{0} k

After

P(0)=1

Conditions: none

Rule: prod_def · Uses: S06

Leaf basis: prod_def + def_unfold

A product with no factors is 1 (the empty product), the first clause of prod_def; so P starts with the same value as F(0)=1.



S08 · equivalentBefore

P(n+1)=P(n)\cdot(n+1)

After

P(n+1)=(n+1)P(n)

Conditions: none

Rule: mul_comm · Uses: S06

Leaf basis: prod_def + mul_comm

The second clause of prod_def gives P(n+1)=P(n)·(n+1); commutativity of multiplication rewrites this as (n+1)P(n), exactly the form of the recursion for F.



S09 · theorem_applicationBefore

P(0)=1,\ \ P(n+1)=(n+1)P(n)

After

F(n)=\prod_{k=1}^{n} k\ \text{for every}\ n\in\mathbb{N}

Conditions: P:\mathbb{N}\to\mathbb{N}

Rule: forall_elim · Uses: S05, S06, S07, S08

Leaf basis: forall_elim + function_def + def_unfold

P is a function ℕ→ℕ (S06) satisfying both equations of F (S07, S08). S05 holds for every such function, so taking G=P gives P=F, that is n!=∏_{k=1}^{n} k. For n>0 this is the product of all integers from 1 to n, for example 5!=1·2·3·4·5.



S10 · theorem_applicationBefore

F(n)

After

F(n)\geq 1\ \text{for every}\ n\in\mathbb{N};\ \text{in particular}\ 0!=1\neq 0

Conditions: none

Rule: L_pos · Uses: S01, L_pos

Leaf basis: nat_induction + order_basics

By Lemma L_pos every factorial is at least 1, so no n! equals 0; in particular 0!=1. The lemma is proved by induction in sub-steps S10.1 and S10.2.



S11 · impliesBefore

F(0)=1

After

F(1)=1,\ F(2)=2,\ F(3)=6

Conditions: none

Rule: forall_elim · Uses: S01

Leaf basis: forall_elim + eq_replace + numeric_evaluation

Substitute into the recursion one step at a time: n=0 gives F(1)=1·F(0)=1; n=1 gives F(2)=2·F(1)=2; n=2 gives F(3)=3·F(2)=6. Each step multiplies by the new factor n+1, not by n.



S12 · impliesBefore

F(3)=6

After

F(4)=24,\ F(5)=120

Conditions: none

Rule: forall_elim · Uses: S01, S11

Leaf basis: forall_elim + eq_replace + numeric_evaluation

Continue: n=3 gives F(4)=4·F(3)=4·6=24, and n=4 gives F(5)=5·F(4)=5·24=120. So 5!=120.



S13 · impliesBefore

\prod_{k=1}^{5} k

After

1\cdot 2\cdot 3\cdot 4\cdot 5=120=F(5)

Conditions: none

Rule: prod_def · Uses: S09, S12

Leaf basis: prod_def + numeric_evaluation

Cross-check: unfolding prod_def gives ∏_{k=1}^{5} k=1·2·3·4·5=120, which agrees with F(5)=120 from the recursion in S12, as S09 predicts.



S14 · impliesBefore

S05,\ S09,\ S10,\ S12

After

\text{goals (1) to (4) established}

Conditions: none

Rule: and_intro_elim · Uses: S05, S09, S10, S12

Leaf basis: and_intro_elim

The four goals are established by S05 (uniqueness), S09 (product form), S10 (F(n)≥1 and 0!=1) and S12 (5!=120).







## Substeps and lemmas

S10.1 · induction_baseBefore

F(0)=1

After

F(0)\geq 1

Conditions: none

Rule: order_basics · Uses: S01

Leaf basis: order_basics + def_unfold

F(0)=1 and 1≥1 (the equality case), so the base case holds.



S10.2 · induction_stepBefore

F(n)\geq 1

After

F(n+1)=(n+1)F(n)\geq 1

Conditions: n+1>0

Rule: order_basics · Uses: S01, nat_closure, order_basics

Leaf basis: order_basics + nat_closure + mul_one

Suppose F(n)≥1. Since n+1>0, multiplying both sides by n+1 keeps the direction: (n+1)F(n)≥(n+1)·1=n+1; and n+1≥1, so by transitivity F(n+1)=(n+1)F(n)≥1. By induction, S10.1 and S10.2 prove Lemma L_pos.







## Reverse audits


- S14 · sufficient_goal_reduction · S05, S09, S10, S12, and_intro_elim — Goal G: (1) to (4) together. Sufficient condition H: S05, S09, S10 and S12 each hold; H⇒G by conjunction introduction. H is proved forwards from the definition and induction; G is never used as a premise.
- S13 · premise_audit · S09, S12, prod_def — This is a consistency check at n=5 only; the general statement of S09 comes from uniqueness, not from this example.
- S12 · premise_audit · S11, forall_elim, numeric_evaluation — Exact integer multiplication (N4, N5), with no floating-point approximation.
- S11 · premise_audit · S01, forall_elim, numeric_evaluation — Each value depends on the previous one and must be computed in order; the products can be recomputed independently (N1 to N3).
- S10.2 · premise_audit · nat_closure, order_basics, nat_induction — Multiplying by n+1 keeps the inequality only because n+1>0; multiplying by a factor that can be 0 (such as the wrong recursion n·F(n) at n=0) breaks the conclusion.
- S10.1 · premise_audit · S01, order_basics — Only the defined starting value is used.
- S10 · premise_audit · L_pos — The conclusion claims only F(n)≥1, not any stronger lower bound.
- S09 · premise_audit · S05, S06, S07, S08, forall_elim — Applying uniqueness needs P to have the same starting value and the same recursion, supplied by S07 and S08. It is not obtained by checking a few values of n.
- S08 · inverse_equivalence · mul_comm — Commutativity is an identity; both forms name the same number, so the step is two-way.
- S07 · inverse_equivalence · prod_def — Both sides are the same number by definition, so the equation holds both ways.
- S06 · premise_audit · prod_def, nat_closure, nat_induction — To apply S05, P must be a function ℕ→ℕ; this step confirms its codomain.
- S05 · premise_audit · S03, S04, nat_induction, function_def, forall_intro — Both the base case S03 and the step S04 are needed; checking the first few n cannot replace the induction step. This proves uniqueness only; existence comes from the MKO.
- S04 · premise_audit · S01, S02, eq_replace — Only the induction hypothesis for the same n and the two recursions are used; n is arbitrary with no extra condition. The converse, Q(n+1)⇒Q(n), is not claimed.
- S03 · premise_audit · S01, S02, eq_refl_symm_trans — It needs the two starting values to agree; if G(0)=0 the base case fails (see error control 1).
- S02 · premise_audit · S01, def_intro — No other assumption is placed on G; that is what allows S05 to conclude for every such G (generalization).
- S01 · premise_audit · G1, G2, mko_factorial_def — This step only states the definition and derives no new fact. Existence of F is a premise supplied by the MKO; uniqueness is proved in S02 to S05.





## Error controls and negative controls

0! is 1, not 0The MKO notes the common mistake of taking 0! to be 0. F(0)=1 is part of the definition. If the start were changed to H(0)=0 while keeping H(n+1)=(n+1)H(n), induction would give H(n)=0 for every n (H(n+1)=(n+1)·0=0): the whole function collapses to 0 and 5! would be 0 instead of 120. The convention that the empty product is 1 (S07) agrees with F(0)=1.

n! is not 'n times'The MKO also notes the mistake of reading n! as 'n times'. Each step of the recursion multiplies by the new factor n+1, so n! accumulates every factor from 1 to n: 3!=6, not 3, and 5!=120, not 5 and not 5·5=25. A related off-by-one error writes H(n+1)=n·H(n); then H(1)=0·H(0)=0 and every later value is 0.

Use exact integers, not floating-point approximationsThe MKO warns against passing off floating-point values outside the safe range as exact results. 23!=25852016738884976640000=2¹⁹·49308808782358125, whose odd part exceeds 2⁵³=9007199254740992. IEEE 754 binary64 has a 53-bit significand, and a positive integer within the exponent range is exactly representable if and only if its odd part is below 2⁵³, so binary64 cannot represent 23! exactly. Every computation in this guide uses exact integer multiplication.


- 0!=0 → reject — The definition gives F(0)=1, and S10 proves F(n)≥1 for every n.
- Writing the recursion as H(n+1)=n·H(n) with H(0)=1 defines the same factorial → reject — H(1)=0·1=0, whereas F(1)=1.
- Checking F(n)=∏_{k=1}^{n} k for n=0 to 5 proves it for every n → reject — A finite check covers only those n; the general statement comes from the uniqueness of S05 (induction).
- The value of 23! computed in binary64 floating point is exact → reject — The odd part of 23! exceeds 2⁵³, so binary64 cannot represent it exactly.





## Result and limitations

Exactly one function is determined by F(0)=1 and F(n+1)=(n+1)F(n) (given its existence); it equals the product ∏_{k=1}^{n} k (the empty product 1 when n=0), every value is at least 1, so 0!=1 and not 0; step-by-step substitution gives 1!=1, 2!=2, 3!=6, 4!=24 and 5!=120.


- Existence of F (the recursion theorem) is taken from the MKO statement and is not proved here; this guide proves uniqueness and the properties that follow from it.
- N8 and N9 are finite checks with the standard factorial function for n=0 to 30; they support only those n, and the argument does not depend on them.
- The statement about binary64 in error control 3 rests on the fact that the IEEE 754 binary64 format has a 53-bit significand; the text of the standard was not checked here.





## Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5
- original source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-factorial-01.json)