Product-reduction differentiation

Dual numbers derive the exact leave-one-out differential of product reduction. The reverse rule is zero-aware and requires no division by primal entries.

def TorchLean.Tensor.Internal.Rep.productReduceDifferential {R : Type u} [Storage R] [CommSemiring R] {s t : Shape} (f : Coord s → Coord t) (inputTensor inputTangent : Rep R s) : Rep R t

The algebraic directional derivative of product reduction.

For each possible selected input coordinate, the Leibniz rule multiplies its tangent by every other primal value in the same reduction fiber. This formula is valid in a commutative semiring: it uses neither subtraction nor division.

def TorchLean.Tensor.Internal.Rep.productReduceVjp {R : Type u} [Storage R] [CommSemiring R] {s t : Shape} (f : Coord s → Coord t) (inputTensor : Rep R s) (outputCotangent : Rep R t) : Rep R s

The zero-aware reverse map for product reduction.

The product explicitly omits the selected input coordinate. Unlike a formula written as the forward product divided by that input, it remains correct when one or more primal values are zero.

theorem TorchLean.Tensor.Internal.Rep.dot_productReduceDifferential_eq_dot_productReduceVjp {R : Type u} [Storage R] [CommSemiring R] {s t : Shape} (f : Coord s → Coord t) (inputTensor inputTangent : Rep R s) (outputCotangent : Rep R t) : (productReduceDifferential f inputTensor inputTangent).dot outputCotangent = inputTangent.dot (productReduceVjp f inputTensor outputCotangent)

The product-reduction differential and its zero-aware reverse map are adjoint under the finite tensor pairing.

The proof partitions the input pairing by reduction fibers, then chooses the same omitted-coordinate product on both sides. It therefore covers empty fibers and every pattern of zero primal values without side conditions.