Linear-time canonical binary addition -- proof internals

This aggregation module collects the pure arithmetic, scan, rewind, resource, and output-discipline proofs used by the public surface.