Neither changing nor removing the "video=" part of the /etc/default/grub
file had any effect. But the bigness of the font in the real-time boot
log display is a cosmetic issue. The grub menu is now as it should be,
and the system boots correctly. That was the real issue. So I consider
this issue solved.
I thank everyone who tried to help. This home user could not have done
it without you.