Pure semantics of chain-to-DAG conversion

LowerToDAG.Chain.eval_toDAGTerm proves that the structural conversion preserves the direct Interp.spec interpretation for every sequential chain, including custom primitives.

The induction keeps arbitrary parameter prefixes, suffixes, and temporary SSA values in the ambient environment. Parameter lookup and environment reassociation are proved independently of primitive arithmetic. Since the embedding reuses Primitive.specFwd, no agreement hypothesis between a primitive's specFwd and its executable program is needed here. Such an agreement is still required to transfer this pure result to program execution or a native backend.

theorem NN.GraphSpec.LowerToDAG.Chain.eval_toDAGTerm {α : Type} [TorchLean.Storage α] [Context α] {ps : List Spec.Shape} {σ τ : Spec.Shape} (g : Chain ps σ τ) (params : TorchLean.TensorPack α ps) (input : TorchLean.Tensor α σ) : DAG.Term.eval (params.append (TorchLean.TensorPack.cons input TorchLean.TensorPack.nil)) (toDAGTerm g) = Interp.spec g params input

Converting any sequential chain to a DAG preserves its pure tensor semantics. The embedding uses each primitive's existing specFwd; no claim about its executable program is needed.