Runtime Approximation Proofs

Umbrella import for TorchLean's executable-runtime-to-real-spec approximation theorems.

The runtime-approximation library is intentionally layered:

• Core: tolerance objects and tensor/context approximation predicates;
• Rounding: scalar FloatLib rounding-error lemmas;
• Graph: forward and reverse graph composition theorems;
• NF: proof-relevant rounded tensor/operator backend;
• FP32: convenient FP32-specialized layer/MLP/CROWN statements;
• Optimizer: one finite-run contract for numerical optimizer updates;
• Reductions: error bounds for rounded-addition trees and finite binary32 schedules;
• Scale: optional magnitude propagation for abs/rel tolerance reporting.

Leaf modules stay available for developers working on one operator family, but public entrypoints and CI should import this umbrella rather than listing every runtime-approximation file by hand.