Fixed-width signed integers

The executable two's-complement carrier is accompanied by its numerical-system adapter, representation laws, arithmetic correctness theorems, and operation refinements.