Spec-level gradient identities for the linear layer

This file records the tensor formulas used by the derivative specification of a linear layer:

y = W x + b

namely:

• ∂L/∂W = δ ⊗ x (outer product),
• ∂L/∂x = Wᵀ δ (matrix-vector multiply), and
• ∂L/∂b = δ.

These are normalization lemmas for TorchLean's derivative specification. They do not prove that a runtime backward pass is the Fréchet derivative of the forward pass; those results live under NN.Proofs.Autograd.

PyTorch correspondence / citations

• torch.nn.Linear / torch.nn.functional.linear implement y = x Wᵀ + b with weight stored as shape (out_features, in_features) (so the math “matrix” is W with output rows). TorchLean’s LinearSpec follows the same convention: weights : Tensor α [outDim, inDim]. https://pytorch.org/docs/stable/generated/torch.nn.Linear.html https://pytorch.org/docs/stable/generated/torch.nn.functional.linear.html
• The “outer product” view of the weight gradient corresponds to the common vector formula grad_W = δ ⊗ x (PyTorch has torch.outer for vectors). https://pytorch.org/docs/stable/generated/torch.outer.html

References

• Standard matrix calculus / backpropagation identities; no single source is required.

theorem Proofs.linearWeightsDerivSpec_eq_outerProductSpec {inDim outDim : ℕ} (x : TorchLean.Tensor ℝ [inDim]) (δ : TorchLean.Tensor ℝ [outDim]) : Spec.linearWeightsDerivSpec x δ = Spec.outerProductSpec δ x

Spec identity: weight gradient for a linear layer.

For y = W x + b, if δ = ∂L/∂y then the weight gradient is

∂L/∂W = δ ⊗ x.

For a batch, PyTorch evaluates the corresponding formula as a matrix multiplication against the input batch.

theorem Proofs.linearInputDerivSpec_eq_vecMatMulSpec {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) (δ : TorchLean.Tensor ℝ [outDim]) : Spec.linearInputDerivSpec layer.weights δ = Spec.vecMatMulSpec δ layer.weights

Spec identity: input gradient for a linear layer.

For y = W x + b, the input gradient is

∂L/∂x = Wᵀ δ.

theorem Proofs.linearBackwardSpec_biasGradient {inDim outDim : ℕ} (layer : Spec.LinearSpec ℝ inDim outDim) (x : TorchLean.Tensor ℝ [inDim]) (δ : TorchLean.Tensor ℝ [outDim]) : (Spec.linearBackwardSpec layer x δ).biasGradient = δ

The complete linear backward result passes the bias cotangent through unchanged.

For y = W x + b, the bias gradient is ∂L/∂b = δ.