Upgrading the CNN conv close from a generic cotangent to the actual backward chain #
cnn_render_conv{W,b}_certified (CnnTrainStep.lean) certify each conv parameter output for
any cotangent c at that conv layer's output. This file pins c to the cotangent the CNN
backward chain actually delivers — the conv analogue of the MLP's mlpCotOut0/1.
The chain, from the loss cotangent dy at the logits, all in flattened Vec space:
- dense head (
W₅→relu→W₄→relu→W₃) is a flatIR.Backchain (emitDenseBack/emitReluBacksubst, themlpCotOutmechanism) → the cotangentcpoolat the flattened pool output;
- maxpool-back is an
IR.Back3node viewed throughflatDenote(crossing the flatten boundary), then relu-back (theselMask4maskrelu'(hc2)⊙·) → the cotangent at conv2's output (W₂'s layer); - conv2-back is another
Back3node viaflatDenote, then relu-back → conv1's output (W₁).
The relu masks sit between the maxpool and conv Back3 nodes, so the cotangent is a flat-level
composition of the rendered backward denotations (not a single Back3 graph) — but the
maxpool/conv steps are exactly the Back3 subgraphs flatDenote denotes. Instantiating the
generic conv bridges at these cotangents gives: each conv θ output denotes θ − lr·(certified ∂conv/∂θ · the-actual-chain-cotangent). (This pins the cotangent — the further "= ∂loss/∂θ" fold
is the separate pdiv G = Back.denote step, as in the MLP mlp_*_total_loss_grad.)
See planning/archive/render_close_handoff.md §1 "Optional polish".
Dense-head backward subgraph — dy at the logits to the cotangent at the flattened
pool output: W₃·(relu'(h3)⊙(W₄·(relu'(h4)⊙(W₅·dy)))). The flat Back chain of the CNN's
classifier head (3 dense + 2 relu); the 3-layer analogue of mlpCotOut0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cotangent the backward chain delivers at conv2's output (W₂'s layer):
relu'(hc2) ⊙ maxpool-back(dense-head-cot dy). The maxpool step is the Back3 maxpool node
through flatDenote (crossing the flatten/pool boundary); the relu-back is the rendered
selMask4 mask.
Equations
- Proofs.cnnChainCotW2 W₃ W₄ W₅ h3 h4 ac2 hc2 dy i = if hc2 i > 0 then (Proofs.IR.Back3.maxpool ac2 Proofs.IR.Back3.cot).flatDenote ((Proofs.cnnDenseHeadCot W₃ W₄ W₅ h3 h4).denote dy) i else 0
Instances For
The cotangent the backward chain delivers at conv1's output (W₁'s layer):
relu'(hc1) ⊙ conv2-back(W₂, conv2-cotangent). The conv2-back step is the Back3 conv node
through flatDenote; the relu-back is the rendered selMask4 mask. Builds on
cnnChainCotW2 exactly as mlpCotOut0 prepends one more relu-back ∘ dense-back to
mlpCotOut1.
Equations
- Proofs.cnnChainCotW1 W₂ hc1 cotW2 i = if hc1 i > 0 then (Proofs.IR.Back3.conv W₂ Proofs.IR.Back3.cot).flatDenote cotW2 i else 0
Instances For
The conv1-output cotangent equals the explicit rendered backward form
relu'(hc1) ⊙ flatten(convBackDenote W₂ (unflatten cotW2)) — i.e. the relu mask applied to
the reversed-kernel conv backward the renderer emits (selMask4 ∘ convBack).
The conv2-output cotangent equals the explicit rendered backward form
relu'(hc2) ⊙ flatten(maxPoolBackDenote ac2 (unflatten (dense-head-cot dy))) — the relu mask
applied to the select_and_scatter maxpool backward the renderer emits.
Conv-2 weight output, chain-certified. W₂ⁿ = W₂ − lr·(transpose-trick kernel grad)
denotes W₂ − lr·(certified ∂conv2/∂W₂ · the cotangent the chain delivers at conv2) — the
generic cnn_render_convW_certified instantiated at cnnChainCotW2.
Conv-2 bias output, chain-certified.
Conv-1 weight output, chain-certified. W₁ⁿ denotes W₁ − lr·(certified ∂conv1/∂W₁ · the deepest chain cotangent) — the generic bridge at cnnChainCotW1 (which crosses one
more conv-back than cnnChainCotW2, the Back3 chain step).
Clause Props for the per-example conv ties #
Each is a conv _den lemma's statement (CifarPoC.convW_den / convB_den, CnnPoC.cW2_den …)
under ∀, so a tie theorem states one line per parameter tensor and intro unfolds it back. The
batched peers are ResNet34PoCB.ConvWTiedB and EnetPoC.ConvWSgdTiedB.
The emitted convWeightSgd op, fed the cotangent c at the conv output, is the certified SGD
step on the kernel W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The emitted convBiasSgd op, fed the cotangent c at the conv output, is the certified SGD
step on the bias b.
Equations
- One or more equations did not get rendered due to their size.