What the document text size is set to.
The same shape as [FontSetting], for the same reason: following the default is a state, persisted as no key, and a chosen size is always written, even when it is today's default, so a person who picked 16 keeps 16 if the default ever moves.
