NF Backpropagation Approximation

The end-to-end theorem for the rounded NF reverse-mode backend. Given approximate inputs and seeds, a graph built from local approximation contracts produces a rounded reverse-pass context within the propagated bounds of the supplied spec reverse pass. Derivative correctness of that spec pass is a separate premise when interpreting the result as a gradient guarantee.

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.

Compose the node-local approximation bounds with NF context-addition bounds. Input and seed errors are explicit premises; shared-node accumulation includes its rounding error.