PoC: the cifar8-bn (Chapter 4 deeper, 8-conv per-channel BN) §1a TIE #
cifar8's §1a tie + a BN-back at every conv. The backward
chain alternates BN-output cotangent dyBnᵢ (relu-masked — fed to the γ/β ops) and conv-output
cotangent cotCᵢ (bnPerChannelTensor3_grad_input of dyBnᵢ — fed to the conv W/b ops), repeated
over 4 conv→conv→pool stages, crossing each pool as conv-back then maxpool-back.
Zero new ops/bridges/constructors. Conv ties reuse CifarPoC.convW_den/convB_den; BN ties reuse
CifarBnPoC.bnGamma_den/bnBeta_den; dense head + loss-cot reuse Cifar8PoC/cifar. All 38 params
(8 conv W/b + 8 BN γ/β + 3 dense) fold with the generics — the cifar8-bn lesson applied to the tie.
Honest residual (same as the rest of the suite) #
- Conv/BN backward rendered hand-written (cotangent SSA ↔ chain-cot per-op trust); per-op
prettylexing; BN0 < εsmoothness; ℝ → Float32.
theorem
Proofs.Cifar8BnPoC.cifar8BnLossCot_den
{ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ}
(nlogN ohN : 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 : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))))
(label : Fin nClasses)
:
StableHLO.den
((StableHLO.SHlo.operand nlogN
(cifarCnnBn8Forward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆
β₆ W₇ b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb x)).expe.softmaxDiv.sub
(StableHLO.SHlo.operand ohN (oneHot nClasses label))) = fun (j : 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 x)
j - oneHot nClasses label j
The emitted loss-cotangent graph denotes the softmax-CE gradient of the cifar8-bn forward.
theorem
Proofs.Cifar8BnPoC.cifar8Bn_convbn_tied_certified
{ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ}
(xN wN bN gN vN epsStr lrStr 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)
(lr : ℝ)
:
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 := bnPerChannelTensor3_grad_input 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 := bnPerChannelTensor3_grad_input 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 := bnPerChannelTensor3_grad_input c3 (2 * (2 * h)) (2 * (2 * w)) ε₆ γ₆ cc6 dyBn6;
have dyBn5 := ⋯;
⋯
Whole cifar8-bn conv+BN tail, tied. All 32 conv/BN params (8 conv W+b, 8 BN γ+β), at the
real cifar8-bn forward and the composed softmax-CE cotangent, denote the certified loss-descent
step. The conv ops are fed the BN-back cotangents cotC1–8; the BN ops the relu-masked
cotangents dyBn1–8; both are the genuine cifar8-bn backward chain (cifar8's chain + a BN-back at
every conv). Dense head + loss-cot reuse Cifar8PoC/cifar.