> It would also help to have a formal lexical structure definition in the
> style of 7.1.1 of R7RS,
> then the srfi document can say "This srfi extends the <num R> of R7RS
> 7.1.1 with the following rules"

That's a great idea. I'll do it.

This may be complicated by the fact that implementations extend the
syntax. Kawa has many extensions, and the Chez syntax is also quite
extensive (it supports e.g. "nondecimal numbers expressed in
floating-point and scientific notation", and a #<n>r prefix for an
arbitrary radix 2..36: #3r100 is 9 and #36rz is 35). Kawa's manual has a
formal syntax spec for numbers
(https://www.gnu.org/software/kawa/Lexical-syntax.html#Numbers) but it
says it is incomplete. In Chez's manual I found only an informal
exposition in section 1.1:
<https://cisco.github.io/ChezScheme/csug9.5/intro.html#./intro:h1>

An amendment of the formal grammar of R5RS/R6RS/R7RS is great for
illustrative purposes anyway. But by the above state of things, it needs
to be augmented by an informal explanation that other things people
would ordinarily regard as "digit spans" in a number should support
underscores as well.

> (Though "no consecutive underscore" rule may be a bit awkward to express
> in EBNF).

Does is work simply to redefine <digits R> like this:

<digits R> = <digit R>+
            | <digit R>+ underscore <digits R>

Then <digits>, <digits 2>, <digits 8>, <digits 10> and <digits 16> and
<hex digit> would be re-defined similarly based on that new version of
<digits R>.