NF Backpropagation Approximation

The end-to-end theorem for the rounded NF reverse-mode backend. A reverse graph built from sound local nodes produces a runtime backpropagated context enclosed by the corresponding spec context.

theorem Proofs.RuntimeApprox.NFBackend.backprop_approx {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xS : TList Spec.SpecScalar Γ) (xR : TList (TorchLean.Floats.NF β fexp rnd) Γ) (epsIn : EList Γ) (seedS : TList Spec.SpecScalar (Γ ++ ss)) (seedR : TList (TorchLean.Floats.NF β fexp rnd) (Γ ++ ss)) (epsSeed : EList (Γ ++ ss)) : approxCtx toSpec xS xR epsIn → approxCtx toSpec seedS seedR epsSeed → approxCtx toSpec (g.backpropSpec xS seedS) (g.backpropRuntime xR seedR) (g.backpropBounds epsIn xR epsSeed seedR fun {Δ : List Spec.Shape} => ctxAddBound)

End-to-end NF reverse-mode soundness for a well-typed reverse graph.

This is the main composition theorem: if each node in the graph has a sound RevNode instance, then the whole backpropagated context is an approxCtx enclosure of the spec backpropagation.