The BATCHED EfficientNet-B0 block forwards and graphs (true batch-norm, matches the render) #

The EfficientNet peer of MobileNetV2StagesPC. EfficientNet's render (EfficientNetRender.Basic) emits true batch-norm (reduce μ/var over the batch+spatial axes [0,2,3] per channel — bnBatchTensor4), which couples the batch. So the forward graph here lives at the batched index N·(c·h·w) (StableHLO.batchOp/StableHLO.bnBatchF, StableHLO.Basic):

• every batch-separable op (conv / strided conv / depthwise / strided depthwise / dense / GAP / the whole SE block) is batchMap N of the proven per-example op (SHlo.batchOp + BatchableOp/denOp);
• swish is the batched pointwise descriptor (.batchOp .swish, denoting the flat swishF by den_batchOp_swish_eq_swishF) and the residual add is .addVB — the tokens the render emits, so pretty of each block graph is the rendered block's text (Codegen/FwdGraphTextTies), names included: SE denses zW1/zb1/zW2/zb2, conv biases biasName false, classifier %Wd/%bd;
• the one batch-coupled op, true batch-norm, is SHlo.bnBatchF, denoting bnBatchLA (= the proven bnBatchTensor4, reindexed to the network's left-assoc N·(oc·h·w) flat layout).

This file proves the FORWARD half — den (graph) = forward — for the stride-2 stem conv-bn-swish (stemGraphB_faithful), an MBConv1 (t=1, no expand) SE block (mbNoExpGraphB_faithful), an MBConv6 expand SE block with a stride-2 downsample (mbStridedGraphB_faithful), an MBConv6 expand SE block with an identity residual skip (mbResidGraphB_faithful), and the 1×1 conv-bn-swish head, GAP and the dense classifier (headGraphB_faithful) — all with true batch-norm and the squeeze-excite gate (seBlockFull, entering as BatchableOp.seBlock = batchMap N seBlockFull). B0's fifth block form, the stride-1 expand block with no skip, is mbExpGraphB_faithful in EfficientNetFullB0. Faithfulness is per-block (*GraphB_faithful: den (block graph) = block forward (den input)), so EfficientNetFullB0 chains the sixteen-block net without the kernel reducing it at once. All five theorems are in tests/AuditAxioms.lean's #print axioms list.