Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV4ParamGrad

MobileNetV4-Conv-M — every parameter gradient node IS the loss's derivative in that parameter #

mnv4_net_tiedB says each of the 233 parameter gradient nodes denotes its layer's parameter Jacobian contracted with the cotangent the emitted backward chain threads to it, from a loss cotangent g; the *CotIn_eq_vjp lemmas say each block's input cotangent is its CertLayer's certified backward. mnv4_net_lossGrad composes them: for any loss L of the logits whose gradient at the net's output is g, every node is ∂L/∂θ of the WHOLE net with that one parameter varied. mnv4_net_lossGrad_smoothedCE discharges hL for the label-smoothed loss the artifacts ship.

How. ResNet50ParamGrad's shape, with two things MNv4 adds:

The depthwise slots. A UIB body's pre- and post-depthwise are if k = 0 then id' else … layers read off the row, and the depthwise weights live in a DWSlot that is a DWBnParams only at k > 0. So each family bundle (mnv4ExtraDWLossTiedB, mnv4ConvNeXtLossTiedB, mnv4FfnLossTiedB, mnv4StridedLossTiedB) takes its row's k ≠ 0 / k = 0 facts, the slots' forwards reduce by mnv4PreDWSlot_fwd_of_ne_zero and friends, and a depthwise parameter is varied through UibParams.withPre / withPost (the slot record with one field replaced).
The layer-group trunk. The forward nests the five resolution groups, not the 21 blocks, so each block's factor lemma peels its group with CertLayer.comp_fwd_apply, and mnv4Pre{k} meets mnv4Blk{k} at the group boundaries (mnv4Pre2_eq_blk …). At the net's literal widths these checks stay cheap because every peel is a named rewrite, never an unfolding.

Hypotheses. Mnv4SmoothAt (every relu off its kink at the real activations — the stem's clause and each group's .ok); the BN ε > 0 facts live in the weights. For the smoothed loss, every example's target summing to one and 0 < nCls.

def Proofs.StableHLO.UibParams.withPre {s : UibSpec} (p : UibParams s) (q : DWBnParams s.ic s.preDWk) :

The record with its pre-depthwise slot's parameters replaced.

Equations

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

Instances For

def Proofs.StableHLO.UibParams.withPost {s : UibSpec} (p : UibParams s) (q : DWBnParams (s.ic * s.expand) s.postDWk) :

The record with its post-depthwise slot's parameters replaced.

Equations

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

Instances For

theorem Proofs.StableHLO.UibParams.withPre_pre_params {s : UibSpec} (p : UibParams s) (q : DWBnParams s.ic s.preDWk) (hk : s.preDWk ≠ 0) :

(p.withPre q).pre.params = q

theorem Proofs.StableHLO.UibParams.withPost_post_params {s : UibSpec} (p : UibParams s) (q : DWBnParams (s.ic * s.expand) s.postDWk) (hk : s.postDWk ≠ 0) :

(p.withPost q).post.params = q

theorem Proofs.Mnv4TieB.mnv4PreDWSlot_fwd_of_ne_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k ≠ 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) :

(StableHLO.mnv4PreDWSlot N k W b ε hε γ β).fwd = StableHLO.dwbB N W b ε γ β

theorem Proofs.Mnv4TieB.mnv4PreDWSlot_fwd_of_eq_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k = 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) :

(StableHLO.mnv4PreDWSlot N k W b ε hε γ β).fwd = fun (y : Vec (N * (c * h * w))) => y

theorem Proofs.Mnv4TieB.mnv4PostDWSlot_fwd_of_ne_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k ≠ 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) :

(StableHLO.mnv4PostDWSlot N k W b ε hε γ β).fwd = StableHLO.dwbReluB N W b ε γ β

theorem Proofs.Mnv4TieB.mnv4PostDWSlot_fwd_of_eq_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k = 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) :

(StableHLO.mnv4PostDWSlot N k W b ε hε γ β).fwd = fun (y : Vec (N * (c * h * w))) => y

theorem Proofs.Mnv4TieB.mnv4PreDWSlot_fwd_apply_of_ne_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k ≠ 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) :

(StableHLO.mnv4PreDWSlot N k W b ε hε γ β).fwd x = StableHLO.dwbB N W b ε γ β x

theorem Proofs.Mnv4TieB.mnv4PreDWSlot_fwd_apply_of_eq_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k = 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) :

(StableHLO.mnv4PreDWSlot N k W b ε hε γ β).fwd x = x

theorem Proofs.Mnv4TieB.mnv4PostDWSlot_fwd_apply_of_ne_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k ≠ 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) :

(StableHLO.mnv4PostDWSlot N k W b ε hε γ β).fwd x = StableHLO.dwbReluB N W b ε γ β x

theorem Proofs.Mnv4TieB.mnv4PostDWSlot_fwd_apply_of_eq_zero (N : ℕ) {c h w kH kW k : ℕ} (hk : k = 0) (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) :

(StableHLO.mnv4PostDWSlot N k W b ε hε γ β).fwd x = x

theorem Proofs.Mnv4TieB.hasGradAt_cast {n m : ℕ} (e : n = m) (x : Vec n) {G : Vec m → Vec 1} {dy : Vec m} (hG : HasGradAt G (fun (j : Fin m) => x (Fin.cast ⋯ j)) dy) :

HasGradAt (fun (u : Vec n) => G fun (j : Fin m) => u (Fin.cast ⋯ j)) x fun (i : Fin n) => dy (Fin.cast e i)

Back through the head's [N, c] ↔ [N, c, 1, 1] relabelling: the cotangent is read back along the same cast.

def Proofs.Mnv4TieB.mnv4StemLossTiedB {N h w ic oc kH kW : ℕ} (xN cotN vN epsStr : String) (Ws : Kernel4 oc ic kH kW) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (Φ : Kernel4 oc ic kH kW → Vec oc → Vec oc → Vec 1) (dy : Vec (N * (oc * h * w))) :

Stem, every parameter node a loss derivative — the three nodes mnv4StemTiedB ties, Φ the loss as a function of the stem's (W, γ, β).

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_stem_lossTiedB {N h w ic oc kH kW : ℕ} (xN cotN vN epsStr : String) (Ws : Kernel4 oc ic kH kW) (bs : Vec oc) (εs : ℝ) (hεs : 0 < εs) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : StableHLO.Mnv4StemSmoothAtB N h w Ws bs εs γs βs x) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (StableHLO.mnv4StemB N h w Ws bs εs γs βs x) dy) {Φ : Kernel4 oc ic kH kW → Vec oc → Vec oc → Vec 1} (hΦ : ∀ (W : Kernel4 oc ic kH kW) (γ β : Vec oc), Φ W γ β = Gn (StableHLO.mnv4StemB N h w W bs εs γ β x)) :

mnv4StemLossTiedB xN cotN vN epsStr Ws bs εs γs βs x Φ dy

def Proofs.Mnv4TieB.mnv4FusedLossTiedB {N h w ic mid oc kH kW : ℕ} (Wc : Kernel4 mid ic kH kW) (bc : Vec mid) (εc : ℝ) (γc βc : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (xN cotN vN epsStr : String) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) (Φ : Kernel4 mid ic kH kW → Vec mid → Vec mid → Kernel4 oc mid 1 1 → Vec oc → Vec oc → Vec 1) (dyF : Vec (N * (oc * h * w))) :

Fused stage, every parameter node a loss derivative — the six nodes mnv4FusedTiedB ties, Φ the loss as a function of (Wc, γc, βc, Wp, γp, βp).

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_fused_lossTiedB {N h w ic mid oc kH kW : ℕ} (Wc : Kernel4 mid ic kH kW) (bc : Vec mid) (εc : ℝ) (hεc : 0 < εc) (γc βc : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (xN cotN vN epsStr : String) (xin : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : ∀ (k : Fin (N * (mid * h * w))), StableHLO.bnBatchLA N mid h w εc γc βc (StableHLO.batchMap N (flatConvStride2 Wc bc) xin) k ≠ 0) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (projB N Wp bp εp γp βp (StableHLO.cbReluStridedB N Wc bc εc γc βc xin)) dy) {Φ : Kernel4 mid ic kH kW → Vec mid → Vec mid → Kernel4 oc mid 1 1 → Vec oc → Vec oc → Vec 1} (hΦ : ∀ (W1 : Kernel4 mid ic kH kW) (γ1 β1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (γ2 β2 : Vec oc), Φ W1 γ1 β1 W2 γ2 β2 = Gn (projB N W2 bp εp γ2 β2 (StableHLO.cbReluStridedB N W1 bc εc γ1 β1 xin))) :

mnv4FusedLossTiedB Wc bc εc γc βc Wp bp εp γp βp xN cotN vN epsStr xin Φ dy

noncomputable def Proofs.Mnv4TieB.mnv4HeadFwd {c mid oc nCls : ℕ} (N h w : ℕ) (W1 : Kernel4 mid c 1 1) (b1 : Vec mid) (ε1 : ℝ) (γ1 β1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 : Vec oc) (ε2 : ℝ) (γ2 β2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) (xin : Vec (N * (c * h * w))) :

Vec (N * nCls)

The head as one plain function of its eight trained parameters (the ε's and conv biases held at the given values): mnv4Head's forward.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4Head_fwd {N h w c mid oc nCls : ℕ} (W1 : Kernel4 mid c 1 1) (b1 : Vec mid) (ε1 : ℝ) (hε1 : 0 < ε1) (γ1 β1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 : Vec oc) (ε2 : ℝ) (hε2 : 0 < ε2) (γ2 β2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) (xin : Vec (N * (c * h * w))) :

(StableHLO.mnv4Head N (StableHLO.cbReluLayer N W1 b1 ε1 hε1 γ1 β1) (StableHLO.gapLayer N) (StableHLO.cbReluLayer N W2 b2 ε2 hε2 γ2 β2) (StableHLO.denseLayer N Wd bd)).fwd xin = mnv4HeadFwd N h w W1 b1 ε1 γ1 β1 W2 b2 ε2 γ2 β2 Wd bd xin

def Proofs.Mnv4TieB.mnv4HeadLossTiedB {N h w c mid oc nCls : ℕ} (W1 : Kernel4 mid c 1 1) (b1 : Vec mid) (ε1 : ℝ) (γ1 β1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 : Vec oc) (ε2 : ℝ) (γ2 β2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) (xN cotN vN epsStr : String) (xin : Vec (N * (c * h * w))) (Φ : Kernel4 mid c 1 1 → Vec mid → Vec mid → Kernel4 oc mid 1 1 → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1) (g : Vec (N * nCls)) :

Head, every parameter node a loss derivative — the eight nodes mnv4HeadTiedB ties, Φ the loss as a function of (W1, γ1, β1, W2, γ2, β2, Wd, bd).

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_head_lossTiedB {N h w c mid oc nCls : ℕ} (W1 : Kernel4 mid c 1 1) (b1 : Vec mid) (ε1 : ℝ) (hε1 : 0 < ε1) (γ1 β1 : Vec mid) (W2 : Kernel4 oc mid 1 1) (b2 : Vec oc) (ε2 : ℝ) (hε2 : 0 < ε2) (γ2 β2 : Vec oc) (Wd : Mat oc nCls) (bd : Vec nCls) (xN cotN vN epsStr : String) (xin : Vec (N * (c * h * w))) (hs1 : ∀ (k : Fin (N * (mid * h * w))), StableHLO.bnBatchLA N mid h w ε1 γ1 β1 (StableHLO.batchMap N (flatConv W1 b1) xin) k ≠ 0) (hs2 : ∀ (k : Fin (N * (oc * 1 * 1))), StableHLO.bnBatchLA N oc 1 1 ε2 γ2 β2 (StableHLO.batchMap N (flatConv W2 b2) (mnv4HeadPool N h w W1 b1 ε1 γ1 β1 xin)) k ≠ 0) {L : Vec (N * nCls) → Vec 1} {g : Vec (N * nCls)} (hL : HasGradAt L (mnv4HeadFwd N h w W1 b1 ε1 γ1 β1 W2 b2 ε2 γ2 β2 Wd bd xin) g) {Φ : Kernel4 mid c 1 1 → Vec mid → Vec mid → Kernel4 oc mid 1 1 → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1} (hΦ : ∀ (W1' : Kernel4 mid c 1 1) (γ1' β1' : Vec mid) (W2' : Kernel4 oc mid 1 1) (γ2' β2' : Vec oc) (Wd' : Mat oc nCls) (bd' : Vec nCls), Φ W1' γ1' β1' W2' γ2' β2' Wd' bd' = L (mnv4HeadFwd N h w W1' b1 ε1 γ1' β1' W2' b2 ε2 γ2' β2' Wd' bd' xin)) :

mnv4HeadLossTiedB W1 b1 ε1 γ1 β1 W2 b2 ε2 γ2 β2 Wd bd xN cotN vN epsStr xin Φ g

def Proofs.Mnv4TieB.mnv4ExtraDWLossTiedB (N : ℕ) (s : StableHLO.UibSpec) (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (xin : Vec (N * (s.ic * s.h * s.h))) (Φ : StableHLO.UibParams s → Vec 1) (dyOut : Vec (N * (s.oc * s.h * s.h))) :

ExtraDW body, every parameter node a loss derivative — the twelve nodes mnv4ExtraDWTiedB ties, Φ the loss at the body output as a function of the row's weight record. A depthwise slot's parameter is varied through withPre / withPost.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_extradw_lossTiedB {N : ℕ} {s : StableHLO.UibSpec} (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (hq0 : s.preDWk ≠ 0) (hd0 : s.postDWk ≠ 0) (v : Vec (N * (s.ic * s.h * s.h))) (hok : (StableHLO.mnv4BodyOfRow N s p).ok v) {Gb : Vec (N * (s.oc * s.h * s.h)) → Vec 1} {dy : Vec (N * (s.oc * s.h * s.h))} (hGb : HasGradAt Gb ((StableHLO.mnv4BodyOfRow N s p).fwd v) dy) {Φ : StableHLO.UibParams s → Vec 1} (hΦ : ∀ (p' : StableHLO.UibParams s), Φ p' = Gb ((StableHLO.mnv4BodyOfRow N s p').fwd v)) :

mnv4ExtraDWLossTiedB N s xN cotN vN epsStr p v Φ dy

def Proofs.Mnv4TieB.mnv4ConvNeXtLossTiedB (N : ℕ) (s : StableHLO.UibSpec) (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (xin : Vec (N * (s.ic * s.h * s.h))) (Φ : StableHLO.UibParams s → Vec 1) (dyOut : Vec (N * (s.oc * s.h * s.h))) :

ConvNeXt-like body, every parameter node a loss derivative — the nine nodes mnv4ConvNeXtTiedB ties.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_convnext_lossTiedB {N : ℕ} {s : StableHLO.UibSpec} (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (hq0 : s.preDWk ≠ 0) (hd0 : s.postDWk = 0) (v : Vec (N * (s.ic * s.h * s.h))) (hok : (StableHLO.mnv4BodyOfRow N s p).ok v) {Gb : Vec (N * (s.oc * s.h * s.h)) → Vec 1} {dy : Vec (N * (s.oc * s.h * s.h))} (hGb : HasGradAt Gb ((StableHLO.mnv4BodyOfRow N s p).fwd v) dy) {Φ : StableHLO.UibParams s → Vec 1} (hΦ : ∀ (p' : StableHLO.UibParams s), Φ p' = Gb ((StableHLO.mnv4BodyOfRow N s p').fwd v)) :

mnv4ConvNeXtLossTiedB N s xN cotN vN epsStr p v Φ dy

def Proofs.Mnv4TieB.mnv4FfnLossTiedB (N : ℕ) (s : StableHLO.UibSpec) (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (xin : Vec (N * (s.ic * s.h * s.h))) (Φ : StableHLO.UibParams s → Vec 1) (dyOut : Vec (N * (s.oc * s.h * s.h))) :

FFN body, every parameter node a loss derivative — the six nodes mnv4FfnTiedB ties.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_ffn_lossTiedB {N : ℕ} {s : StableHLO.UibSpec} (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (hq0 : s.preDWk = 0) (hd0 : s.postDWk = 0) (v : Vec (N * (s.ic * s.h * s.h))) (hok : (StableHLO.mnv4BodyOfRow N s p).ok v) {Gb : Vec (N * (s.oc * s.h * s.h)) → Vec 1} {dy : Vec (N * (s.oc * s.h * s.h))} (hGb : HasGradAt Gb ((StableHLO.mnv4BodyOfRow N s p).fwd v) dy) {Φ : StableHLO.UibParams s → Vec 1} (hΦ : ∀ (p' : StableHLO.UibParams s), Φ p' = Gb ((StableHLO.mnv4BodyOfRow N s p').fwd v)) :

mnv4FfnLossTiedB N s xN cotN vN epsStr p v Φ dy

def Proofs.Mnv4TieB.mnv4StridedLossTiedB (N : ℕ) (s : StableHLO.UibSpec) (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (xin : Vec (N * (s.ic * (2 * s.h) * (2 * s.h)))) (Φ : StableHLO.UibParams s → Vec 1) (dyOut : Vec (N * (s.oc * s.h * s.h))) :

Strided body, every parameter node a loss derivative — the twelve nodes mnv4StridedTiedB ties; the post-DW is the symmetric strided depthwise.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_strided_lossTiedB {N : ℕ} {s : StableHLO.UibSpec} (xN cotN vN epsStr : String) (p : StableHLO.UibParams s) (hq0 : s.preDWk ≠ 0) (hd0 : s.postDWk ≠ 0) (v : Vec (N * (s.ic * (2 * s.h) * (2 * s.h)))) (hok : (StableHLO.mnv4StridedBodyOfRow N s p).ok v) {Gn : Vec (N * (s.oc * s.h * s.h)) → Vec 1} {dy : Vec (N * (s.oc * s.h * s.h))} (hGn : HasGradAt Gn ((StableHLO.mnv4StridedBodyOfRow N s p).fwd v) dy) {Φ : StableHLO.UibParams s → Vec 1} (hΦ : ∀ (p' : StableHLO.UibParams s), Φ p' = Gn ((StableHLO.mnv4StridedBodyOfRow N s p').fwd v)) :

mnv4StridedLossTiedB N s xN cotN vN epsStr p v Φ dy

theorem Proofs.Mnv4TieB.certLayer_hasGradAt_comp {m n : ℕ} (L : StableHLO.CertLayer m n) (x : Vec m) (hx : L.ok x) {G : Vec n → Vec 1} {dy : Vec n} (hG : HasGradAt G (L.fwd x) dy) :

HasGradAt (fun (y : Vec m) => G (L.fwd y)) x ((L.vjp x hx).backward dy)

Pull a gradient back through any certified layer, at a point it certifies.

theorem Proofs.Mnv4TieB.mnv4Skip_hasGradAt_comp {N n : ℕ} (L : StableHLO.CertLayer (N * n) (N * n)) (v : Vec (N * n)) (hok : L.ok v) {G : Vec (N * n) → Vec 1} {dy bodyDx : Vec (N * n)} (hdx : bodyDx = (L.vjp v hok).backward dy) (hG : HasGradAt G (L.residual.fwd v) dy) :

HasGradAt (fun (y : Vec (N * n)) => G (L.residual.fwd y)) v (mnv4SkipCotIn bodyDx dy)

A skip block's step: the emitted fan-in body dx + dyOut is the residual layer's backward.

theorem Proofs.Mnv4TieB.mnv4_residual_body_hasGradAt {N n : ℕ} (L : StableHLO.CertLayer (N * n) (N * n)) (v : Vec (N * n)) {G : Vec (N * n) → Vec 1} {dy : Vec (N * n)} (hG : HasGradAt G (L.residual.fwd v) dy) :

HasGradAt (fun (u : Vec (N * n)) => G fun (i : Fin (N * n)) => u i + v i) (L.fwd v) dy

At a skip block the loss read at the BODY output is u ↦ G (u + v): the skip is a constant once a body parameter varies, so its gradient there is still the block-output cotangent.

theorem Proofs.Mnv4TieB.mnv4Pre2_eq_blk (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre2 N w x = mnv4Blk2 N w x

The group prefixes meet the block prefixes at every group boundary.

theorem Proofs.Mnv4TieB.mnv4Pre3_eq_blk (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre3 N w x = mnv4Blk6 N w x

theorem Proofs.Mnv4TieB.mnv4Pre4_eq_blk (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre4 N w x = mnv4Blk10 N w x

theorem Proofs.Mnv4TieB.mnv4Pre5_eq_blk (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre5 N w x = mnv4Blk15 N w x

theorem Proofs.Mnv4TieB.mnv4Pre6_eq_blk (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre6 N w x = mnv4Blk21 N w x

theorem Proofs.Mnv4TieB.mnv4Blk0_eq (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

mnv4Blk0 N w x = projB N w.f0pW w.f0pb w.f0pE w.f0pg w.f0pbt (StableHLO.cbReluStridedB N w.f0cW w.f0cb w.f0cE w.f0cg w.f0cbt (StableHLO.mnv4Pre0 N w x))

The fused stage's output, as the plain stage functions.

theorem Proofs.Mnv4TieB.mnv4Pre0_eq (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) :

StableHLO.mnv4Pre0 N w x = StableHLO.mnv4StemB N 112 112 w.sW w.sb w.sE w.sg w.sbt x

noncomputable def Proofs.Mnv4TieB.mnv4Suf21 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 21 — the head.

Equations

Proofs.Mnv4TieB.mnv4Suf21 N w = (Proofs.StableHLO.mnv4HeadStack N w).fwd

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf20 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 20: block 21, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf20 N w y = Proofs.Mnv4TieB.mnv4Suf21 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row21 w.b21).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf19 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 19: block 20, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf19 N w y = Proofs.Mnv4TieB.mnv4Suf20 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row20 w.b20).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf18 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 18: block 19, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf18 N w y = Proofs.Mnv4TieB.mnv4Suf19 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row19 w.b19).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf17 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 17: block 18, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf17 N w y = Proofs.Mnv4TieB.mnv4Suf18 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row18 w.b18).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf16 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 16: block 17, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf16 N w y = Proofs.Mnv4TieB.mnv4Suf17 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row17 w.b17).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf15 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 15: block 16, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf15 N w y = Proofs.Mnv4TieB.mnv4Suf16 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row16 w.b16).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf14 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 14: block 15, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf14 N w y = Proofs.Mnv4TieB.mnv4Suf15 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row15 w.b15).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf13 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 13: block 14, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf13 N w y = Proofs.Mnv4TieB.mnv4Suf14 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row14 w.b14).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf12 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 12: block 13, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf12 N w y = Proofs.Mnv4TieB.mnv4Suf13 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row13 w.b13).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf11 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (256 * 7 * 7)) → Vec (N * nCls)

The net after block 11: block 12, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf11 N w y = Proofs.Mnv4TieB.mnv4Suf12 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row12 w.b12).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf10 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 10: block 11, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf10 N w y = Proofs.Mnv4TieB.mnv4Suf11 N w ((Proofs.StableHLO.mnv4StridedBodyOfRow N Proofs.StableHLO.mnv4Row11 w.b11).fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf9 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 9: block 10, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf9 N w y = Proofs.Mnv4TieB.mnv4Suf10 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row10 w.b10).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf8 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 8: block 9, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf8 N w y = Proofs.Mnv4TieB.mnv4Suf9 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row9 w.b9).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf7 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 7: block 8, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf7 N w y = Proofs.Mnv4TieB.mnv4Suf8 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row8 w.b8).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf6 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 6: block 7, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf6 N w y = Proofs.Mnv4TieB.mnv4Suf7 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row7 w.b7).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf5 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 5: block 6, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf5 N w y = Proofs.Mnv4TieB.mnv4Suf6 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row6 w.b6).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf4 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 4: block 5, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf4 N w y = Proofs.Mnv4TieB.mnv4Suf5 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row5 w.b5).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf3 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (160 * 14 * 14)) → Vec (N * nCls)

The net after block 3: block 4, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf3 N w y = Proofs.Mnv4TieB.mnv4Suf4 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row4 w.b4).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf2 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (80 * 28 * 28)) → Vec (N * nCls)

The net after block 2: block 3, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf2 N w y = Proofs.Mnv4TieB.mnv4Suf3 N w ((Proofs.StableHLO.mnv4StridedBodyOfRow N Proofs.StableHLO.mnv4Row3 w.b3).fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf1 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (80 * 28 * 28)) → Vec (N * nCls)

The net after block 1: block 2, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf1 N w y = Proofs.Mnv4TieB.mnv4Suf2 N w ((Proofs.StableHLO.mnv4BodyOfRow N Proofs.StableHLO.mnv4Row2 w.b2).residual.fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4Suf0 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (48 * 56 * 56)) → Vec (N * nCls)

The net after the fused stage: block 1, then the rest.

Equations

Proofs.Mnv4TieB.mnv4Suf0 N w y = Proofs.Mnv4TieB.mnv4Suf1 N w ((Proofs.StableHLO.mnv4StridedBodyOfRow N Proofs.StableHLO.mnv4Row1 w.b1).fwd y)

Instances For

noncomputable def Proofs.Mnv4TieB.mnv4SufStem (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) :

Vec (N * (32 * 112 * 112)) → Vec (N * nCls)

The net after the stem: the fused stage, then the rest.

Equations

Proofs.Mnv4TieB.mnv4SufStem N w y = Proofs.Mnv4TieB.mnv4Suf0 N w ((Proofs.StableHLO.mnv4FusedStack N w).fwd y)

Instances For

theorem Proofs.Mnv4TieB.mnv4_factor_stem (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (W : Kernel4 32 3 3 3) (γ β : Vec 32) :

StableHLO.mobilenetv4ForwardBFull N { sW := W, sb := w.sb, sE := w.sE, hsE := ⋯, sg := γ, sbt := β, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4SufStem N w (StableHLO.mnv4StemB N 112 112 W w.sb w.sE γ β x)

The net with the stem's trained parameters varied is the suffix after the stem at the varied stem.

theorem Proofs.Mnv4TieB.mnv4_factor_fused (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (Wc : Kernel4 128 32 3 3) (γc βc : Vec 128) (Wp : Kernel4 48 128 1 1) (γp βp : Vec 48) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := Wc, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := γc, f0cbt := βc, f0pW := Wp, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := γp, f0pbt := βp, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf0 N w (projB N Wp w.f0pb w.f0pE γp βp (StableHLO.cbReluStridedB N Wc w.f0cb w.f0cE γc βc (StableHLO.mnv4Pre0 N w x)))

The net with the fused stage's trained parameters varied.

theorem Proofs.Mnv4TieB.mnv4_factor_b1 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row1) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := p, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf1 N w ((StableHLO.mnv4StridedBodyOfRow N StableHLO.mnv4Row1 p).fwd (mnv4Blk0 N w x))

The net with block 1's weights varied is the suffix after block 1 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b2 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row2) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := p, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf2 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row2 p).residual.fwd (mnv4Blk1 N w x))

The net with block 2's weights varied is the suffix after block 2 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b3 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row3) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := p, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf3 N w ((StableHLO.mnv4StridedBodyOfRow N StableHLO.mnv4Row3 p).fwd (mnv4Blk2 N w x))

The net with block 3's weights varied is the suffix after block 3 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b4 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row4) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := p, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf4 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row4 p).residual.fwd (mnv4Blk3 N w x))

The net with block 4's weights varied is the suffix after block 4 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b5 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row5) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := p, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf5 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row5 p).residual.fwd (mnv4Blk4 N w x))

The net with block 5's weights varied is the suffix after block 5 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b6 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row6) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := p, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf6 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row6 p).residual.fwd (mnv4Blk5 N w x))

The net with block 6's weights varied is the suffix after block 6 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b7 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row7) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := p, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf7 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row7 p).residual.fwd (mnv4Blk6 N w x))

The net with block 7's weights varied is the suffix after block 7 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b8 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row8) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := p, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf8 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row8 p).residual.fwd (mnv4Blk7 N w x))

The net with block 8's weights varied is the suffix after block 8 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b9 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row9) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := p, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf9 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row9 p).residual.fwd (mnv4Blk8 N w x))

The net with block 9's weights varied is the suffix after block 9 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b10 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row10) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := p, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf10 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row10 p).residual.fwd (mnv4Blk9 N w x))

The net with block 10's weights varied is the suffix after block 10 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b11 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row11) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := p, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf11 N w ((StableHLO.mnv4StridedBodyOfRow N StableHLO.mnv4Row11 p).fwd (mnv4Blk10 N w x))

The net with block 11's weights varied is the suffix after block 11 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b12 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row12) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := p, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf12 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row12 p).residual.fwd (mnv4Blk11 N w x))

The net with block 12's weights varied is the suffix after block 12 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b13 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row13) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := p, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf13 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row13 p).residual.fwd (mnv4Blk12 N w x))

The net with block 13's weights varied is the suffix after block 13 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b14 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row14) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := p, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf14 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row14 p).residual.fwd (mnv4Blk13 N w x))

The net with block 14's weights varied is the suffix after block 14 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b15 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row15) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := p, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf15 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row15 p).residual.fwd (mnv4Blk14 N w x))

The net with block 15's weights varied is the suffix after block 15 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b16 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row16) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := p, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf16 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row16 p).residual.fwd (mnv4Blk15 N w x))

The net with block 16's weights varied is the suffix after block 16 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b17 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row17) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := p, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf17 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row17 p).residual.fwd (mnv4Blk16 N w x))

The net with block 17's weights varied is the suffix after block 17 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b18 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row18) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := p, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf18 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row18 p).residual.fwd (mnv4Blk17 N w x))

The net with block 18's weights varied is the suffix after block 18 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b19 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row19) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := p, b20 := w.b20, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf19 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row19 p).residual.fwd (mnv4Blk18 N w x))

The net with block 19's weights varied is the suffix after block 19 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b20 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row20) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := p, b21 := w.b21, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf20 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row20 p).residual.fwd (mnv4Blk19 N w x))

The net with block 20's weights varied is the suffix after block 20 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_b21 (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (p : StableHLO.UibParams StableHLO.mnv4Row21) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := p, h1W := w.h1W, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := w.h1g, h1bt := w.h1bt, hW := w.hW, hb := w.hb, hE := w.hE, hhE := ⋯, hg := w.hg, hbt := w.hbt, Wd := w.Wd, bd := w.bd } x = mnv4Suf21 N w ((StableHLO.mnv4BodyOfRow N StableHLO.mnv4Row21 p).residual.fwd (mnv4Blk20 N w x))

The net with block 21's weights varied is the suffix after block 21 at the varied block.

theorem Proofs.Mnv4TieB.mnv4_factor_head (N : ℕ) {nCls : ℕ} (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (W1 : Kernel4 960 256 1 1) (γ1 β1 : Vec 960) (W2 : Kernel4 1280 960 1 1) (γ2 β2 : Vec 1280) (Wd : Mat 1280 nCls) (bd : Vec nCls) :

StableHLO.mobilenetv4ForwardBFull N { sW := w.sW, sb := w.sb, sE := w.sE, hsE := ⋯, sg := w.sg, sbt := w.sbt, f0cW := w.f0cW, f0cb := w.f0cb, f0cE := w.f0cE, hf0cE := ⋯, f0cg := w.f0cg, f0cbt := w.f0cbt, f0pW := w.f0pW, f0pb := w.f0pb, f0pE := w.f0pE, hf0pE := ⋯, f0pg := w.f0pg, f0pbt := w.f0pbt, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, b18 := w.b18, b19 := w.b19, b20 := w.b20, b21 := w.b21, h1W := W1, h1b := w.h1b, h1E := w.h1E, hh1E := ⋯, h1g := γ1, h1bt := β1, hW := W2, hb := w.hb, hE := w.hE, hhE := ⋯, hg := γ2, hbt := β2, Wd := Wd, bd := bd } x = mnv4HeadFwd N 7 7 W1 w.h1b w.h1E γ1 β1 W2 w.hb w.hE γ2 β2 Wd bd (mnv4Blk21 N w x)

The net with the head's trained parameters varied is the head at them.

def Proofs.Mnv4TieB.Mnv4NetLossTiedB (N : ℕ) {nCls : ℕ} (xN cotN vN epsStr : String) (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (L : Vec (N * nCls) → Vec 1) (g : Vec (N * nCls)) :

Every MobileNetV4-Conv-M parameter gradient node is the derivative of L in that parameter, for a loss L of the logits and g the cotangent the chain starts from: the 233 nodes mnv4_net_tiedB ties, each at the cotangent the emitted chain threads to it, stated against L of mobilenetv4ForwardBFull with that one parameter varied.

Equations

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

Instances For

theorem Proofs.Mnv4TieB.mnv4_net_lossGrad (N : ℕ) {nCls : ℕ} (xN cotN vN epsStr : String) (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (hx : StableHLO.Mnv4SmoothAt N w x) {L : Vec (N * nCls) → Vec 1} {g : Vec (N * nCls)} (hL : HasGradAt L (StableHLO.mobilenetv4ForwardBFull N w x) g) :

Mnv4NetLossTiedB N xN cotN vN epsStr w x L g

Every MobileNetV4-Conv-M parameter gradient node is the derivative of the loss in that parameter. For any loss L of the logits with gradient g at the net's output, each of the 233 nodes mnv4_net_tiedB ties — at the same cotangent — is ∂L/∂θ of the WHOLE net, mobilenetv4ForwardBFull with that one parameter varied (a stem, fused-stage or head field, or a block's weight record w.bk := p with one slot changed — a depthwise slot through withPre / withPost).

The only hypothesis is Mnv4SmoothAt (the stem's relu clause and each group's .ok); the BN ε > 0 facts are fields of the weights. The loss enters only through hL; mnv4_net_lossGrad_smoothedCE discharges it for the loss the artifacts ship.

theorem Proofs.Mnv4TieB.mnv4_net_lossGrad_smoothedCE (N : ℕ) {nCls : ℕ} (hK : 0 < nCls) (xN cotN vN epsStr aStr negAK bStr logN ohN : String) (α B : ℝ) (w : StableHLO.Mnv4BWeights nCls) (x : Vec (N * (3 * 224 * 224))) (hx : StableHLO.Mnv4SmoothAt N w x) (t : Vec (N * (1 * nCls))) (ht : ∀ (n : Fin N), ∑ k : Fin nCls, targetRow N nCls t n k = 1) :

Mnv4NetLossTiedB N xN cotN vN epsStr w x (smoothedBatchLoss N nCls α B t) (BackLinks.unrowB N nCls (StableHLO.den (smoothedLossCotGraph N nCls α B aStr negAK bStr logN ohN (BackLinks.rowB N nCls (StableHLO.mobilenetv4ForwardBFull N w x)) t)))

The loss the artifacts ship: every node is the derivative of the batched label-smoothed cross-entropy smoothedBatchLoss, g the six-op cotangent the render emits.