🚀 go-pugleaf

A problem with your proposals (2) and (3) is that they violate the
sanctity of the local-part.  Your software that might try to recognize
          AAA!BBB!CCC%DDD@EEE
 as meaning the user CCC on Usenet host BBB would be making possibly
incorrect assumptions about how EEE parses its local parts.  On a
suitably unusual computer "AAA!BBB!CCC%DDD" could be a local user name;
there is no way for your site to know how what those special characters
mean to EEE.  If, perhaps, you know that EEE treats % in the local part
as synonymous with @, then you have the next level of assumption, about
how DDD parses ITS local-part, and then AAA.
                                        barmar