The PAPER-SPEC MobileNetV2 at INFERENCE — all 17 bottlenecks, forward + graph + faithfulness #

The eval twin of MobileNetV2FullPaper.lean. That file states the seventeen-block [t,c,n,s] net at TRAINING BatchNorm, the world its VJP and its typed graph live in; this file states the same ladder at INFERENCE BatchNorm — frozen running statistics at all 52 sites, one shared ε, as the shipped mobilenetv2_fwd_eval does — and proves its typed SHlo graph denotes it — T2 at inference BatchNorm for the paper net, the graph of mobilenetv2_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.2(e).)

Pure enumeration and chaining of MobileNetV2RenderPCEval.lean's four inference stage abbreviations (ivExpandPCEval / ivDepthwisePCEval / ivDepthwiseStridedPCEval / ivProjectPCEval) and its two bodies, generic in the class count. No new mathematics and no new tokens: every BatchNorm node's den is bnPerChannelEvalTensor3, proved once.

⭐ The SSA names are the committed ones, and that is the point of this file's graph. The seventeen-block TRAINING graph names its parameters %b17gp/%b17btp, where the render emits %gp17/%btp17. This file's graph carries bnSiteP's names verbatim: %stnmu/%stnvar for the stem, %b{k}enmu, %b{k}dnmu, %b{k}pnmu and their nvar peers per block, %hnmu/%hnvar for the head, around irSig/irSigNoExp's %We{k}/%ge{k}/%bte{k}/%Wd{k}/%gd{k}/%btd{k}/%Wp{k}/%gp{k}/ %btp{k}. Names are pretty-printing metadata and do not enter den; matching them is what lets a reader diff the typed graph against the committed text line for line.

What it is tied to. mobilenetv2_fwd_eval.mlir is THIS net: 263 inputs — %x, 158 parameter tensors (paperSig at convBias := false, which is why the graph's bias slots %bs/%bd{k}/… have no argument: the render folds each conv bias into the BatchNorm that follows it) and 104 statistic slots (52 sites × μ, var) — with mobilenetv2in_fwd_eval.mlir its 1000-class twin. The classifier here is generic in nCls, so one theorem covers both.

Paper [t,c,n,s] spec (stem 3×3-s2 3→32 at the XLA-SAME phase; head 1×1 320→1280 → GAP → dense): (1, 16,1,1) (6, 24,2,2) (6, 32,3,2) (6, 64,4,2) (6, 96,3,1) (6,160,3,2) (6,320,1,1)