Logarithmic-system rules for numerical automation

Multiplication is exact in the encoded sign/exponent representation. The real-valued decoder is proof-facing and remains absent from compiled kernels.