Convolution backward-dot proof entry point.

The split files isolate the input, weight, and main algebraic components needed to justify convolution-gradient computations in the tape semantics.