Runtime Approximation Scale Bounds

Optional scale propagation for runtime-approximation proofs.

Plain approximation lemmas track absolute error budgets. This layer additionally tracks nonnegative bounds on tensor magnitudes, usually ‖x‖∞ ≤ B, so absolute error statements can be reported as more readable absolute/relative tolerances.