I didn’t mean to imply that it was in the paper as I have it, that’s why I said based on instead of from, sorry if that was confusing. It’s a presentational thing and it’s fine to just use instead (although I think a bit less clean).
I don’t see how there’s an implicit optimality assumption unless you’re trying to read quantities at every step in the proof as a program length. I agree that there’s something aesthetically worse about a proof that routes through something less nicely interpretable.
I didn’t mean to imply that it was in the paper as I have it, that’s why I said based on instead of from, sorry if that was confusing. It’s a presentational thing and it’s fine to just use
I don’t see how there’s an implicit optimality assumption unless you’re trying to read quantities at every step in the proof as a program length. I agree that there’s something aesthetically worse about a proof that routes through something less nicely interpretable.