The paper-spec MobileNetV2 at inference — all 17 bottlenecks, forward + graph + faithfulness #

The inference twin of MobileNetV2FullB.lean, the batch-BatchNorm training forward. This file states the same seventeen-block [t,c,n,s] ladder at inference BatchNorm — frozen running statistics at all 52 sites, one shared ε, as mobilenetv2_fwd_eval does (mobilenetv2ForwardPaperEval) — and proves its typed SHlo graph denotes it (mobilenetv2FwdGraphPaperEval_faithful). Both are stated for one example (x : Vec (3 * 224 * 224)); frozen-statistics BatchNorm does not couple examples. The block weight records are IVWEval / IVWNoExpEval below; the training records IVW / IVWNoExp are MobileNetV2FullPaper.lean's.

Pure enumeration and chaining of MobileNetV2StagesPCEval.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 eval render's. The training graph (MobileNetV2FullB) names its parameters %b{k}{e,d,p}{W,g,bt}, as the train-step render does. The eval render uses other names, and this file's graph carries them verbatim: bnEvalSite's %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}, and every conv bias as %zb{c}, the zero constant the render binds it to at convBias := false. Names are pretty-printing metadata and do not enter den. FwdGraphTextTies checks the render's stem, head and one block of each kind against this file's graphs, byte for byte.

Per example, and the artifact is batched. The render writes this graph's own per-example constructors, printed at the artifact's batch B (mnv2FwdChain): each op takes a leading batch dimension and none reduces across it — frozen-statistics BatchNorm reads its μ, σ² as inputs, and the one reduction is the GAP over [2, 3], which FwdGraphTextTies also checks over the whole rendered module. So the artifact computes this forward at every example of its batch.

What it is tied to. mobilenetv2_fwd_eval.mlir: 263 inputs — %x, 158 parameter tensors (paperSig at convBias := false, so no bias slot has an argument: the render binds each conv bias to the %zb{c} zero constant) and 104 statistic slots (52 sites × μ, var) — with mobilenetv2in_fwd_eval.mlir and mobilenetv2in_fwd_eval_eps0001.mlir its 1000-class twins. The classifier here is generic in nCls and ε is a binder, so one theorem covers all three.

The artifacts are the zero-bias instance. IVWEval / IVWNoExpEval and the stem and head carry a conv-bias field per conv site, which den reads, while the graph spells each one as %zb{c}. So the three artifacts are the instance with every conv bias 0. At inference BatchNorm a conv bias does not cancel as it does under batch BN, so this is a restriction, not a reparametrisation.

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)