Signed fits from magnitude envelopes #
A representable nonnegative envelope covers every integer whose absolute value is at most it. The envelope itself must fit: the asymmetric signed range still excludes its positive endpoint.
Main results #
Fits.of_natAbs_le: derive signed fitting from a representable natural magnitude envelope.
This elementary bound is original.