PoC: the cifar8 (Chapter 4 deeper, 8-conv no-BN) §1a TIE — tied through the real forward #
The 4-stage peer of CifarFold's §1a tie (cifar_conv_tied_certified). cifar8 is cifar (ch5)
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 CifarPoC.convW_den/convB_den (generic in the cotangent); the dense head
- loss-cot mirror cifar.
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))),…).
Honest residual (same as cifar) #
- Conv backward rendered hand-written (cotangent SSA ↔ chain-cot per-op trust); per-op
prettylexing; ℝ → Float32.
The emitted loss-cotangent graph denotes the softmax-CE gradient of the cifar8 forward.
Dense output weight Wb, tied to the WHOLE softmax-CE loss through the cifar8 forward. The
dense head is the standard 3-layer MLP; given the forward logits = mnistLinear Wb bb a_head
(true by Function.comp_apply, supplied as hlog), Wb folds to ∂CE/∂Wb.
Whole cifar8 conv tail, tied. All 16 conv params (8 conv W+b), at the real cifar8 forward
and the composed softmax-CE cotangent, denote the certified loss-descent step. 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). Together with the dense head (cifar8_Wb_tied_totalloss + the generic
denseW_den/denseB_den at g) the WHOLE cifar8 train step is den-composed forward→loss→backward.