The cifar8 (Chapter 4 deeper, 8-conv no-BN) TIE — tied through the real forward #
The 4-stage peer of CifarFold's tie (cifar_train_step_tied_certified). cifar8 is cifar (ch4)
with four conv→conv→pool stages instead of two, so its conv backward chain is the cifar chain
repeated: within each stage the second conv is the maxpool-back layer (cnnChainCotW2 for the very
last, then cifarChainCotW2's cross-pool move) and the first conv is the conv-back layer
(cnnChainCotW1). Every chain cotangent reuses an existing constructor (cnnChainCotW2 /
cnnChainCotW1 / cifarChainCotW2) at the 4-stage dims — no new constructor, no new ops, no new
bridges. The conv ties are SgdNode.convW_den/convB_den (generic in the cotangent); the dense head
ties are SgdNode.denseW_den/denseB_den at the mlpCotOut0/mlpCotOut1/g cotangents, and the
loss cotangent mirrors cifar.
No per-net fold file. cifar8 needs zero new core ops and zero new fold lemmas: every conv
layer is the generic SgdNode.convW_den/convB_den (dim- and cotangent-generic, so they certify
W₁…W₈ by instantiation), and the three dense layers are the generic SgdNode.denseW_den/
denseB_den (Foundation/SgdNodes.lean, free in activation, weight, bias and cotangent).
Spatial bookkeeping (the 2-stage (h,w) convention nested two levels deeper): final pooled (h,w);
stage 4 (conv₇/conv₈) at (2h,2w); stage 3 (conv₅/conv₆) at (2(2h),2(2w)); stage 2 (conv₃/conv₄) at
(2(2(2h)),…); stage 1 (conv₁/conv₂) at (2(2(2(2h))),…).
Not the trained artifact. No trainer runs cifar8_train_step.mlir; the packed cifar8w_*
arms the chapter's runs use feed the same chain to *Grad nodes and a separate optimizer, tied in
Cifar8TieG.cifar8_train_step_tiedG.
Scope (same as cifar) #
- Below the output layer the cotangents are the rendered chain (
mlpCotOut1/mlpCotOut0in the head;cnnChainCotW2,cnnChainCotW1,CifarFold.cifarChainCotW2below it). The loss-gradient statement isCifar8TieG.cifar8_net_lossGrad, at the trained arms'*Gradnodes and with each pool's cotangent routed to one maximal cell, as the renderedselect_and_scatterdoes; this chain'smaxPoolBackDenoteroutes it to the first maximal cell (maxPool2Argmax), the op's own choice, so it is the capstone's chain at that selection (CnnFold.cnnChainCotW2_eq_sel,CifarFold.cifarChainCotW2_eq_sel). - Conv backward rendered hand-written (cotangent SSA ↔ chain-cot per-op trust); per-op
prettylexing; ℝ → Float32.
Whole cifar8 train step, tied. All 22 parameter ops (8 conv W+b, then the dense head
W₉,b₉,Wa,ba,Wb,bb), at the real cifar8 forward, denote θ − lr·(certified ∂layer/∂θ · c) with
c the rendered backward-chain cotangent driven by the composed softmax-CE cotangent g (the
loss-gradient form is Cifar8TieG.cifar8_net_lossGrad, see the module's Scope). Each conv op is fed the cotangent the
4-stage backward chain delivers: cnnChainCotW2 (conv₈, the last before pool₄), cnnChainCotW1
(conv₇/₅/₃/₁, the within-stage conv-back), cifarChainCotW2 (conv₆/₄/₂, the cross-pool move);
the dense head is fed mlpCotOut0, mlpCotOut1 and g.