Runtime Rounding Approximation

Scalar approximation lemmas for proof-relevant rounded arithmetic.

This layer reasons about the noncomputable rounded-real model FloatLib.Floats.Formats.Flocq.round, exposed locally as roundR: one scalar operation is replaced by a rounded scalar operation, and the proof records the resulting ulp-style error budget. Tensor and graph modules lift these scalar facts to operators and end-to-end executions.

The public vocabulary is focused:

• scalarApprox is the absolute-error predicate for one real scalar;
• roundR is one modeled rounding step;
• roundedAdd and roundedMul are the rounded scalar operations used by NF semantics;
• scalarApprox_roundedAdd and scalarApprox_roundedMul are the compositional error rules.