The FULL EfficientNet-B0 at INFERENCE — all 16 MBConv blocks, eval forward + graph + faithfulness #

The eval twin of EfficientNetFullB0.lean. That file states the sixteen-block [t,c,n,s,k] net at TRAINING BatchNorm (bnBatchLA), the world its VJP and its typed graph live in; this file states the same ladder at INFERENCE BatchNorm — frozen running statistics at all 49 sites, one shared ε, as the shipped efficientnet_fwd_eval does — and proves its typed SHlo graph denotes it — T2 at inference BatchNorm for the paper net, the graph of efficientnet_fwd_eval.mlir and its 1000-class twin. (Built 2026-09-05 so the whole-net float budget could end at a graph; the budget was deleted 2026-09-08 and the graph statement stays — planning/archive/proofs_tier_to_paper_nets.md 3.3(e).)

Pure enumeration and chaining of EfficientNetRenderPCEval.lean's per-block machinery, at the batched index N·(c·h·w) and generic in the class count. The one genuinely new piece is the fourth block shape at inference — mbExpFwdBEval / mbExpGraphBEval: expand, stride 1, no residual (ic ≠ oc; the stage-5 and stage-7 first blocks b9/b16) — which the three-block representative has no instance of and EfficientNetFullB0.lean added at training BN as mbExpFwdB.

What it is tied to. efficientnet_fwd_eval.mlir is THIS net: %x plus 213 parameters (the render folds each conv bias into the BatchNorm that follows it, so %sb/%b1db/… have no slot) plus 98 statistic slots — 312 inputs at ten classes, and efficientnetin_fwd_eval.mlir its 1000-class twin. ⚠ The typed graph below inherits the three-block eval graph's SSA names, and they differ from the artifact's in four ways, none of which enters den (names are pretty-printing metadata): the graph carries a bias slot per conv ("%sb", s!"%{p}db", …) that the render folds away; it names the statistic slots %smu/%svar, %b{k}{e,d,p}mu/var, %hmu/%hvar where the artifact has %stnmu/%stnvar, %b{k}{e,d,p}nmu/nvar, %hnmu/%hnvar; it names the SE denses zWa/zba/zWb/zbb where the artifact has zW1/zb1/zW2/zb2; and its classifier is %Wfc/%bfc where the artifact's is %Wd/%bd. The den-level statement is what the number needs; matching the text is a separate, cosmetic pass over EfficientNetRenderPCEval.lean.

B0 stage spec [t,c,n,s,k]: s1 (1,16,1,1,3) s2 (6,24,2,2,3) s3 (6,40,2,2,5) s4 (6,80,3,2,3) s5 (6,112,3,1,5) s6 (6,192,4,2,5) s7 (6,320,1,1,3); stem 3×3/s2 (3→32) at the XLA-SAME phase, head 1×1 (320→1280) → GAP → dense.