The cotangent pass — folding the certified per-layer Jacobian to ∂loss/∂θ

The Item C/D closes certify each conv/depthwise param output as θ − lr·(certified ∂(layer)/∂θ · c) for the cotangent c the backward chain delivers at that layer's output. What ties that to genuine gradient descent on the loss is the fold: the single gradient of the whole loss wrt θ equals exactly that certified Jacobian contracted with ∂loss/∂(layer output). This is the conv/depthwise analogue of mlp_hidden_total_loss_grad (MlpTrainStep.lean) — the pdiv_comp chain rule applied to loss-of-θ = (downstream loss) ∘ (the θ-weight-map), differentiable at a smooth point.

The inner factor pdiv G (layer output) k 0 = ∂loss/∂(layer output)_k IS the cotangent the backward chain delivers at the layer output — abstractly. The Item D *Cot* defs render that exact cotangent concretely (per-op faithfulness composed through the downstream). So composing this fold with Item D's pin closes the loop: θⁿ = θ − lr·∂loss/∂θ, for any conv/depthwise param, at a smooth point. The smooth-point hypothesis is bundled honestly as "the downstream loss G is differentiable at the layer output" (the relu6/BN smoothness bundle, exactly as mobilenetv2_has_vjp_at carries it).

These folds are program-wide — generic in the downstream G, so one theorem covers every conv (in CNN / CIFAR / MobileNetV2 / ResNet-34) and one covers every depthwise (MobileNetV2 / EfficientNet …). 3-axiom clean.

theorem Proofs.conv_total_loss_grad_fold {ic oc h w kH kW : ℕ} (b : Vec oc) (x : Tensor3 ic h w) (W : Kernel4 oc ic kH kW) (G : Vec (oc * h * w) → Vec 1) (hG : DifferentiableAt ℝ G (conv2d W b x).flatten) (idx : Fin (oc * ic * kH * kW)) : pdiv (fun (v : Vec (oc * ic * kH * kW)) => G (conv2d (Kernel4.unflatten v) b x).flatten) W.flatten idx 0 = ∑ k : Fin (oc * h * w), pdiv (fun (v : Vec (oc * ic * kH * kW)) => (conv2d (Kernel4.unflatten v) b x).flatten) W.flatten idx k * pdiv G (conv2d W b x).flatten k 0

Conv-layer total-loss fold. The single gradient of the whole loss wrt a conv kernel W (flattened) equals the certified ∂conv/∂W contracted with ∂loss/∂(conv output) — the chain rule (pdiv_comp) on G ∘ (conv weight-map), at any point where the downstream loss G is differentiable at the conv output (the smoothness bundle). The conv analogue of mlp_hidden_total_loss_grad; generic in G, so it covers every conv layer. The inner factor pdiv G (conv output) k 0 is the cotangent the backward chain delivers there (Item C/D's c).

theorem Proofs.conv_bias_total_loss_grad_fold {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (x : Tensor3 ic h w) (b : Vec oc) (G : Vec (oc * h * w) → Vec 1) (hG : DifferentiableAt ℝ G (conv2d W b x).flatten) (o : Fin oc) : pdiv (fun (b' : Vec oc) => G (conv2d W b' x).flatten) b o 0 = ∑ k : Fin (oc * h * w), pdiv (fun (b' : Vec oc) => (conv2d W b' x).flatten) b o k * pdiv G (conv2d W b x).flatten k 0

Conv bias total-loss fold. Same fold for the conv bias b (the bias-map is b ↦ flatten(conv W b x), differentiable everywhere).

theorem Proofs.depthwise_total_loss_grad_fold {c h w kH kW : ℕ} (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (G : Vec (c * h * w) → Vec 1) (hG : DifferentiableAt ℝ G (depthwiseConv2d W b x).flatten) (idx : Fin (c * kH * kW)) : pdiv (fun (v : Vec (c * kH * kW)) => G (depthwiseConv2d (Tensor3.unflatten v) b x).flatten) (Tensor3.flatten W) idx 0 = ∑ k : Fin (c * h * w), pdiv (fun (v : Vec (c * kH * kW)) => (depthwiseConv2d (Tensor3.unflatten v) b x).flatten) (Tensor3.flatten W) idx k * pdiv G (depthwiseConv2d W b x).flatten k 0

Depthwise total-loss fold. The depthwise analogue: the single loss gradient wrt the depthwise kernel W (flattened) equals the certified ∂(depthwiseConv2d)/∂W contracted with ∂loss/∂(depthwise output), via pdiv_comp on G ∘ (depthwise weight-map) at a smooth point.

theorem Proofs.depthwise_bias_total_loss_grad_fold {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Tensor3 c h w) (b : Vec c) (G : Vec (c * h * w) → Vec 1) (hG : DifferentiableAt ℝ G (depthwiseConv2d W b x).flatten) (o : Fin c) : pdiv (fun (b' : Vec c) => G (depthwiseConv2d W b' x).flatten) b o 0 = ∑ k : Fin (c * h * w), pdiv (fun (b' : Vec c) => (depthwiseConv2d W b' x).flatten) b o k * pdiv G (depthwiseConv2d W b x).flatten k 0

Depthwise bias total-loss fold.