Runtime Approximation Proofs #
Umbrella import for TorchLean's executable-runtime-to-real-spec approximation theorems.
The stack is intentionally layered:
Core: tolerance objects and tensor/context approximation predicates;Rounding: scalarneural_rounderror lemmas;Graph: forward and reverse graph composition theorems;NF: proof-relevant rounded tensor/operator backend;FP32: convenient FP32-specialized layer/MLP/CROWN statements;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.