EfficientNet-B0's step tie at the un-fused gradient and the smoothed loss #

EfficientNetStepTie.lean ties all 262 parameters of the SGD-inline efficientnet_train_step.mlir: each fused theta - lr * g op dens to the certified step at the cotangent the emitted backward chain delivers. This file is that statement re-pointed along two axes.

Axis 1 — the gradient node. Every conjunct is at the raw gradient node (*GradB), which is what efficientnet_adam_train_step.mlir and the f32 efficientnetin_* artifacts emit; the fused op appears only in the SGD-inline file. The optimizer update that consumes the node (Adam, RMSProp, EMA, clipping) is outside this statement. The threaded forward is efficientnetForwardBFullDrop at the renderer's two optional sites (below). GradNodesB is the fold each conjunct delegates to.

Precision is a flag on the statement. The ImageNet run the book reports trains from efficientnetin_emarmsdp64dropdowxeps0001bf16, whose conv and depthwise weight gradients are the bf16 kinds (convWeightGradBBf16, depthwiseWeightGradBBf16, …; Foundation.Bf16GradNodes). Every conv and depthwise weight node below is stated on the renderers' switch — ConvWTiedBAt bf16 / ConvStridedXlaWTiedBAt bf16 / DepthwiseWTiedBAt bf16 / DepthwiseStridedXlaWTiedBAt bf16 (Foundation.GradNodesBAt): bf16 := false is the f32 node, bf16 := true the bf16 one — and the capstone efficientnet_net_tiedG takes bf16, so it reaches the bf16 artifacts' gradient nodes read over ℝ exactly as it reads the f32 ones (Bf16Erasure: at the identity rounding the bf16 kind denotes what its f32 peer does). The squeeze-excite and classifier denses, BatchNorm and the bias nodes carry no flag because no render switches them.

The training masks are optional sites on the statement. efficientnetin_emarmsdp64dropdowxeps0001bf16 is a dropdo artifact: stochastic depth on the nine skip-carrying blocks (b3 b5 b7 b8 b10 b11 b13 b14 b15, the renderer's enetDropIdxs, a per-example scale %dp<i> on the residual branch before the skip add) and classifier dropout (%do, per element, between the GAP and the dense). The capstone takes them as sd : Option (Fin 9 → Vec N) and cd : Option (Vec (N * 1280)) (Proofs.Foundation.DropSites; the forward is efficientnetForwardBFullDrop at the same binders): none is the drop-free artifacts' chain — the statement exactly as it was — and some the *drop* / *do* / dropdo artifacts'. At a drop site the backward applies the same scale to the block-output cotangent on its way into the BRANCH and leaves the skip's raw (eBack's rule, Proofs.dropPath_vjp_is_self): the block's parameter nodes are tied at dropPathOpt … dy, and the block VJP that threads the chain is mbResidDropWHasVJP, whose backward is that by definition. At the head the dense weight node reads the DROPPED activation and the classifier's input-VJP passes through the mask before the GAP backward (headDoFwdBHasVJP), as MobileNetV2StepTieB's does.

Axis 2 — the loss. The capstone's top-of-chain cotangent is smoothedLossCotGraph's (Foundation/SmoothedLossCot.lean), at a general target: the six-op chain softmaxRow → subB → scaleB → addVB → shiftB → divConstB the batched renders emit, with the target arriving as the graph input %onehot — a soft vector under mixup or cutmix. The fused file pins it to softmax − oneHot, the gradient of plain cross-entropy at a hard label. unrowB / rowB are ResNet-34's casts between the loss chain's one-row-per-example index and the dense ops' plain per-example width.

Relation to the fused file #

Every cotangent chain, every forward activation and every Jacobian witness is EfficientNetStepTie.lean's, unchanged. The fusion is rfl — *SgdB_eq_grad says the fused op is theta - lr * applied to the un-fused one — so each conjunct's proof is the fused file's with the wrapper peeling dropped. The lr, wN, bN, gN and lrStr binders disappear with the wrapper.

The head takes g as a parameter here. The fused enetHeadTied computes g := rowSoftmax(logits) − onehot internally, which is what pinned that file to the hard label. The per-block ties are forall cot statements and were already loss-agnostic, so only the head and the capstone differ.

Conventions carried unchanged from the fused file: batch BatchNorm (bnBatchLA), XLA-SAME at the 3x3/s2 stem and at the four strided depthwises (TF's padding at every strided conv since D3, 2026-10-12), swish (no kink, so no smoothness hypothesis anywhere), and the SE gate's fan-in folded into the block VJPs.

One replica. Every statement here is at one replica's node. Every B0 data-parallel render synchronises BatchNorm; its all-reduced gradients are efficientnet_net_syncTiedG (EfficientNetSyncStepTieG.lean): this file's node at N := R·N, at the same mask sites.

Strided downsampling MBConv block — all 16 params tied (b2/b4/b6/b12) #

Same as the expand block EXCEPT the expand stage lives at the block-input grid 2h×2w and the depthwise is strided (depthwiseStridedXlaWeightGradB, the expand-side cotangent cotEr upsamples h→2h via dStridedXlaInB). No skip (spatial+channels change).

No-expand MBConv block (b1, t=1) — all 12 params tied (depthwise on ic → SE → project) #

NO expand conv: the depthwise runs directly on the block input (ic channels). 12 params (4 depthwise+BN, 4 SE, 4 project). The SE squeeze/excite is on ic channels (ic → r → ic).

Stem — the 3×3/s2 conv-bn-swish (4 params), feeding block 1 #

swish(bn(convStride2Xla Ws bs x)), 3→32 at 224→112, at the XLA-SAME phase the shipped stem uses. The cotangent block 1 delivers at the stem swish output (dyStem) lifts through swish-back

• true-BN-back to the conv-out cotangent (the convStridedXlaWeightGradB consumes it; NO conv-back past %x). 4 params.

Head — the 1×1 conv-bn-swish (4 params) → GAP → dense (Wfc/bfc), + the loss cotangent #

dense(GAP(swish(bn(conv Wh bh))))) (320→1280 conv, GAP, 1280→nClasses dense). The loss cotangent g is a parameter here (the capstone supplies the smoothed-loss chain's). The head conv params tie at the chain cotangent (g → dense-back → GAP-back → swish/BN-back); the dense Wfc/bfc tie at g directly.

Bundle-taking *TiedAt wrappers — one per block type, for the whole-net thread #

Each takes the B0Weights block bundle (MBW/MBWNoExp) + its ε-positivity + the block input + the downstream cotangent dyOut, and delegates to the per-block-type tie.