Commit 2024-07-08 14:54 60b7d340

chore: tidy three miscellaneous porting notes (#14511) One porting note seems clearly superfluous now. In another, make the note match the statement below it (some variable renaming had made them go out of sync). Fix a third porting note; to me, the new proof feels good enough.