Bounded fixed-point rules for numerical automation

Symbolic goals use the proved operation contracts. Concrete reduction unfolds the signed-word kernels only during the explicit closed-term phase.