Item A — the PER-CHANNEL-BN MobileNetV2 forward graph (matches the render)

planning/archive/mobilenetv2_close.md Item A. StableHLO.lean already has the full strided MobileNetV2 forward graph mobilenetv2FwdGraphFull + mobilenetv2FwdGraphFull_faithful — but those use scalar bnF (one γ/β over the whole c·h·w), tied to the scalar ℝ-forward mobilenetv2Forward_full. The operational render (tests/TestMobilenetV2Train.lean, the bnPC block) emits per-channel BN (reduce over spatial [2,3], γ/β : Vec c). So neither existing graph is a faithful "render of a proven graph": they compute a different function than the render.

This file closes that gap — the per-channel-BN twin of mobilenetv2FwdGraphFull:

• mobilenetv2Forward_full_pc — the ℝ-forward with bnPerChannelTensor3 (per-channel, γ/β : Vec c) at every BN site, same topology/stride schedule/relu6 placement as mobilenetv2Forward_full. Built from per-channel stage abbreviations ivExpandPC/ivDepthwisePC/ivDepthwiseStridedPC/ivProjectPC (per-channel mirrors of ivExpand/…/ivProject).
• mobilenetv2FwdGraphFullPC — the typed SHlo forward graph using bnPerChannelF tokens.
• mobilenetv2FwdGraphFullPC_faithful — den (graph) = mobilenetv2Forward_full_pc, via bnPerChannelF_faithful (den (bnPerChannelF …) = bnPerChannelTensor3 …, an rfl lemma). Same simp-then-unfold recipe as mobilenetv2FwdGraphFull_faithful.

This is the prerequisite for the structured render (Item B): now MobileNetV2 has a proven per-channel forward graph whose pretty matches the render's forward text. Everything closes 3-axiom-clean (tests/AuditAxioms.lean). Stride-2 flatConvStridedF/depthwiseStridedF (4 downsampling blocks) and the residual addV skip (b2/b4) are all assembled here, not just exercised at the op level.

@[reducible]

noncomputable def Proofs.ivExpandPC {ic mid h w kHe kWe : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) : Vec (ic * h * w) → Vec (mid * h * w)

Expand stage, per-channel BN: relu6 ∘ bnPC ∘ conv(1×1).

Equations

• Proofs.ivExpandPC We be εe γe βe = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εe γe βe ∘ Proofs.flatConv We be

@[reducible]

noncomputable def Proofs.ivDepthwisePC {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) : Vec (mid * h * w) → Vec (mid * h * w)

Depthwise stage (stride-1), per-channel BN: relu6 ∘ bnPC ∘ depthwise.

Equations

• Proofs.ivDepthwisePC Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εd γd βd ∘ Proofs.depthwiseFlat Wd bd

@[reducible]

noncomputable def Proofs.ivDepthwiseStridedPC {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) : Vec (mid * (2 * h) * (2 * w)) → Vec (mid * h * w)

Depthwise stage (stride-2 downsample), per-channel BN: relu6 ∘ bnPC ∘ depthwiseStrided.

Equations

• Proofs.ivDepthwiseStridedPC Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelTensor3 mid h w εd γd βd ∘ Proofs.depthwiseStride2FlatXla Wd bd

@[reducible]

noncomputable def Proofs.ivProjectPC {mid oc h w kHp kWp : ℕ} (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) : Vec (mid * h * w) → Vec (oc * h * w)

Project (linear bottleneck) stage, per-channel BN: bnPC ∘ conv(1×1) (no relu6).

Equations

• Proofs.ivProjectPC Wp bp εp γp βp = Proofs.bnPerChannelTensor3 oc h w εp γp βp ∘ Proofs.flatConv Wp bp

@[reducible]

noncomputable def Proofs.invresBodyPC {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) : Vec (ic * h * w) → Vec (oc * h * w)

Inverted-residual body (stride-1), per-channel BN: project ∘ depthwise ∘ expand.

Equations

• Proofs.invresBodyPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProjectPC Wp bp εp γp βp ∘ Proofs.ivDepthwisePC Wd bd εd γd βd ∘ Proofs.ivExpandPC We be εe γe βe

@[reducible]

noncomputable def Proofs.invresBodyStridedPC {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Inverted-residual body (stride-2 downsample), per-channel BN: expand SAME (at 2h×2w) → depthwise-strided → project.

Equations

• Proofs.invresBodyStridedPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProjectPC Wp bp εp γp βp ∘ Proofs.ivDepthwiseStridedPC Wd bd εd γd βd ∘ Proofs.ivExpandPC We be εe γe βe

noncomputable def Proofs.mobilenetv2Forward_full_pc (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs : ℝ) (γs βs : Vec 16) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 : ℝ) (γe1 βe1 : Vec 64) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 : ℝ) (γd1 βd1 : Vec 64) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 : ℝ) (γp1 βp1 : Vec 24) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 : ℝ) (γe2 βe2 : Vec 96) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 : ℝ) (γd2 βd2 : Vec 96) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 : ℝ) (γp2 βp2 : Vec 24) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 : ℝ) (γe3 βe3 : Vec 96) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 : ℝ) (γd3 βd3 : Vec 96) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 : ℝ) (γp3 βp3 : Vec 32) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 : ℝ) (γe4 βe4 : Vec 128) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 : ℝ) (γd4 βd4 : Vec 128) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 : ℝ) (γp4 βp4 : Vec 32) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 : ℝ) (γe5 βe5 : Vec 128) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 : ℝ) (γd5 βd5 : Vec 128) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 : ℝ) (γp5 βp5 : Vec 64) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 : ℝ) (γe6 βe6 : Vec 256) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 : ℝ) (γd6 βd6 : Vec 256) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 : ℝ) (γp6 βp6 : Vec 64) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh : ℝ) (γh βh : Vec 128) (Wfc : Mat 128 10) (bfc : Vec 10) : Vec (3 * 224 * 224) → Vec 10

The full MobileNetV2 forward with per-channel BN (ch7 render): strided stem (224→112) → 6 inverted-residual blocks (b1/b3/b5/b6 stride-2 downsample, b2/b4 stride-1 skip) → 1×1 conv-bn-relu6 head → global-avg-pool → dense. Per-channel-BN twin of mobilenetv2Forward_full; matches the operational render's BN flavor.

Equations

• One or more equations did not get rendered due to their size.

def Proofs.StableHLO.mobilenetv2FwdGraphFullPC (epsStr : String) (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs : ℝ) (γs βs : Vec 16) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 : ℝ) (γe1 βe1 : Vec 64) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 : ℝ) (γd1 βd1 : Vec 64) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 : ℝ) (γp1 βp1 : Vec 24) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 : ℝ) (γe2 βe2 : Vec 96) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 : ℝ) (γd2 βd2 : Vec 96) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 : ℝ) (γp2 βp2 : Vec 24) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 : ℝ) (γe3 βe3 : Vec 96) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 : ℝ) (γd3 βd3 : Vec 96) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 : ℝ) (γp3 βp3 : Vec 32) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 : ℝ) (γe4 βe4 : Vec 128) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 : ℝ) (γd4 βd4 : Vec 128) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 : ℝ) (γp4 βp4 : Vec 32) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 : ℝ) (γe5 βe5 : Vec 128) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 : ℝ) (γd5 βd5 : Vec 128) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 : ℝ) (γp5 βp5 : Vec 64) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 : ℝ) (γe6 βe6 : Vec 256) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 : ℝ) (γd6 βd6 : Vec 256) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 : ℝ) (γp6 βp6 : Vec 64) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh : ℝ) (γh βh : Vec 128) (Wfc : Mat 128 10) (bfc : Vec 10) (x : Vec (3 * 224 * 224)) : SHlo 10

Whole per-channel-BN MobileNetV2 forward graph at the full ch7 render dims (3×224² → 7×7×64): strided stem (flatConvStridedF, 224→112) → 6 inverted-residual blocks (b1/b3/b5/b6 stride-2 downsample via depthwiseStridedF, b2/b4 stride-1 SAME with an addV skip) → 1×1 conv-bn-relu6 head → global-avg-pool → dense. Per-channel BN (bnPerChannelF, γ/β : Vec c) at every BN site — matches the operational render. The per-channel twin of mobilenetv2FwdGraphFull.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.mobilenetv2FwdGraphFullPC_faithful (epsStr : String) (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs : ℝ) (γs βs : Vec 16) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 : ℝ) (γe1 βe1 : Vec 64) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 : ℝ) (γd1 βd1 : Vec 64) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 : ℝ) (γp1 βp1 : Vec 24) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 : ℝ) (γe2 βe2 : Vec 96) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 : ℝ) (γd2 βd2 : Vec 96) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 : ℝ) (γp2 βp2 : Vec 24) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 : ℝ) (γe3 βe3 : Vec 96) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 : ℝ) (γd3 βd3 : Vec 96) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 : ℝ) (γp3 βp3 : Vec 32) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 : ℝ) (γe4 βe4 : Vec 128) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 : ℝ) (γd4 βd4 : Vec 128) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 : ℝ) (γp4 βp4 : Vec 32) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 : ℝ) (γe5 βe5 : Vec 128) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 : ℝ) (γd5 βd5 : Vec 128) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 : ℝ) (γp5 βp5 : Vec 64) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 : ℝ) (γe6 βe6 : Vec 256) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 : ℝ) (γd6 βd6 : Vec 256) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 : ℝ) (γp6 βp6 : Vec 64) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh : ℝ) (γh βh : Vec 128) (Wfc : Mat 128 10) (bfc : Vec 10) (x : Vec (3 * 224 * 224)) : den (mobilenetv2FwdGraphFullPC epsStr Ws bs εs γs βs We1 be1 εe1 γe1 βe1 Wd1 bd1 εd1 γd1 βd1 Wp1 bp1 εp1 γp1 βp1 We2 be2 εe2 γe2 βe2 Wd2 bd2 εd2 γd2 βd2 Wp2 bp2 εp2 γp2 βp2 We3 be3 εe3 γe3 βe3 Wd3 bd3 εd3 γd3 βd3 Wp3 bp3 εp3 γp3 βp3 We4 be4 εe4 γe4 βe4 Wd4 bd4 εd4 γd4 βd4 Wp4 bp4 εp4 γp4 βp4 We5 be5 εe5 γe5 βe5 Wd5 bd5 εd5 γd5 βd5 Wp5 bp5 εp5 γp5 βp5 We6 be6 εe6 γe6 βe6 Wd6 bd6 εd6 γd6 βd6 Wp6 bp6 εp6 γp6 βp6 Wh bh εh γh βh Wfc bfc x) = mobilenetv2Forward_full_pc Ws bs εs γs βs We1 be1 εe1 γe1 βe1 Wd1 bd1 εd1 γd1 βd1 Wp1 bp1 εp1 γp1 βp1 We2 be2 εe2 γe2 βe2 Wd2 bd2 εd2 γd2 βd2 Wp2 bp2 εp2 γp2 βp2 We3 be3 εe3 γe3 βe3 Wd3 bd3 εd3 γd3 βd3 Wp3 bp3 εp3 γp3 βp3 We4 be4 εe4 γe4 βe4 Wd4 bd4 εd4 γd4 βd4 Wp4 bp4 εp4 γp4 βp4 We5 be5 εe5 γe5 βe5 Wd5 bd5 εd5 γd5 βd5 Wp5 bp5 εp5 γp5 βp5 We6 be6 εe6 γe6 βe6 Wd6 bd6 εd6 γd6 βd6 Wp6 bp6 εp6 γp6 βp6 Wh bh εh γh βh Wfc bfc x

Full per-channel-BN MobileNetV2 forward faithfulness. The per-channel strided render graph denotes the proven mobilenetv2Forward_full_pc. simp-based (like mobilenetv2FwdGraphFull_faithful, so it avoids the concrete-dim isDefEq wall), with bnPerChannelF_faithful replacing bnF_faithful. This is the "text = render of a proven graph" forward half at the render's BN flavor.