I don’t honestly see what kind of attack could be defeated by multiplying by a fixed value (maybe because there isn’t one, or likely because I simply can’t) but

I don’t honestly see what kind of attack could be defeated by multiplying by a fixed value (maybe because there isn’t one, or likely because I simply can’t) but sure, why not! It feels like good hygiene, can be done with just the X25519 function and a scalar field multiplication, and I imagine it can help with proofs. Any reason not to use a simpler SHA-512(ID || <PK>) value for t? BTW, I was about to report an errata for RFC 8017, until I realized they inverted both the order and the starting index in going from X_n to x_n... yeah, as much as I’d like not to redefine that function every time, I might keep calling it big endian fixed size encoding.