Documentation

LeanMlir.Proofs.Nets.ViT.ViTStepTie

ViT-Tiny §1a tie — the SGD-inline train step, all 200 parameters at the real backward chain #

What this file is. The T3 §1a tie of verified_mlir/vit_train_step.mlir — the per-example SGD-inline step ViTRender.lean still writes — at the fused θ − lr·g ops: vit_net_tied_certified (the last theorem) threads all 200 ViT-Tiny parameters through the committed multi-head (3 heads, d_head 64), depth-12, vector-LayerNorm forward and the loss-driven backward cotangent chain. Its batched peer at the un-fused gradient node, the smoothed loss and a batch binder — the chain every vitin_* accuracy comes from — is ViTTiePoCGB.vit_net_tiedGB, built from this file's block ties by batchMap / batchMapAux.

The file has two layers:

Every conjunct delegates to a ViTPoC.*_den fold lemma at the chain cotangent — zero new ops, zero new bridges. The vector-LN granularity that ships ([192] γ/β) is what is modelled.

Multi-head promotion (3 heads, d_head=64) — the committed-render block tie #

The committed vitTrainStepRenderV is multi-head: the SDPA-internal backward dAtt → dQ/dK/dV runs per head (vitCotD{Q,K,V}mh, ViTMultiHeadChain), so the Q/K/V dense cotangents are the multi-head …mh ones rather than the single-head vitCotD{Q,K,V}; everything else (the out-proj Wo, LN₂, the MLP) is head-agnostic. vitBlockTiedMHV states the block's 16 parameter ties with those cotangents (no separate ss/p saves — the per-head scores/weights are recomputed inside the …mh cots from the saved Q/K); every conjunct delegates to a head-agnostic §1-fold generic ViTPoC.*_den. @[irreducible] wrappers keep the 12-block composition opaque.

source
def Proofs.ViTTiePoC.vitBlockTiedMHV {Np1 heads d mlpDim : ℕ} (xN wN bN gN epsStr lrStr cotN : String) (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (bfc2 : Vec (heads * d)) (xin ln1 q k v att h ln2 : Vec (Np1 * (heads * d))) (g m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * (heads * d))) (lr : ℝ) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Proofs.ViTTiePoC.vit_block_tiedMHV {Np1 heads d mlpDim : ℕ} (xN wN bN gN epsStr lrStr cotN : String) (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (bfc2 : Vec (heads * d)) (xin ln1 q k v att h ln2 : Vec (Np1 * (heads * d))) (g m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * (heads * d))) (lr : ℝ) :
    vitBlockTiedMHV xN wN bN gN epsStr lrStr cotN ε γ1 β1 γ2 β2 Wq Wk Wv Wo bq bk bv bo Wfc1 bfc1 Wfc2 bfc2 xin ln1 q k v att h ln2 g m1 dyOut lr

    Multi-head forward + cot-in + input-only block wrappers (@[irreducible], the thread template) #

    source
    @[irreducible]
    noncomputable def Proofs.ViTTiePoC.vitBlockFwdOMHV {Np1 heads d mlpDim : ℕ} (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (bfc2 : Vec (heads * d)) (xin : Vec (Np1 * (heads * d))) :
    Vec (Np1 * (heads * d))

    Multi-head forward block step (the committed render's block forward = vitBlockSpelledMHV, which IS transformerBlockV at general heads by vitBlockSpelledMHV_eq).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[irreducible]
      noncomputable def Proofs.ViTTiePoC.vitBlockCotInAtMHV {Np1 heads d mlpDim : ℕ} (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (xin dyOut : Vec (Np1 * (heads * d))) :
      Vec (Np1 * (heads * d))

      Multi-head attention-residual fan-in: the block-input cotangent the chain hands upstream (vitCotXinV at the multi-head Q/K/V dense cots — vitCotLn1 Wq Wk Wv dQmh dKmh dVmh IS the multi-head LN₁ fan-in vitCotLn1MH). Recomputes the saves from xin (the vitBlockSpelledMHV let-chain, multi-head att).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[irreducible]
        def Proofs.ViTTiePoC.vitBlockTiedAtMHV {Np1 heads d mlpDim : ℕ} (xN wN bN gN epsStr lrStr cotN : String) (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (bfc2 : Vec (heads * d)) (xin dyOut : Vec (Np1 * (heads * d))) (lr : ℝ) :
        Prop

        Multi-head input-only block tie — recompute the 9 saves from xin, then vit_block_tiedMHV.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Proofs.ViTTiePoC.vit_block_tiedAtMHV {Np1 heads d mlpDim : ℕ} (xN wN bN gN epsStr lrStr cotN : String) (ε : ℝ) (γ1 β1 γ2 β2 : Vec (heads * d)) (Wq Wk Wv Wo : Mat (heads * d) (heads * d)) (bq bk bv bo : Vec (heads * d)) (Wfc1 : Mat (heads * d) mlpDim) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim (heads * d)) (bfc2 : Vec (heads * d)) (xin dyOut : Vec (Np1 * (heads * d))) (lr : ℝ) :
          vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε γ1 β1 γ2 β2 Wq Wk Wv Wo bq bk bv bo Wfc1 bfc1 Wfc2 bfc2 xin dyOut lr

          The multi-head input-only block tie holds — unfold the saves, delegate to vit_block_tiedMHV.

          Task 3 — the non-block param bundle + the all-200-params capstone (committed ViT-Tiny config) #

          vitFinalLNTied/vitHeadTied/vitEmbedTied bundle the final vector-LN γ/β, the classifier Wcls/bcls, and the patch-embed wConv/bConv/cls/pos as den = certified at their chain cotangents — each a direct delegation to the §1-fold generics (ViTPoC.*_den), with the cls op (denseBiasSgdB N=1) folded by vit_cls_den (its row-0 batch slice IS cls_token_grad, closed by vit_render_cls_certified). Then vit_net_tied_certified threads the REAL forward + loss-driven backward and bundles all 200 params.

          source
          theorem Proofs.ViTTiePoC.vit_cls_den (clsN lrStr cotN : String) (Wc : Kernel4 192 3 16 16) (bc cls : Vec 192) (pos : Mat 197 192) (img : Vec (3 * 224 * 224)) (dyEmbed : Vec (197 * 192)) (lr : ℝ) (i : Fin 192) :
          StableHLO.den (StableHLO.SHlo.denseBiasSgdB clsN lrStr cls lr (StableHLO.SHlo.operand cotN (StableHLO.clsSliceFlat 196 192 dyEmbed))) i = cls i - lr * ∑ j : Fin (197 * 192), pdiv (fun (cl : Vec 192) => patchEmbed_flat 3 224 224 16 196 192 Wc bc cl pos img) cls i j * dyEmbed j
          source
          def Proofs.ViTTiePoC.vitFinalLNTied (gN xN bN epsStr lrStr cotN : String) (ε : ℝ) (γF βF : Vec 192) (Wcls : Mat 192 10) (b12out : Vec (197 * 192)) (g : Vec 10) (lr : ℝ) :
          Prop

          Final vector-LN γF/βF tied at the classifier-back cot vitCotFl.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Proofs.ViTTiePoC.vit_finalLN_tied (gN xN bN epsStr lrStr cotN : String) (ε : ℝ) (γF βF : Vec 192) (Wcls : Mat 192 10) (b12out : Vec (197 * 192)) (g : Vec 10) (lr : ℝ) :
            vitFinalLNTied gN xN bN epsStr lrStr cotN ε γF βF Wcls b12out g lr
            source
            def Proofs.ViTTiePoC.vitHeadTied (aN wN bN lrStr cotN : String) (hn : Vec 192) (Wcls : Mat 192 10) (bcls g : Vec 10) (lr : ℝ) :
            Prop

            Classifier Wcls/bcls tied at the loss cotangent g.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Proofs.ViTTiePoC.vit_head_tied (aN wN bN lrStr cotN : String) (hn : Vec 192) (Wcls : Mat 192 10) (bcls g : Vec 10) (lr : ℝ) :
              vitHeadTied aN wN bN lrStr cotN hn Wcls bcls g lr
              source
              def Proofs.ViTTiePoC.vitEmbedTied (wN xN bN clsN pN lrStr cotN : String) (Wc : Kernel4 192 3 16 16) (bc cls : Vec 192) (pos : Mat 197 192) (img : Vec (3 * 224 * 224)) (dyEmbed : Vec (197 * 192)) (lr : ℝ) :
              Prop

              Patch embed wConv/bConv/cls/pos tied at the embed-output cot dyEmbed.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Proofs.ViTTiePoC.vit_embed_tied (wN xN bN clsN pN lrStr cotN : String) (Wc : Kernel4 192 3 16 16) (bc cls : Vec 192) (pos : Mat 197 192) (img : Vec (3 * 224 * 224)) (dyEmbed : Vec (197 * 192)) (lr : ℝ) :
                vitEmbedTied wN xN bN clsN pN lrStr cotN Wc bc cls pos img dyEmbed lr
                source
                theorem Proofs.ViTTiePoC.vit_net_tied_certified (xN wN bN gN aN clsN pN epsStr lrStr cotN : String) (ε : ℝ) (Wc : Kernel4 192 3 16 16) (bc cls : Vec 192) (pos : Mat 197 192) (γF βF : Vec 192) (Wcls : Mat 192 10) (bcls : Vec 10) (lnG1_1 lnB1_1 lnG2_1 lnB2_1 : Vec 192) (mWq_1 mWk_1 mWv_1 mWo_1 : Mat 192 192) (mbq_1 mbk_1 mbv_1 mbo_1 : Vec 192) (fW1_1 : Mat 192 768) (fb1_1 : Vec 768) (fW2_1 : Mat 768 192) (fb2_1 lnG1_2 lnB1_2 lnG2_2 lnB2_2 : Vec 192) (mWq_2 mWk_2 mWv_2 mWo_2 : Mat 192 192) (mbq_2 mbk_2 mbv_2 mbo_2 : Vec 192) (fW1_2 : Mat 192 768) (fb1_2 : Vec 768) (fW2_2 : Mat 768 192) (fb2_2 lnG1_3 lnB1_3 lnG2_3 lnB2_3 : Vec 192) (mWq_3 mWk_3 mWv_3 mWo_3 : Mat 192 192) (mbq_3 mbk_3 mbv_3 mbo_3 : Vec 192) (fW1_3 : Mat 192 768) (fb1_3 : Vec 768) (fW2_3 : Mat 768 192) (fb2_3 lnG1_4 lnB1_4 lnG2_4 lnB2_4 : Vec 192) (mWq_4 mWk_4 mWv_4 mWo_4 : Mat 192 192) (mbq_4 mbk_4 mbv_4 mbo_4 : Vec 192) (fW1_4 : Mat 192 768) (fb1_4 : Vec 768) (fW2_4 : Mat 768 192) (fb2_4 lnG1_5 lnB1_5 lnG2_5 lnB2_5 : Vec 192) (mWq_5 mWk_5 mWv_5 mWo_5 : Mat 192 192) (mbq_5 mbk_5 mbv_5 mbo_5 : Vec 192) (fW1_5 : Mat 192 768) (fb1_5 : Vec 768) (fW2_5 : Mat 768 192) (fb2_5 lnG1_6 lnB1_6 lnG2_6 lnB2_6 : Vec 192) (mWq_6 mWk_6 mWv_6 mWo_6 : Mat 192 192) (mbq_6 mbk_6 mbv_6 mbo_6 : Vec 192) (fW1_6 : Mat 192 768) (fb1_6 : Vec 768) (fW2_6 : Mat 768 192) (fb2_6 lnG1_7 lnB1_7 lnG2_7 lnB2_7 : Vec 192) (mWq_7 mWk_7 mWv_7 mWo_7 : Mat 192 192) (mbq_7 mbk_7 mbv_7 mbo_7 : Vec 192) (fW1_7 : Mat 192 768) (fb1_7 : Vec 768) (fW2_7 : Mat 768 192) (fb2_7 lnG1_8 lnB1_8 lnG2_8 lnB2_8 : Vec 192) (mWq_8 mWk_8 mWv_8 mWo_8 : Mat 192 192) (mbq_8 mbk_8 mbv_8 mbo_8 : Vec 192) (fW1_8 : Mat 192 768) (fb1_8 : Vec 768) (fW2_8 : Mat 768 192) (fb2_8 lnG1_9 lnB1_9 lnG2_9 lnB2_9 : Vec 192) (mWq_9 mWk_9 mWv_9 mWo_9 : Mat 192 192) (mbq_9 mbk_9 mbv_9 mbo_9 : Vec 192) (fW1_9 : Mat 192 768) (fb1_9 : Vec 768) (fW2_9 : Mat 768 192) (fb2_9 lnG1_10 lnB1_10 lnG2_10 lnB2_10 : Vec 192) (mWq_10 mWk_10 mWv_10 mWo_10 : Mat 192 192) (mbq_10 mbk_10 mbv_10 mbo_10 : Vec 192) (fW1_10 : Mat 192 768) (fb1_10 : Vec 768) (fW2_10 : Mat 768 192) (fb2_10 lnG1_11 lnB1_11 lnG2_11 lnB2_11 : Vec 192) (mWq_11 mWk_11 mWv_11 mWo_11 : Mat 192 192) (mbq_11 mbk_11 mbv_11 mbo_11 : Vec 192) (fW1_11 : Mat 192 768) (fb1_11 : Vec 768) (fW2_11 : Mat 768 192) (fb2_11 lnG1_12 lnB1_12 lnG2_12 lnB2_12 : Vec 192) (mWq_12 mWk_12 mWv_12 mWo_12 : Mat 192 192) (mbq_12 mbk_12 mbv_12 mbo_12 : Vec 192) (fW1_12 : Mat 192 768) (fb1_12 : Vec 768) (fW2_12 : Mat 768 192) (fb2_12 : Vec 192) (img : Vec (3 * 224 * 224)) (label : Fin 10) (lr : ℝ) :
                have ib1 := patchEmbed_flat 3 224 224 16 196 192 Wc bc cls pos img; have ib2 := vitBlockFwdOMHV ε lnG1_1 lnB1_1 lnG2_1 lnB2_1 mWq_1 mWk_1 mWv_1 mWo_1 mbq_1 mbk_1 mbv_1 mbo_1 fW1_1 fb1_1 fW2_1 fb2_1 ib1; have ib3 := vitBlockFwdOMHV ε lnG1_2 lnB1_2 lnG2_2 lnB2_2 mWq_2 mWk_2 mWv_2 mWo_2 mbq_2 mbk_2 mbv_2 mbo_2 fW1_2 fb1_2 fW2_2 fb2_2 ib2; have ib4 := vitBlockFwdOMHV ε lnG1_3 lnB1_3 lnG2_3 lnB2_3 mWq_3 mWk_3 mWv_3 mWo_3 mbq_3 mbk_3 mbv_3 mbo_3 fW1_3 fb1_3 fW2_3 fb2_3 ib3; have ib5 := vitBlockFwdOMHV ε lnG1_4 lnB1_4 lnG2_4 lnB2_4 mWq_4 mWk_4 mWv_4 mWo_4 mbq_4 mbk_4 mbv_4 mbo_4 fW1_4 fb1_4 fW2_4 fb2_4 ib4; have ib6 := vitBlockFwdOMHV ε lnG1_5 lnB1_5 lnG2_5 lnB2_5 mWq_5 mWk_5 mWv_5 mWo_5 mbq_5 mbk_5 mbv_5 mbo_5 fW1_5 fb1_5 fW2_5 fb2_5 ib5; have ib7 := vitBlockFwdOMHV ε lnG1_6 lnB1_6 lnG2_6 lnB2_6 mWq_6 mWk_6 mWv_6 mWo_6 mbq_6 mbk_6 mbv_6 mbo_6 fW1_6 fb1_6 fW2_6 fb2_6 ib6; have ib8 := vitBlockFwdOMHV ε lnG1_7 lnB1_7 lnG2_7 lnB2_7 mWq_7 mWk_7 mWv_7 mWo_7 mbq_7 mbk_7 mbv_7 mbo_7 fW1_7 fb1_7 fW2_7 fb2_7 ib7; have ib9 := vitBlockFwdOMHV ε lnG1_8 lnB1_8 lnG2_8 lnB2_8 mWq_8 mWk_8 mWv_8 mWo_8 mbq_8 mbk_8 mbv_8 mbo_8 fW1_8 fb1_8 fW2_8 fb2_8 ib8; have ib10 := vitBlockFwdOMHV ε lnG1_9 lnB1_9 lnG2_9 lnB2_9 mWq_9 mWk_9 mWv_9 mWo_9 mbq_9 mbk_9 mbv_9 mbo_9 fW1_9 fb1_9 fW2_9 fb2_9 ib9; have ib11 := vitBlockFwdOMHV ε lnG1_10 lnB1_10 lnG2_10 lnB2_10 mWq_10 mWk_10 mWv_10 mWo_10 mbq_10 mbk_10 mbv_10 mbo_10 fW1_10 fb1_10 fW2_10 fb2_10 ib10; have ib12 := vitBlockFwdOMHV ε lnG1_11 lnB1_11 lnG2_11 lnB2_11 mWq_11 mWk_11 mWv_11 mWo_11 mbq_11 mbk_11 mbv_11 mbo_11 fW1_11 fb1_11 fW2_11 fb2_11 ib11; have b12out := vitBlockFwdOMHV ε lnG1_12 lnB1_12 lnG2_12 lnB2_12 mWq_12 mWk_12 mWv_12 mWo_12 mbq_12 mbk_12 mbv_12 mbo_12 fW1_12 fb1_12 fW2_12 fb2_12 ib12; have fl := Mat.flatten fun (r : Fin 197) => layerNormVec 192 ε γF βF (Mat.unflatten b12out r); have hn := StableHLO.clsSliceFlat 196 192 fl; have logits := dense Wcls bcls hn; have g := fun (c : Fin 10) => softmax 10 logits c - oneHot 10 label c; have dy12 := vitCotB2outV 196 192 10 ε γF Wcls b12out g; have dy11 := vitBlockCotInAtMHV ε lnG1_12 lnB1_12 lnG2_12 lnB2_12 mWq_12 mWk_12 mWv_12 mWo_12 mbq_12 mbk_12 mbv_12 mbo_12 fW1_12 fb1_12 fW2_12 ib12 dy12; have dy10 := vitBlockCotInAtMHV ε lnG1_11 lnB1_11 lnG2_11 lnB2_11 mWq_11 mWk_11 mWv_11 mWo_11 mbq_11 mbk_11 mbv_11 mbo_11 fW1_11 fb1_11 fW2_11 ib11 dy11; have dy9 := vitBlockCotInAtMHV ε lnG1_10 lnB1_10 lnG2_10 lnB2_10 mWq_10 mWk_10 mWv_10 mWo_10 mbq_10 mbk_10 mbv_10 mbo_10 fW1_10 fb1_10 fW2_10 ib10 dy10; have dy8 := vitBlockCotInAtMHV ε lnG1_9 lnB1_9 lnG2_9 lnB2_9 mWq_9 mWk_9 mWv_9 mWo_9 mbq_9 mbk_9 mbv_9 mbo_9 fW1_9 fb1_9 fW2_9 ib9 dy9; have dy7 := vitBlockCotInAtMHV ε lnG1_8 lnB1_8 lnG2_8 lnB2_8 mWq_8 mWk_8 mWv_8 mWo_8 mbq_8 mbk_8 mbv_8 mbo_8 fW1_8 fb1_8 fW2_8 ib8 dy8; have dy6 := vitBlockCotInAtMHV ε lnG1_7 lnB1_7 lnG2_7 lnB2_7 mWq_7 mWk_7 mWv_7 mWo_7 mbq_7 mbk_7 mbv_7 mbo_7 fW1_7 fb1_7 fW2_7 ib7 dy7; have dy5 := vitBlockCotInAtMHV ε lnG1_6 lnB1_6 lnG2_6 lnB2_6 mWq_6 mWk_6 mWv_6 mWo_6 mbq_6 mbk_6 mbv_6 mbo_6 fW1_6 fb1_6 fW2_6 ib6 dy6; have dy4 := vitBlockCotInAtMHV ε lnG1_5 lnB1_5 lnG2_5 lnB2_5 mWq_5 mWk_5 mWv_5 mWo_5 mbq_5 mbk_5 mbv_5 mbo_5 fW1_5 fb1_5 fW2_5 ib5 dy5; have dy3 := vitBlockCotInAtMHV ε lnG1_4 lnB1_4 lnG2_4 lnB2_4 mWq_4 mWk_4 mWv_4 mWo_4 mbq_4 mbk_4 mbv_4 mbo_4 fW1_4 fb1_4 fW2_4 ib4 dy4; have dy2 := vitBlockCotInAtMHV ε lnG1_3 lnB1_3 lnG2_3 lnB2_3 mWq_3 mWk_3 mWv_3 mWo_3 mbq_3 mbk_3 mbv_3 mbo_3 fW1_3 fb1_3 fW2_3 ib3 dy3; have dy1 := vitBlockCotInAtMHV ε lnG1_2 lnB1_2 lnG2_2 lnB2_2 mWq_2 mWk_2 mWv_2 mWo_2 mbq_2 mbk_2 mbv_2 mbo_2 fW1_2 fb1_2 fW2_2 ib2 dy2; have dyEmbed := vitBlockCotInAtMHV ε lnG1_1 lnB1_1 lnG2_1 lnB2_1 mWq_1 mWk_1 mWv_1 mWo_1 mbq_1 mbk_1 mbv_1 mbo_1 fW1_1 fb1_1 fW2_1 ib1 dy1; vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_1 lnB1_1 lnG2_1 lnB2_1 mWq_1 mWk_1 mWv_1 mWo_1 mbq_1 mbk_1 mbv_1 mbo_1 fW1_1 fb1_1 fW2_1 fb2_1 ib1 dy1 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_2 lnB1_2 lnG2_2 lnB2_2 mWq_2 mWk_2 mWv_2 mWo_2 mbq_2 mbk_2 mbv_2 mbo_2 fW1_2 fb1_2 fW2_2 fb2_2 ib2 dy2 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_3 lnB1_3 lnG2_3 lnB2_3 mWq_3 mWk_3 mWv_3 mWo_3 mbq_3 mbk_3 mbv_3 mbo_3 fW1_3 fb1_3 fW2_3 fb2_3 ib3 dy3 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_4 lnB1_4 lnG2_4 lnB2_4 mWq_4 mWk_4 mWv_4 mWo_4 mbq_4 mbk_4 mbv_4 mbo_4 fW1_4 fb1_4 fW2_4 fb2_4 ib4 dy4 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_5 lnB1_5 lnG2_5 lnB2_5 mWq_5 mWk_5 mWv_5 mWo_5 mbq_5 mbk_5 mbv_5 mbo_5 fW1_5 fb1_5 fW2_5 fb2_5 ib5 dy5 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_6 lnB1_6 lnG2_6 lnB2_6 mWq_6 mWk_6 mWv_6 mWo_6 mbq_6 mbk_6 mbv_6 mbo_6 fW1_6 fb1_6 fW2_6 fb2_6 ib6 dy6 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_7 lnB1_7 lnG2_7 lnB2_7 mWq_7 mWk_7 mWv_7 mWo_7 mbq_7 mbk_7 mbv_7 mbo_7 fW1_7 fb1_7 fW2_7 fb2_7 ib7 dy7 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_8 lnB1_8 lnG2_8 lnB2_8 mWq_8 mWk_8 mWv_8 mWo_8 mbq_8 mbk_8 mbv_8 mbo_8 fW1_8 fb1_8 fW2_8 fb2_8 ib8 dy8 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_9 lnB1_9 lnG2_9 lnB2_9 mWq_9 mWk_9 mWv_9 mWo_9 mbq_9 mbk_9 mbv_9 mbo_9 fW1_9 fb1_9 fW2_9 fb2_9 ib9 dy9 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_10 lnB1_10 lnG2_10 lnB2_10 mWq_10 mWk_10 mWv_10 mWo_10 mbq_10 mbk_10 mbv_10 mbo_10 fW1_10 fb1_10 fW2_10 fb2_10 ib10 dy10 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_11 lnB1_11 lnG2_11 lnB2_11 mWq_11 mWk_11 mWv_11 mWo_11 mbq_11 mbk_11 mbv_11 mbo_11 fW1_11 fb1_11 fW2_11 fb2_11 ib11 dy11 lr ∧ vitBlockTiedAtMHV xN wN bN gN epsStr lrStr cotN ε lnG1_12 lnB1_12 lnG2_12 lnB2_12 mWq_12 mWk_12 mWv_12 mWo_12 mbq_12 mbk_12 mbv_12 mbo_12 fW1_12 fb1_12 fW2_12 fb2_12 ib12 dy12 lr ∧ vitFinalLNTied gN xN bN epsStr lrStr cotN ε γF βF Wcls b12out g lr ∧ vitHeadTied aN wN bN lrStr cotN hn Wcls bcls g lr ∧ vitEmbedTied wN xN bN clsN pN lrStr cotN Wc bc cls pos img dyEmbed lr

                The whole depth-12 MULTI-HEAD ViT-Tiny train step, tied — ALL 200 params (the vit peer of convnext's cnx_net_tied_certified, at the committed config: 3 heads, d_head=64, D=192, N=196, mlpDim=768, 10 classes, 16×16 patches). The real forward patchEmbed → 12 multi-head vector-LN blocks → final vector-LN → CLS-slice → dense head and the loss-driven backward cotangent chain (the per-block multi-head fan-ins, the final-LN-back vitCotB2outV, the classifier-back vitCotFl, the embed-output cot = block-1's vitBlockCotInAtMHV output) are threaded, and EVERY param op denotes the certified loss-descent step: the 12 blocks' 192 params (vitBlockTiedAtMHV), the final-LN γ/β, the classifier Wcls/bcls, and the patch-embed wConv/bConv/cls/pos — 200/200, the FIRST net with zero param gaps (vit has the patch-weight cert). 3-axiom clean.