Lowered Forward Evaluation: End-to-End Correctness

The proved first-order fragment and its lowered IR share the complete intermediate value table. The final theorem seeds that table with the distinguished input, uses the let-chain agreement, and selects the source return index. Equality includes evaluation errors; it is not a theorem about the broader polymorphic Program interpreter.

theorem NN.Verification.Builtin.Proved.Correctness.runForwardIR_eq_evalForward {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (p : ForwardProgram α paramShapes inShape outShape) (params : TorchLean.TensorPack α paramShapes) (x : TorchLean.Tensor α inShape) : runForwardIR (lowerForwardProgramToIR p params) x = evalForward p params x

Lowering a first-order forward program and evaluating its IR gives the same result, including errors, as evalForward on the source program.