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.
Scope. One replica, at either precision: every conv and depthwise weight node is stated on the
renderers' switch (convWeightGradBAt bf16 id …, depthwiseWeightGradBAt bf16 id …, …;
Foundation.GradNodesBAt), so bf16 := true is the bf16 kind the mnv4in_*bf16 artifacts emit,
read over ℝ at the identity rounding (Bf16Erasure), and bf16 := false the f32 artifacts'.
Drop-path and classifier dropout (*drop*, *do*) are outside this statement. Sync-BN data parallelism is reached by composition:
mnv4_net_syncTiedB says each all-reduced gradient is this net's tied node at N := R·N, which
this file's capstone makes the loss's gradient at the global batch.
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 aDWSlotthat is aDWBnParamsonly atk > 0. So each family bundle (mnv4ExtraDWLossTiedB,mnv4ConvNeXtLossTiedB,mnv4FfnLossTiedB,mnv4StridedLossTiedB) takes its row'sk ≠ 0/k = 0facts, the slots' forwards reduce bymnv4PreDWSlot_fwd_of_ne_zeroand friends, and a depthwise parameter is varied throughUibParams.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, andmnv4Pre{k}meetsmnv4Blk{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.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)
:
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)
:
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)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 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)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 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)))
:
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)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 xin Φ g
def
Proofs.Mnv4TieB.mnv4ExtraDWLossTiedB
(N : ℕ)
(s : StableHLO.UibSpec)
(xN cotN vN epsStr : String)
(p : StableHLO.UibParams s)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 v Φ dy
def
Proofs.Mnv4TieB.mnv4ConvNeXtLossTiedB
(N : ℕ)
(s : StableHLO.UibSpec)
(xN cotN vN epsStr : String)
(p : StableHLO.UibParams s)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 v Φ dy
def
Proofs.Mnv4TieB.mnv4FfnLossTiedB
(N : ℕ)
(s : StableHLO.UibSpec)
(xN cotN vN epsStr : String)
(p : StableHLO.UibParams s)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 v Φ dy
def
Proofs.Mnv4TieB.mnv4StridedLossTiedB
(N : ℕ)
(s : StableHLO.UibSpec)
(xN cotN vN epsStr : String)
(p : StableHLO.UibParams s)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 v Φ dy
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)
:
A skip block's step: the emitted fan-in body dx + dyOut is the residual layer's backward.
theorem
Proofs.Mnv4TieB.mnv4Pre2_eq_blk
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights nCls)
(x : Vec (N * (3 * 224 * 224)))
:
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)))
:
theorem
Proofs.Mnv4TieB.mnv4Pre4_eq_blk
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights nCls)
(x : Vec (N * (3 * 224 * 224)))
:
theorem
Proofs.Mnv4TieB.mnv4Pre5_eq_blk
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights nCls)
(x : Vec (N * (3 * 224 * 224)))
:
theorem
Proofs.Mnv4TieB.mnv4Pre6_eq_blk
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights nCls)
(x : Vec (N * (3 * 224 * 224)))
:
theorem
Proofs.Mnv4TieB.mnv4Blk0_eq
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights nCls)
(x : Vec (N * (3 * 224 * 224)))
:
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)))
:
The net after block 21 — the head.
Equations
Instances For
The net after block 20: block 21, then the rest.
Equations
Instances For
The net after block 19: block 20, then the rest.
Equations
Instances For
The net after block 18: block 19, then the rest.
Equations
Instances For
The net after block 17: block 18, then the rest.
Equations
Instances For
The net after block 16: block 17, then the rest.
Equations
Instances For
The net after block 15: block 16, then the rest.
Equations
Instances For
The net after block 14: block 15, then the rest.
Equations
Instances For
The net after block 13: block 14, then the rest.
Equations
Instances For
The net after block 12: block 13, then the rest.
Equations
Instances For
The net after block 11: block 12, then the rest.
Equations
Instances For
The net after block 10: block 11, then the rest.
Equations
Instances For
The net after block 9: block 10, then the rest.
Equations
Instances For
The net after block 8: block 9, then the rest.
Equations
Instances For
The net after block 7: block 8, then the rest.
Equations
Instances For
The net after block 6: block 7, then the rest.
Equations
Instances For
The net after block 5: block 6, then the rest.
Equations
Instances For
The net after block 4: block 5, then the rest.
Equations
Instances For
The net after block 3: block 4, then the rest.
Equations
Instances For
The net after block 2: block 3, then the rest.
Equations
Instances For
The net after block 1: block 2, then the rest.
Equations
Instances For
The net after the fused stage: block 1, then the rest.
Equations
Instances For
noncomputable def
Proofs.Mnv4TieB.mnv4SufStem
(N : ℕ)
{nCls : ℕ}
(w : StableHLO.Mnv4BWeights 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)
(bf16 : Bool)
(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)
(bf16 : Bool)
(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 bf16 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.
The nodes are one replica's, at either precision (the module's Scope).
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)
(bf16 : Bool)
(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 bf16 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.
theorem
Proofs.Mnv4TieB.mnv4_net_tied_lossGrad
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : StableHLO.Mnv4BWeights nCls)
(bf16 : Bool)
(x : Vec (N * (3 * 224 * 224)))
(g : Vec (N * nCls))
(hx : StableHLO.Mnv4SmoothAt N w x)
{L : Vec (N * nCls) → Vec 1}
(hL : HasGradAt L (StableHLO.mobilenetv4ForwardBFull N w x) g)
:
have dy21 := mnv4HeadCotIn N 7 7 w.h1W w.h1b w.h1E w.h1g w.h1bt w.hW w.hb w.hE w.hg w.hbt w.Wd w.bd (mnv4Blk21 N w x) g;
have dy20 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row21 w.b21 (mnv4Blk20 N w x) dy21) dy21;
have dy19 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row20 w.b20 (mnv4Blk19 N w x) dy20) dy20;
have dy18 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row19 w.b19 (mnv4Blk18 N w x) dy19) dy19;
have dy17 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row18 w.b18 (mnv4Blk17 N w x) dy18) dy18;
have dy16 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row17 w.b17 (mnv4Blk16 N w x) dy17) dy17;
have dy15 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row16 w.b16 (mnv4Blk15 N w x) dy16) dy16;
have dy14 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row15 w.b15 (mnv4Blk14 N w x) dy15) dy15;
have dy13 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row14 w.b14 (mnv4Blk13 N w x) dy14) dy14;
have dy12 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row13 w.b13 (mnv4Blk12 N w x) dy13) dy13;
have dy11 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row12 w.b12 (mnv4Blk11 N w x) dy12) dy12;
have dy10 := mnv4SBodyCotIn N StableHLO.mnv4Row11 w.b11 (mnv4Blk10 N w x) dy11;
have dy9 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row10 w.b10 (mnv4Blk9 N w x) dy10) dy10;
have dy8 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row9 w.b9 (mnv4Blk8 N w x) dy9) dy9;
have dy7 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row8 w.b8 (mnv4Blk7 N w x) dy8) dy8;
have dy6 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row7 w.b7 (mnv4Blk6 N w x) dy7) dy7;
have dy5 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row6 w.b6 (mnv4Blk5 N w x) dy6) dy6;
have dy4 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row5 w.b5 (mnv4Blk4 N w x) dy5) dy5;
have dy3 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row4 w.b4 (mnv4Blk3 N w x) dy4) dy4;
have dy2 := mnv4SBodyCotIn N StableHLO.mnv4Row3 w.b3 (mnv4Blk2 N w x) dy3;
have dy1 := mnv4SkipCotIn (mnv4BodyCotIn N StableHLO.mnv4Row2 w.b2 (mnv4Blk1 N w x) dy2) dy2;
have dy0 := mnv4SBodyCotIn N StableHLO.mnv4Row1 w.b1 (mnv4Blk0 N w x) dy1;
have dyStem :=
mnv4FusedCotIn N 56 56 w.f0cW w.f0cb w.f0cE w.f0cg w.f0cbt w.f0pW w.f0pb w.f0pE w.f0pg w.f0pbt
(StableHLO.mnv4Pre0 N w x) dy0;
(mnv4StemTiedB N 112 112 xN cotN vN epsStr w.sW w.sb w.sE w.sg w.sbt bf16 x dyStem ∧ mnv4StemLossTiedB xN cotN vN epsStr w.sW w.sb w.sE w.sg w.sbt bf16 x
(fun (W : Kernel4 32 3 3 3) (γ β : Vec 32) =>
L
(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))
dyStem) ∧ (mnv4FusedTiedB N 56 56 w.f0cW w.f0cb w.f0cE w.f0cg w.f0cbt w.f0pW w.f0pb w.f0pE w.f0pg w.f0pbt xN cotN vN epsStr bf16
(StableHLO.mnv4Pre0 N w x) dy0 ∧ mnv4FusedLossTiedB w.f0cW w.f0cb w.f0cE w.f0cg w.f0cbt w.f0pW w.f0pb w.f0pE w.f0pg w.f0pbt xN cotN vN epsStr bf16
(StableHLO.mnv4Pre0 N w x)
(fun (Wc : Kernel4 128 32 3 3) (γc βc : Vec 128) (Wp : Kernel4 48 128 1 1) (γp βp : Vec 48) =>
L
(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))
dy0) ∧ (mnv4StridedTiedB N StableHLO.mnv4Row1 xN cotN vN epsStr w.b1 bf16 (mnv4Blk0 N w x) dy1 ∧ mnv4StridedLossTiedB N StableHLO.mnv4Row1 xN cotN vN epsStr w.b1 bf16 (mnv4Blk0 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row1) =>
L
(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))
dy1) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row2 xN cotN vN epsStr w.b2 bf16 (mnv4Blk1 N w x) dy2 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row2 xN cotN vN epsStr w.b2 bf16 (mnv4Blk1 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row2) =>
L
(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))
dy2) ∧ (mnv4StridedTiedB N StableHLO.mnv4Row3 xN cotN vN epsStr w.b3 bf16 (mnv4Blk2 N w x) dy3 ∧ mnv4StridedLossTiedB N StableHLO.mnv4Row3 xN cotN vN epsStr w.b3 bf16 (mnv4Blk2 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row3) =>
L
(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))
dy3) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row4 xN cotN vN epsStr w.b4 bf16 (mnv4Blk3 N w x) dy4 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row4 xN cotN vN epsStr w.b4 bf16 (mnv4Blk3 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row4) =>
L
(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))
dy4) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row5 xN cotN vN epsStr w.b5 bf16 (mnv4Blk4 N w x) dy5 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row5 xN cotN vN epsStr w.b5 bf16 (mnv4Blk4 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row5) =>
L
(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))
dy5) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row6 xN cotN vN epsStr w.b6 bf16 (mnv4Blk5 N w x) dy6 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row6 xN cotN vN epsStr w.b6 bf16 (mnv4Blk5 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row6) =>
L
(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))
dy6) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row7 xN cotN vN epsStr w.b7 bf16 (mnv4Blk6 N w x) dy7 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row7 xN cotN vN epsStr w.b7 bf16 (mnv4Blk6 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row7) =>
L
(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))
dy7) ∧ (mnv4ConvNeXtTiedB N StableHLO.mnv4Row8 xN cotN vN epsStr w.b8 bf16 (mnv4Blk7 N w x) dy8 ∧ mnv4ConvNeXtLossTiedB N StableHLO.mnv4Row8 xN cotN vN epsStr w.b8 bf16 (mnv4Blk7 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row8) =>
L
(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))
dy8) ∧ (mnv4FfnTiedB N StableHLO.mnv4Row9 xN cotN vN epsStr w.b9 bf16 (mnv4Blk8 N w x) dy9 ∧ mnv4FfnLossTiedB N StableHLO.mnv4Row9 xN cotN vN epsStr w.b9 bf16 (mnv4Blk8 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row9) =>
L
(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))
dy9) ∧ (mnv4ConvNeXtTiedB N StableHLO.mnv4Row10 xN cotN vN epsStr w.b10 bf16 (mnv4Blk9 N w x) dy10 ∧ mnv4ConvNeXtLossTiedB N StableHLO.mnv4Row10 xN cotN vN epsStr w.b10 bf16 (mnv4Blk9 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row10) =>
L
(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))
dy10) ∧ (mnv4StridedTiedB N StableHLO.mnv4Row11 xN cotN vN epsStr w.b11 bf16 (mnv4Blk10 N w x) dy11 ∧ mnv4StridedLossTiedB N StableHLO.mnv4Row11 xN cotN vN epsStr w.b11 bf16 (mnv4Blk10 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row11) =>
L
(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))
dy11) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row12 xN cotN vN epsStr w.b12 bf16 (mnv4Blk11 N w x) dy12 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row12 xN cotN vN epsStr w.b12 bf16 (mnv4Blk11 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row12) =>
L
(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))
dy12) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row13 xN cotN vN epsStr w.b13 bf16 (mnv4Blk12 N w x)
dy13 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row13 xN cotN vN epsStr w.b13 bf16
(mnv4Blk12 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row13) =>
L
(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))
dy13) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row14 xN cotN vN epsStr w.b14 bf16 (mnv4Blk13 N w x)
dy14 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row14 xN cotN vN epsStr w.b14 bf16
(mnv4Blk13 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row14) =>
L
(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))
dy14) ∧ (mnv4FfnTiedB N StableHLO.mnv4Row15 xN cotN vN epsStr w.b15 bf16 (mnv4Blk14 N w x)
dy15 ∧ mnv4FfnLossTiedB N StableHLO.mnv4Row15 xN cotN vN epsStr w.b15 bf16
(mnv4Blk14 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row15) =>
L
(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))
dy15) ∧ (mnv4ConvNeXtTiedB N StableHLO.mnv4Row16 xN cotN vN epsStr w.b16 bf16
(mnv4Blk15 N w x) dy16 ∧ mnv4ConvNeXtLossTiedB N StableHLO.mnv4Row16 xN cotN vN epsStr w.b16 bf16
(mnv4Blk15 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row16) =>
L
(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))
dy16) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row17 xN cotN vN epsStr w.b17 bf16
(mnv4Blk16 N w x) dy17 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row17 xN cotN vN epsStr w.b17 bf16
(mnv4Blk16 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row17) =>
L
(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))
dy17) ∧ (mnv4ExtraDWTiedB N StableHLO.mnv4Row18 xN cotN vN epsStr w.b18 bf16
(mnv4Blk17 N w x) dy18 ∧ mnv4ExtraDWLossTiedB N StableHLO.mnv4Row18 xN cotN vN epsStr w.b18 bf16
(mnv4Blk17 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row18) =>
L
(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))
dy18) ∧ (mnv4FfnTiedB N StableHLO.mnv4Row19 xN cotN vN epsStr w.b19 bf16
(mnv4Blk18 N w x) dy19 ∧ mnv4FfnLossTiedB N StableHLO.mnv4Row19 xN cotN vN epsStr w.b19 bf16
(mnv4Blk18 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row19) =>
L
(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))
dy19) ∧ (mnv4FfnTiedB N StableHLO.mnv4Row20 xN cotN vN epsStr w.b20 bf16
(mnv4Blk19 N w x) dy20 ∧ mnv4FfnLossTiedB N StableHLO.mnv4Row20 xN cotN vN epsStr w.b20 bf16
(mnv4Blk19 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row20) =>
L
(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))
dy20) ∧ (mnv4ConvNeXtTiedB N StableHLO.mnv4Row21 xN cotN vN epsStr w.b21 bf16
(mnv4Blk20 N w x) dy21 ∧ mnv4ConvNeXtLossTiedB N StableHLO.mnv4Row21 xN cotN vN epsStr w.b21 bf16
(mnv4Blk20 N w x)
(fun (p : StableHLO.UibParams StableHLO.mnv4Row21) =>
L (StableHLO.mobilenetv4ForwardBFull N ⋯ x))
dy21) ∧ mnv4HeadTiedB N 7 7 w.h1W w.h1b w.h1E w.h1g w.h1bt w.hW w.hb w.hE w.hg
w.hbt w.Wd w.bd xN cotN vN epsStr bf16 (mnv4Blk21 N w x) g ∧ mnv4HeadLossTiedB w.h1W w.h1b w.h1E w.h1g w.h1bt w.hW w.hb w.hE w.hg
w.hbt w.Wd w.bd xN cotN vN epsStr bf16 (mnv4Blk21 N w x)
(fun (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) =>
L (StableHLO.mobilenetv4ForwardBFull N ⋯ x))
g
The emitted MobileNetV4 step's gradient nodes ARE the loss's gradient, at one chain. For
each of the 233 parameter slots, at ONE cotangent chain (the tie's own, from g): the node
denotes its layer's Jacobian against the chain cotangent (mnv4_net_tiedB), and any loss L of
the logits with gradient g at the network's output, read on mobilenetv4ForwardBFull with
that one slot varied, is differentiable there with the node as its gradient
(mnv4_net_lossGrad). The two theorems each state the chain; this one states it once, so an
edit to either chain breaks its proof.