EfficientNet-B0's T3 §1a 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 the two axes 4b left open (planning/archive/proofs_tier_to_paper_nets.md, "What is NOT done, and is the honest boundary").

⭐ Axis 1 — the OPTIMIZER FORM. Every conjunct is at the RAW gradient node (*GradB), which is what efficientnet_adam_train_step.mlir and every ImageNet artifact emit; the fused op appears only in the SGD-inline file. One statement therefore covers AdamW, RMSProp, EMA, the clipped and drop-path variants and their data-parallel and bf16 twins, because they all consume this node. 4b.1's EfficientNetFoldG.lean is the fold each conjunct delegates to.

⭐ Axis 2 — the LOSS. The capstone's top-of-chain cotangent is Foundation/SmoothedLossCot.lean's, 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, which no ImageNet artifact computes. 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.

What is NOT new, and why the file is a transformation rather than a proof #

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, exactly as 4b's folds were. 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. Making it a binder is the whole of axis 2: the per-block ties are forall cot statements and were already loss-agnostic, so only the head and the capstone had to move.

⛔ Conventions carried unchanged from the fused file: batch BatchNorm (bnBatchLA), XLA-SAME at the 3x3/s2 stem and SYMMETRIC at the strided depthwises, swish (no kink, so no smoothness hypothesis anywhere), and the SE gate's fan-in folded into the block VJPs. ⛔ ONE REPLICA: in efficientnetin_emarmsdp64dropdo every gradient node feeds allReduceMeanF — the collective as an AST node since 4d piece 2 (2026-09-07), until then emitted text and a declared carve-out. Every statement here is at the per-replica node; DataParallelNode.lean composes it with the replica mean and the tail (adamW_at_allReduceMeanF). For the sync-BN data-parallel render (2026-09-21) EfficientNetSyncStepTieG.lean is the whole step: its efficientnet_net_syncTiedG says each all-reduced gradient IS this file's node at N := R·N (without drop-path and dropout).

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 (depthwiseStridedWeightSgdB, the expand-side cotangent cotEr upsamples h→2h via dStridedInB). 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 convStridedXlaWeightSgdB 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), then the batched per-row softmax-CE gradient g = rowSoftmax(logits) − onehot. The head conv params tie at the chain cotangent (loss → dense-back → GAP-back → swish/BN-back); the dense Wfc/bfc tie at the loss cotangent g directly.

@[irreducible] 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. @[irreducible] keeps the 16-deep capstone thread opaque to the elaborator (the r34/mnv2 heartbeat lesson).