NF End-To-End GraphData Bridge

End-to-end runtime→spec bridge for NF graphs executed as GraphData.

NN.Proofs.RuntimeApprox.NF provides per-op NF approximation lemmas and composes them over RevGraph via RevGraph.eval_approx and NFBackend.backprop_approx.

This file links those results to the executable SSA/DAG form used by the proof-compiled runtime: Proofs.Autograd.Algebra.GraphData.

In other words, this is where the abstract approximation graph model meets the executable graph interpreter used elsewhere in TorchLean.

theorem Proofs.RuntimeApprox.NFBackend.eval_approx_graphData {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xS : TList Spec.SpecScalar Γ) (xR : TList (TorchLean.Floats.NF β fexp rnd) Γ) (epsIn : EList Γ) : approxCtx toSpec xS xR epsIn → approxCtx toSpec (g.evalSpec xS) ((LinkAutogradAlgebra.RevGraph.toGraphData g).eval xR ()) (g.evalBounds epsIn xR)

Executable forward-pass soundness for an NF RevGraph erased to GraphData.

The theorem says that evaluating the executable GraphData forward interpreter gives the same runtime context covered by RevGraph.eval_approx, so the abstract graph approximation theorem applies to the executable representation.

theorem Proofs.RuntimeApprox.NFBackend.backprop_approx_graphData {β : 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) ((LinkAutogradAlgebra.RevGraph.toGraphData g).backpropCtx xR () seedR) (g.backpropBounds epsIn xR epsSeed seedR fun {Δ : List Spec.Shape} => ctxAddBound)

Executable backward-pass soundness for an NF RevGraph erased to GraphData.

Given approximate inputs and approximate seed cotangents, executable GraphData.backpropCtx approximates the real-spec reverse-mode result with the bound computed by the NF backend.