TorchLean API

NN.Proofs.RuntimeApprox.NF.BackwardOps

BackwardOps #

NF reverse-mode runtime-to-spec approximation lemmas.

The public theorem is NFBackend.backprop_approx: a reverse graph built from sound local NF nodes has a backpropagated runtime context enclosed by the spec backpropagated context. The local node families cover sparse VJP contexts, context accumulation, primitive operations, and linear algebra.