Definition·D107
Triangular numbers
The sum of the naturals up to k, defined by recursion: nothing at zero, and each next one adds the new top.
The triangular number function
is characterized by:
and, for every
:
In words
The zeroth triangular number is zero, and each next triangular number is the previous one plus the new top natural.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
Existence and uniqueness of
is the recursion theorem, taking start value
and step rule
at each
.
, the usual triangular number, though this wiki never needs a closed form - only that
is strictly increasing with a controlled gap (T51), which is what will make the pairing map built from it injective.