Fixed-state derivative seeds

Input derivatives use zero directions for parameters, but a subsequent pullback differentiates with respect to the whole context. We therefore interpret the runtime seed as a jet on the full parameter-and-input space. This preserves parameter dependence without requiring a normed-space instance on the heterogeneous tensor pack or on the sealed model-state type.

theorem TorchLean.TensorPack.JetRelated.const_append_seed {shapes : List Spec.Shape} {shape : Spec.Shape} {n : ℕ} (state : TensorPack ℝ shapes) (input : Tensor ℝ shape) (directions : Fin n → Tensor ℝ shape) : JetRelated (fun (k : Fin n) => Proofs.Autograd.flattenCtx (zero.append (singleton (directions k)))) (Proofs.Autograd.flattenCtx (state.append (singleton input))) Proofs.Autograd.unflattenCtx ((map (fun {shape : Spec.Shape} => Tensor.map (Runtime.Autograd.Model.Dual.Nested.ofPrimal n)) state).append (singleton (Runtime.Autograd.Model.Dual.Nested.seedTensor directions input)))

Constant state followed by a seeded input is the full-context jet in input-only directions.

The base point still contains all state entries. Zero parameter directions mean that this jet takes input derivatives; they do not remove parameter dependence from the differentiated map.