PoC: the full-16 EfficientNet-B0 train step §1a TIE (whole-net thread) — DONE (capstone efficientnet_net_tied, all 262 params, 3-axiom clean; only the optional dense-head fold below remains) #

The EfficientNet-B0 §1a tie (its batched, un-fused peer is EnetTiePoCG.efficientnet_net_tiedG). The §1 fold (EfficientNetFold) gives every batched param-SGD op den = certified ∀ cotangent; this file pins each cotangent to the actual loss-driven backward chain of the rendered net — threading the real forward activations through every param op and composing the backward cotangent from the loss down through all 16 MBConv blocks (with the residual fan-in at every stride-1 skip AND the SE gate fan-in), so each output's den = certified becomes a single composed theorem with the forward = the proven efficientnetForwardB_full.

What is NEW vs mnv2's tie (the harder content, hence a dedicated effort):

• swish masks instead of relu6 — the cotangent crosses swishBack (smooth, no two-kink selectMid) at every conv-bn-swish / depthwise-bn-swish stage.
• the SE multiplicative gate fan-in — the cotangent at an SE input is gate ⊙ dyOut (the fused seBackBatched value) and the SE dense param cotangents come from seReduceB (the gate cotangent Σ_{h,w}(x⊙dy)) threaded back through sigmoidBack → denseRowBack(W₂) → swishBack.
• true batch-norm backward (bnBatchBack) — batch-coupled, vs mnv2's per-example BN.
• EfficientNetChainClose's whole-net backward is HasVJP-composition style (vjp_comp of the per-block _has_vjp), NOT explicit cotangent-vector defs like mnv2's invresCot* — so the tie must BUILD explicit chain-cot constructors (the bulk of the remaining work).

Landed so far (all 3-axiom clean — [propext, Classical.choice, Quot.sound]) #

• All five per-block-type tie lemmas — every one of the 262 params' SGD ops denotes the certified batched Σ_n loss-descent step at the REAL loss-driven backward cotangent:

  • enet_exp_tied (16 params) — stride-1 expand block; covers the 9 residual blocks (ic=oc) AND the 2 no-skip widenings (ic≠oc, b9/b16); the param ops are skip-agnostic (the fan-in lives in the thread).
  • enet_strided_tied (16) — strided downsample (b2/4/6/12): expand at 2h×2w, strided depthwise.
  • enet_noexp_tied (12) — b1 (t=1, no expand; depthwise on ic → SE → project).
  • enet_stem_tied (4) — 3×3/s2 conv-bn-swish stem.
  • enet_head_tied (6) — 1×1 conv-bn-swish head + dense (Wfc/bfc tied at the loss cotangent g).

• The genuinely-new content vs mnv2 is PROVEN here: swish masks (swBackB), the SE gate fan-in (gateCotB=den seReduceB → sigBackB → rowDenseBackFlat → swBackB → SE dense ops), true batch-norm backward (bnBackB=bnBatchLA VJP), the strided depthwise back (dStridedInB), all at the batched index N·(c·h·w). reassocB bridges the conv/swish (oc·h·w) ↔ BN (oc·(h·w)) index. Each per-block tie is a pure delegation to the §1-fold generics EnetPoC.* at the chain cotangents.

• The whole-net thread efficientnet_net_tied (DONE, 3-axiom clean) — all 262 params tied through the REAL efficientnetForwardB_full: block inputs are its forward prefixes (a0..a16), the per-block output cotangents (dy0..dy16) composed top-down by the proven block VJPs (headFwdB_has_vjp, mb{Exp,Resid,Strided,NoExp}W_has_vjp) from the loss cotangent g. @[irreducible] *TiedAt wrappers keep the 16-deep thread opaque (the r34/mnv2 heartbeat lesson). The residual fan-in at the 9 identity skips is folded into mbResidW's own VJP (it includes the + x), so it is automatic — the whole 262-param train step is den-composed forward→loss→backward, no free activations, no symbolic cot.

Remaining (optional refinement) #

• The dense-head total-loss fold (Wfc → ∂CE/∂Wfc) — the batched-Σ_n analogue of mlp_output_total_loss_grad; today the head dense ties at the loss cotangent g directly.

Chain-cotangent helpers — the per-op batched backward steps (built fresh, HasVJP-style) #

EfficientNetChainClose proves the per-block VJPs by vjp_comp of the per-op VJPs but exposes no explicit cotangent-vector defs (unlike mnv2's invresCot*). So the tie BUILDS the chain cotangents from the proven per-op backwards: bnBackB (true-BN, the batch-coupled bnBatchLA VJP), swBackB (swish, smooth), cInB/dInB (the batched conv/depthwise input-VJP = den convBackBatched/ depthwiseBackBatched), seInB (the fused SE input-cot = den seBackBatched), gateCotB (the SE gate cotangent = den seReduceB), sigBackB, rowDenseBackFlat (the SE excite/reduce backs). Every helper IS a .backward of a proven VJP (or the exact den of the emitted backward op), so the cotangents are the genuine loss-driven backward, not a free ∀c. reassocB bridges the conv/swish index (oc·h·w) to the BN param-op index (oc·(h·w)).

Residual stride-1 MBConv block — all 16 params tied (expand → dw → SE → project + skip) #

The centerpiece: exercises the genuinely-new content vs mnv2 — swish masks (smooth), the SE gate fan-in (gateCotB → sigBackB → {zW₂,zb₂} → rowDenseBackFlat → swBackB → {zW₁,zb₁}), and true batch-norm backward (bnBackB), all at the batched index N·(c·h·w). Backward from dyOut (cot at project-BN out): project-BN-back → project-conv-back (cot at SE out) → SE backward (fused dx for the depthwise side; un-fused gate-cot for the SE params) → depthwise swish/BN/conv backs → expand swish/BN/conv backs. Residual (ic=oc=c): the block-input cotangent fan-in + dyOut lives in the whole-net thread, not here (the param ops are skip-agnostic — identical to the no-skip widenings).

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).

The whole-net thread — all 262 params tied through the REAL efficientnetForwardB_full #

The capstone: efficientnetForwardB_full's prefixes are the block inputs (a0..a16 = stem, then the 16 MBConv blocks), and the per-block output cotangents (dy0..dy16) are composed TOP-DOWN by the proven block VJPs (headFwdB_has_vjp, mb{Exp,Resid,Strided,NoExp}W_has_vjp) from the loss cotangent g = rowSoftmax(logits) − onehot. Each block's tie then holds at its real input + threaded dyOut. The full §1a tie: the WHOLE 16-MBConv (262-param) EfficientNet-B0 train step is den-composed forward→loss→backward, no free activations, no symbolic cotangent. The residual fan-in at the 9 identity skips is folded into mbResidW's own VJP (it includes the + x), so it is automatic.