Primitive NF Reverse Nodes

Reverse-mode approximation nodes for scalar, elementwise, reduction, and activation operations. Each node packages the forward operation, the spec VJP, the rounded runtime VJP, and the local error bound proof used by graph-level backpropagation.

noncomputable def Proofs.RuntimeApprox.NFBackend.addRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : RevNode toSpec Γ s

Reverse node for addition: z = a + b.

VJP is (δ ↦ (δ, δ)), with a special-case when a and b are the same context index.

noncomputable def Proofs.RuntimeApprox.NFBackend.subRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : RevNode toSpec Γ s

Reverse node for subtraction: z = a - b.

VJP is (δ ↦ (δ, -δ)), with a special-case when a and b are the same context index.

noncomputable def Proofs.RuntimeApprox.NFBackend.mulRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : RevNode toSpec Γ s

Reverse node for multiplication: z = a * b.

VJP is (δ ↦ (δ*b, δ*a)), with rounding-aware bounds produced by the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.scaleRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (c : TorchLean.Floats.NF β fexp rnd) : RevNode toSpec Γ s

Reverse node for scaling by a constant: z = c * a.

noncomputable def Proofs.RuntimeApprox.NFBackend.negRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for negation: z = -a.

noncomputable def Proofs.RuntimeApprox.NFBackend.expRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for exp.

noncomputable def Proofs.RuntimeApprox.NFBackend.tanhRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for tanh.

noncomputable def Proofs.RuntimeApprox.NFBackend.sigmoidRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for sigmoid.

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for softplus.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) (ε : ℝ) (hε : 0 < ε) : RevNode toSpec Γ s

Reverse node for a log with an explicit stabilization parameter ε (to avoid log 0-style issues).

noncomputable def Proofs.RuntimeApprox.NFBackend.softmaxRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for the scalar softmax node, using the analytic ℝ derivative plus NF error bounds.

noncomputable def Proofs.RuntimeApprox.NFBackend.reluRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ s

Reverse node for ReLU, using the standard piecewise derivative/VJP.

noncomputable def Proofs.RuntimeApprox.NFBackend.sumRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {s : Spec.Shape} (a : Idx Γ s) : RevNode toSpec Γ Spec.Shape.scalar

Reverse node for reduction sum, sending the upstream gradient back along the broadcasted shape.