The cifar8-bn step tie at its UN-FUSED gradient nodes — the packed cifar8w_bn_* arms #
Cifar8BnTie.cifar8Bn_train_step_tied_certified ties the fused-SGD render
(cifar8BnTrainStepText at opt := none). The artifacts the book's Chapter-4 runs train
(cifar8w_bn_{sgd,mom,adam}_train_step.mlir, and the narrow cifar8_bn_* width sweep) are the same
renderer at opt := some _: the same forward and backward chain, feeding *Grad ops (the *Sgd
arms with θ − lr· stripped) to a separate optimizer. This file states those nodes, each at the
same chain cotangent: all 38 parameter tensors, via GradNode (Foundation/SgdNodes.lean). The
optimizer update that consumes them (SGD, Nesterov, AdamW) is outside the statement.
Scope (as the fused tie) #
- Below the output layer the cotangents are the rendered chain.
cifar8Bn_net_lossGrad(Cifar8BnParamGrad) states each node as the loss gradient in its parameter, with each pool's cotangent routed to one maximal cell, as the renderedselect_and_scatterdoes; this chain'sBack3.maxpoolroutes it to the first maximal cell (maxPool2Argmax), the op's own choice, so each pool step is the capstone's scatter at that selection (SmallParamGrad.maxpool_flatDenote_eq_selScatter). - Conv/BN backward rendered hand-written (cotangent SSA ↔ chain-cot per-op trust); per-op
prettylexing; ℝ → Float32.
theorem
Proofs.Cifar8BnTieG.cifar8Bn_train_step_tiedG
{ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ}
(xN vN epsStr cotN : String)
(W₁ : Kernel4 c1 ic kH kW)
(b₁ : Vec c1)
(ε₁ : ℝ)
(γ₁ β₁ : Vec c1)
(W₂ : Kernel4 c1 c1 kH kW)
(b₂ : Vec c1)
(ε₂ : ℝ)
(γ₂ β₂ : Vec c1)
(W₃ : Kernel4 c2 c1 kH kW)
(b₃ : Vec c2)
(ε₃ : ℝ)
(γ₃ β₃ : Vec c2)
(W₄ : Kernel4 c2 c2 kH kW)
(b₄ : Vec c2)
(ε₄ : ℝ)
(γ₄ β₄ : Vec c2)
(W₅ : Kernel4 c3 c2 kH kW)
(b₅ : Vec c3)
(ε₅ : ℝ)
(γ₅ β₅ : Vec c3)
(W₆ : Kernel4 c3 c3 kH kW)
(b₆ : Vec c3)
(ε₆ : ℝ)
(γ₆ β₆ : Vec c3)
(W₇ : Kernel4 c4 c3 kH kW)
(b₇ : Vec c4)
(ε₇ : ℝ)
(γ₇ β₇ : Vec c4)
(W₈ : Kernel4 c4 c4 kH kW)
(b₈ : Vec c4)
(ε₈ : ℝ)
(γ₈ β₈ : Vec c4)
(W₉ : Mat (c4 * h * w) d1)
(b₉ : Vec d1)
(Wa : Mat d1 d1)
(ba : Vec d1)
(Wb : Mat d1 nClasses)
(bb : Vec nClasses)
(x : Tensor3 ic (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))))
(label : Fin nClasses)
:
have xv := x.flatten;
have cc1 := flatConv W₁ b₁ xv;
have bn1o := bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₁ γ₁ β₁ cc1;
have r1 := relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) bn1o;
have r1t := Tensor3.unflatten r1;
have cc2 := flatConv W₂ b₂ r1;
have bn2o := bnPerChannelTensor3 c1 (2 * (2 * (2 * (2 * h)))) (2 * (2 * (2 * (2 * w)))) ε₂ γ₂ β₂ cc2;
have r2 := relu (c1 * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) bn2o;
have r2t := Tensor3.unflatten r2;
have zp1 := maxPoolFlat c1 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) r2;
have zp1t := Tensor3.unflatten zp1;
have cc3 := flatConv W₃ b₃ zp1;
have bn3o := bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₃ γ₃ β₃ cc3;
have r3 := relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) bn3o;
have r3t := Tensor3.unflatten r3;
have cc4 := flatConv W₄ b₄ r3;
have bn4o := bnPerChannelTensor3 c2 (2 * (2 * (2 * h))) (2 * (2 * (2 * w))) ε₄ γ₄ β₄ cc4;
have r4 := relu (c2 * (2 * (2 * (2 * h))) * (2 * (2 * (2 * w)))) bn4o;
have r4t := Tensor3.unflatten r4;
have zp2 := maxPoolFlat c2 (2 * (2 * h)) (2 * (2 * w)) r4;
have zp2t := Tensor3.unflatten zp2;
have cc5 := flatConv W₅ b₅ zp2;
have bn5o := bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₅ γ₅ β₅ cc5;
have r5 := relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) bn5o;
have r5t := Tensor3.unflatten r5;
have cc6 := flatConv W₆ b₆ r5;
have bn6o := bnPerChannelTensor3 c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ β₆ cc6;
have r6 := relu (c3 * (2 * (2 * h)) * (2 * (2 * w))) bn6o;
have r6t := Tensor3.unflatten r6;
have zp3 := maxPoolFlat c3 (2 * h) (2 * w) r6;
have zp3t := Tensor3.unflatten zp3;
have cc7 := flatConv W₇ b₇ zp3;
have bn7o := bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₇ γ₇ β₇ cc7;
have r7 := relu (c4 * (2 * h) * (2 * w)) bn7o;
have r7t := Tensor3.unflatten r7;
have cc8 := flatConv W₈ b₈ r7;
have bn8o := bnPerChannelTensor3 c4 (2 * h) (2 * w) ε₈ γ₈ β₈ cc8;
have r8 := relu (c4 * (2 * h) * (2 * w)) bn8o;
have r8t := Tensor3.unflatten r8;
have zp4 := maxPoolFlat c4 h w r8;
have h9 := dense W₉ b₉ zp4;
have ha := dense Wa ba (relu d1 h9);
have g := fun (k : Fin nClasses) =>
softmax nClasses
(cifarCnnBn8Forward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆ β₆ W₇
b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb xv)
k - oneHot nClasses label k;
have cpool4 := (cnnDenseHeadCot W₉ Wa Wb h9 ha).denote g;
have dyBn8 := fun (i : Fin (c4 * (2 * h) * (2 * w))) =>
if bn8o i > 0 then (IR.Back3.maxpool r8t IR.Back3.cot).flatDenote cpool4 i else 0;
have cotC8 := bnPerChannelTensor3GradInput c4 (2 * h) (2 * w) ε₈ γ₈ cc8 dyBn8;
have dyBn7 := fun (i : Fin (c4 * (2 * h) * (2 * w))) =>
if bn7o i > 0 then (IR.Back3.conv W₈ IR.Back3.cot).flatDenote cotC8 i else 0;
have cotC7 := bnPerChannelTensor3GradInput c4 (2 * h) (2 * w) ε₇ γ₇ cc7 dyBn7;
have dyBn6 := fun (i : Fin (c3 * (2 * (2 * h)) * (2 * (2 * w)))) => if bn6o i > 0 then ⋯ else 0;
have cotC6 := bnPerChannelTensor3GradInput c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ cc6 dyBn6;
have dyBn5 := ⋯;
⋯
Whole cifar8-bn train step at its gradient nodes. All 38 parameter tensors (8 conv W+b,
8 BN γ+β, 3 dense W+b), at the real cifar8-bn forward: each emitted *Grad node denotes
the certified per-layer Jacobian contracted with the rendered backward-chain cotangent, driven
by the composed softmax-CE cotangent g — the fused tie's chain, node for node.