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 {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xS : TorchLean.TensorPack Spec.SpecScalar Γ) (xR : TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) Γ) (epsIn : EList Γ) (seedS : TorchLean.TensorPack Spec.SpecScalar (Γ ++ ss)) (seedR : TorchLean.TensorPack (FloatLib.Floats.Formats.Flocq.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.