Rayo's number is the least nonnegative integer exceeding every nonnegative integer specified
by a sentential formula with fewer than a googol symbols, using the language and semantic interpretation
of the bounded-length Rayo function 
. This is the strict-length convention of the formal construction
in Rayo's "Big Number Duel." The number is 
.
Let 
denote the exact-length variant of
the Rayo function, whose values begin 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 1, 0, ... at 
(OEIS A368006). Then
the strict-length definition is equivalently
 |
Taking this maximum implements the bound on formula length. The inclusive wording in Rayo (2019, p. 228) permits at most a googol symbols
and corresponds to 
.
