FloatRep rules for numerical automation

The rules expose exact negation and multiplication through the shared operation contracts. Concrete evaluation reduces only the executable integer carrier; real decoding remains proof-only.