Binary total-order correctness

This proof entry point exports complete-data and encoded-word order laws, numerical comparison bridges, signed-zero and NaN rules, and the magnitude-order specification. Runtime clients can import TotalOrder.Runtime alone.