ViT Item D — pinning the attention-block cotangent chain

ViTClose.lean (Item C) certifies each ViT param output for any cotangent dy at that site's output. This file pins dy to the cotangent the actual backward chain delivers — the ViT analogue of ConvNeXtChainClose (planning/archive/vit_close.md Item D). Pure-Lean, batch-1 — everything in a ViT is per-example separable.

The chain composes the rendered backward denotations — exactly the Item B render's backward tokens: per-token dense input-VJP (denseRowBack's denotation rowDenseBackFlat = rowwise dX = W·dy), the GELU mask (dy ⊙ geluScalarDeriv at the saved pre-GELU), the rowwise scalar-LN input-VJP (lnRowBack's denotation rowLNBackFlat = rowwise bn_grad_input), the row-softmax backward (softmaxRowBack's denotation rowSoftmaxBackFlat, recomputing the weights from the saved pre-softmax scores), and the SDPA matmuls spelled with the forward matmulF/transposeF on cotangents (matMulFlat/transposeFlat):

block: bout = h + fc2(gelu(fc1(LN₂ h))), h = x + Wo·SDPA(Wq·LN₁x, Wk·LN₁x, Wv·LN₁x)

The MLP residual passes dyOut straight to the fc2 output AND down the LN₂ branch (vitCotH = dyOut + LN₂-back(…)); the attention residual likewise (vitCotXin = cotH + LN₁-back(…)). The new wrinkle vs all prior nets is the three-way fan-in at LN₁'s output — the Q/K/V dense-backs all read from LN₁ x, so their three cotangents SUM (vitCotLn1), the biPath fan-in at width 3.

The substantive new ties (vitCotD{Q,K,V}_eq_sdpa_back_{Q,K,V}): at the pinned saved activations (pre-softmax scores = the scaled Q·Kᵀ, post-softmax weights = sdpa_weights), the matmul-spelled chain segments ARE the proven closed forms sdpa_back_{Q,K,V} (Attention.lean) — dP = dO·Vᵀ → softmax-back → ·1/√d → dQ = dS·K / dK = dSᵀ·Q / dV = Pᵀ·dO, flattened. So the rendered attention backward is pinned to the audited SDPA backward suite, and each param output denotes θ − lr·(certified ∂/∂θ · the actual-chain cotangent). 3-axiom clean.

noncomputable def Proofs.vitCotG {Np1 D mlpDim : ℕ} (Wfc2 : Mat mlpDim D) (dyOut : Vec (Np1 * D)) : Vec (Np1 * mlpDim)

Cotangent at the GELU output (= the fc2 input): the MLP residual passes the block cotangent dyOut straight to the fc2 output (bout = h + fc2(…), no post-add activation), and fc2's input-VJP is the per-token dX = W·dy (denseRowBack's denotation).

Equations

• Proofs.vitCotG Wfc2 dyOut = Proofs.StableHLO.rowDenseBackFlat Np1 mlpDim D Wfc2 dyOut

noncomputable def Proofs.vitCotM1 {Np1 D mlpDim : ℕ} (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) : Vec (Np1 * mlpDim)

Cotangent at the fc1 output (pre-GELU): the GELU mask at the saved pre-activation m1 (geluBack's denotation).

Equations

• Proofs.vitCotM1 Wfc2 m1 dyOut i = Proofs.vitCotG Wfc2 dyOut i * Proofs.geluScalarDeriv (m1 i)

noncomputable def Proofs.vitCotLn2 {Np1 D mlpDim : ℕ} (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) : Vec (Np1 * D)

Cotangent at the LN₂ output (= the fc1 input): fc1's per-token input-VJP.

Equations

• Proofs.vitCotLn2 Wfc1 Wfc2 m1 dyOut = Proofs.StableHLO.rowDenseBackFlat Np1 D mlpDim Wfc1 (Proofs.vitCotM1 Wfc2 m1 dyOut)

noncomputable def Proofs.vitCotH {Np1 D mlpDim : ℕ} (ε γ2 : ℝ) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) : Vec (Np1 * D)

Cotangent at the attention-sublayer output h: the MLP residual fan-in — dyOut (the skip) plus the LN₂ input-VJP (lnRowBack's denotation, recomputing x̂/istd from the saved pre-LN₂ input h).

Equations

• Proofs.vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut i = dyOut i + Proofs.StableHLO.rowLNBackFlat Np1 D ε γ2 h (Proofs.vitCotLn2 Wfc1 Wfc2 m1 dyOut) i

noncomputable def Proofs.vitCotAtt {Np1 D mlpDim : ℕ} (ε γ2 : ℝ) (Wo : Mat D D) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) : Vec (Np1 * D)

Cotangent at the SDPA output att (= the out-proj input): Wo's per-token input-VJP of vitCotH.

Equations

• Proofs.vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut = Proofs.StableHLO.rowDenseBackFlat Np1 D D Wo (Proofs.vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut)

noncomputable def Proofs.vitCotDP {Np1 D : ℕ} (v dAtt : Vec (Np1 * D)) : Vec (Np1 * Np1)

dP = dAtt·Vᵀ — the rendered matmulF/transposeF on the cotangent against the saved v.

Equations

• Proofs.vitCotDP v dAtt = Proofs.StableHLO.matMulFlat Np1 D Np1 dAtt (Proofs.StableHLO.transposeFlat Np1 D v)

noncomputable def Proofs.vitCotDS {Np1 D : ℕ} (ss : Vec (Np1 * Np1)) (v dAtt : Vec (Np1 * D)) : Vec (Np1 * Np1)

dS — softmaxRowBack's denotation at the saved pre-softmax scaled scores ss.

Equations

• Proofs.vitCotDS ss v dAtt = Proofs.StableHLO.rowSoftmaxBackFlat Np1 Np1 ss (Proofs.vitCotDP v dAtt)

noncomputable def Proofs.vitCotDQ {Np1 D : ℕ} (d : ℕ) (ss : Vec (Np1 * Np1)) (k v dAtt : Vec (Np1 * D)) : Vec (Np1 * D)

dQ = (1/√d · dS)·K against the saved k.

Equations

• Proofs.vitCotDQ d ss k v dAtt = Proofs.StableHLO.matMulFlat Np1 Np1 D (fun (i : Fin (Np1 * Np1)) => Proofs.sdpa_scale d * Proofs.vitCotDS ss v dAtt i) k

noncomputable def Proofs.vitCotDK {Np1 D : ℕ} (d : ℕ) (ss : Vec (Np1 * Np1)) (q v dAtt : Vec (Np1 * D)) : Vec (Np1 * D)

dK = (1/√d · dS)ᵀ·Q against the saved q.

Equations

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

noncomputable def Proofs.vitCotDV {Np1 D : ℕ} (p : Vec (Np1 * Np1)) (dAtt : Vec (Np1 * D)) : Vec (Np1 * D)

dV = Pᵀ·dAtt against the saved post-softmax weights p.

Equations

• Proofs.vitCotDV p dAtt = Proofs.StableHLO.matMulFlat Np1 Np1 D (Proofs.StableHLO.transposeFlat Np1 Np1 p) dAtt

noncomputable def Proofs.vitCotLn1 {Np1 D : ℕ} (Wq Wk Wv : Mat D D) (dQ dK dV : Vec (Np1 * D)) : Vec (Np1 * D)

The three-way fan-in at LN₁'s output: the Q/K/V dense-backs all read from LN₁ x, so their cotangents SUM — the biPath fan-in at width 3, the new structural wrinkle vs every prior net.

Equations

• Proofs.vitCotLn1 Wq Wk Wv dQ dK dV i = Proofs.StableHLO.rowDenseBackFlat Np1 D D Wq dQ i + Proofs.StableHLO.rowDenseBackFlat Np1 D D Wk dK i + Proofs.StableHLO.rowDenseBackFlat Np1 D D Wv dV i

noncomputable def Proofs.vitCotXin {Np1 D : ℕ} (ε γ1 : ℝ) (Wq Wk Wv : Mat D D) (xin dQ dK dV cotH : Vec (Np1 * D)) : Vec (Np1 * D)

Cotangent at the block input: the attention residual fan-in — the LN₁ input-VJP of the three-way fan-in, plus the skip's cotH. This is what the block hands upstream (the previous block's dyOut; at block 1, the cotangent the embed params contract with).

Equations

• Proofs.vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH i = cotH i + Proofs.StableHLO.rowLNBackFlat Np1 D ε γ1 xin (Proofs.vitCotLn1 Wq Wk Wv dQ dK dV) i

noncomputable def Proofs.vitCotFl (N D nClasses : ℕ) (Wcls : Mat D nClasses) (dy : Vec nClasses) : Vec ((N + 1) * D)

Cotangent at the final-LN output: classifier-back (dotOut's denotation Mat.mulVec Wcls) scattered to row 0 (clsPadF's denotation clsPadFlat).

Equations

• Proofs.vitCotFl N D nClasses Wcls dy = Proofs.StableHLO.clsPadFlat N D (Wcls.mulVec dy)

noncomputable def Proofs.vitCotB2out (N D nClasses : ℕ) (ε γF : ℝ) (Wcls : Mat D nClasses) (b2out : Vec ((N + 1) * D)) (dy : Vec nClasses) : Vec ((N + 1) * D)

Cotangent at block 2's output: the final-LN input-VJP at the saved pre-LN input b2out, of vitCotFl.

Equations

• Proofs.vitCotB2out N D nClasses ε γF Wcls b2out dy = Proofs.StableHLO.rowLNBackFlat (N + 1) D ε γF b2out (Proofs.vitCotFl N D nClasses Wcls dy)

theorem Proofs.vitCotDP_eq_sdpa_dWeights (Np1 d : ℕ) (V dOut : Mat Np1 d) : vitCotDP V.flatten dOut.flatten = (sdpa_dWeights V dOut).flatten

dP-segment tie: the rendered matmulF(dOut, transposeF V) is the proven sdpa_dWeights V dOut = dOut·Vᵀ, flattened.

theorem Proofs.vitCotDV_eq_sdpa_back_V (Np1 d : ℕ) (Q K V dOut : Mat Np1 d) : vitCotDV (sdpa_weights Np1 d Q K).flatten dOut.flatten = (sdpa_back_V Np1 d Q K V dOut).flatten

dV tie: at the saved post-softmax weights (sdpa_weights Q K), the rendered matmulF(transposeF P, dOut) IS the proven sdpa_back_V = weightsᵀ·dOut.

theorem Proofs.vitCotDS_eq_sdpa_dScaled (Np1 d : ℕ) (Q K V dOut : Mat Np1 d) : vitCotDS (Mat.flatten fun (i j : Fin Np1) => sdpa_scale d * Q.mul K.transpose i j) V.flatten dOut.flatten = (sdpa_dScaled Np1 d Q K V dOut).flatten

dS-segment tie: softmaxRowBack's denotation, recomputing the weights from the saved pre-softmax scaled scores, applied to the flattened sdpa_dWeights, IS the proven sdpa_dScaled (the per-row pᵢ⊙(dwᵢ − ⟨pᵢ,dwᵢ⟩) closed form).

theorem Proofs.vitCotDQ_eq_sdpa_back_Q (Np1 d : ℕ) (Q K V dOut : Mat Np1 d) : vitCotDQ d (Mat.flatten fun (i j : Fin Np1) => sdpa_scale d * Q.mul K.transpose i j) K.flatten V.flatten dOut.flatten = (sdpa_back_Q Np1 d Q K V dOut).flatten

dQ tie: at the saved activations, the rendered matmulF(scaleF(softmaxRowBack(matmulF(dOut, transposeF V))), K) IS the proven sdpa_back_Q = (1/√d · softmax-back(dOut·Vᵀ))·K.

theorem Proofs.vitCotDK_eq_sdpa_back_K (Np1 d : ℕ) (Q K V dOut : Mat Np1 d) : vitCotDK d (Mat.flatten fun (i j : Fin Np1) => sdpa_scale d * Q.mul K.transpose i j) Q.flatten V.flatten dOut.flatten = (sdpa_back_K Np1 d Q K V dOut).flatten

dK tie: likewise the rendered transposed chain IS the proven sdpa_back_K = (1/√d · softmax-back(dOut·Vᵀ))ᵀ·Q.

theorem Proofs.vit_render_Wfc2_chain_certified {Np1 D mlpDim : ℕ} (bfc2 : Vec D) (g : Vec (Np1 * mlpDim)) (Wfc2 : Mat mlpDim D) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i : Fin mlpDim) (j : Fin D) : Wfc2 i j - lr * rowDense_weight_grad (Mat.unflatten g) (Mat.unflatten dyOut) i j = Wfc2 i j - lr * ∑ o : Fin (Np1 * D), pdiv (fun (v : Vec (mlpDim * D)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten v) bfc2 (Mat.unflatten g r)) Wfc2.flatten (finProdFinEquiv (i, j)) o * dyOut o

fc2 W, chain-certified. The chain cotangent at the fc2 output IS the block cotangent dyOut (the MLP residual is the outermost op, no post-add activation); the saved GELU output g is the layer input.

theorem Proofs.vit_render_bfc2_chain_certified {Np1 D mlpDim : ℕ} (Wfc2 : Mat mlpDim D) (g : Vec (Np1 * mlpDim)) (bfc2 : Vec D) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i : Fin D) : bfc2 i - lr * rowDense_bias_grad (Mat.unflatten dyOut) i = bfc2 i - lr * ∑ o : Fin (Np1 * D), pdiv (fun (b' : Vec D) => Mat.flatten fun (r : Fin Np1) => dense Wfc2 b' (Mat.unflatten g r)) bfc2 i o * dyOut o

fc2 b, chain-certified.

theorem Proofs.vit_render_Wfc1_chain_certified {Np1 D mlpDim : ℕ} (bfc1 : Vec mlpDim) (ln2 : Vec (Np1 * D)) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i : Fin D) (j : Fin mlpDim) : Wfc1 i j - lr * rowDense_weight_grad (Mat.unflatten ln2) (Mat.unflatten (vitCotM1 Wfc2 m1 dyOut)) i j = Wfc1 i j - lr * ∑ o : Fin (Np1 * mlpDim), pdiv (fun (v : Vec (D * mlpDim)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten v) bfc1 (Mat.unflatten ln2 r)) Wfc1.flatten (finProdFinEquiv (i, j)) o * vitCotM1 Wfc2 m1 dyOut o

fc1 W, chain-certified at vitCotM1 (fc2-back → GELU mask); the saved LN₂ output ln2 is the layer input.

theorem Proofs.vit_render_bfc1_chain_certified {Np1 D mlpDim : ℕ} (Wfc1 : Mat D mlpDim) (ln2 : Vec (Np1 * D)) (bfc1 : Vec mlpDim) (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i : Fin mlpDim) : bfc1 i - lr * rowDense_bias_grad (Mat.unflatten (vitCotM1 Wfc2 m1 dyOut)) i = bfc1 i - lr * ∑ o : Fin (Np1 * mlpDim), pdiv (fun (b' : Vec mlpDim) => Mat.flatten fun (r : Fin Np1) => dense Wfc1 b' (Mat.unflatten ln2 r)) bfc1 i o * vitCotM1 Wfc2 m1 dyOut o

fc1 b, chain-certified.

theorem Proofs.vit_render_ln2gamma_chain_certified {Np1 D mlpDim : ℕ} (ε β : ℝ) (γ : Vec 1) (h : Vec (Np1 * D)) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) : γ 0 - lr * rowLN_grad_gamma Np1 D ε (Mat.unflatten h) (Mat.unflatten (vitCotLn2 Wfc1 Wfc2 m1 dyOut)) = γ 0 - lr * ∑ o : Fin (Np1 * D), pdiv (fun (γ' : Vec 1) => Mat.flatten fun (r : Fin Np1) => layerNormForward D ε (γ' 0) β (Mat.unflatten h r)) γ 0 o * vitCotLn2 Wfc1 Wfc2 m1 dyOut o

LN₂ γ, chain-certified at vitCotLn2 (fc2-back → GELU mask → fc1-back), with the saved attention-sublayer output h as the LN input.

theorem Proofs.vit_render_ln2beta_chain_certified {Np1 D mlpDim : ℕ} (ε γsc : ℝ) (β : Vec 1) (h : Vec (Np1 * D)) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) : β 0 - lr * rowLN_grad_beta Np1 D (Mat.unflatten (vitCotLn2 Wfc1 Wfc2 m1 dyOut)) = β 0 - lr * ∑ o : Fin (Np1 * D), pdiv (fun (β' : Vec 1) => Mat.flatten fun (r : Fin Np1) => layerNormForward D ε γsc (β' 0) (Mat.unflatten h r)) β 0 o * vitCotLn2 Wfc1 Wfc2 m1 dyOut o

LN₂ β, chain-certified.

theorem Proofs.vit_render_Wo_chain_certified {Np1 D mlpDim : ℕ} (bo : Vec D) (att : Vec (Np1 * D)) (Wo : Mat D D) (ε γ2 : ℝ) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i j : Fin D) : Wo i j - lr * rowDense_weight_grad (Mat.unflatten att) (Mat.unflatten (vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut)) i j = Wo i j - lr * ∑ o : Fin (Np1 * D), pdiv (fun (v : Vec (D * D)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten v) bo (Mat.unflatten att r)) Wo.flatten (finProdFinEquiv (i, j)) o * vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut o

Wo, chain-certified at vitCotH (the MLP-sublayer residual fan-in), with the saved SDPA output att as the layer input.

theorem Proofs.vit_render_bo_chain_certified {Np1 D mlpDim : ℕ} (Wo : Mat D D) (att : Vec (Np1 * D)) (bo : Vec D) (ε γ2 : ℝ) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i : Fin D) : bo i - lr * rowDense_bias_grad (Mat.unflatten (vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut)) i = bo i - lr * ∑ o : Fin (Np1 * D), pdiv (fun (b' : Vec D) => Mat.flatten fun (r : Fin Np1) => dense Wo b' (Mat.unflatten att r)) bo i o * vitCotH ε γ2 Wfc1 Wfc2 h m1 dyOut o

bo, chain-certified.

theorem Proofs.vit_render_Wq_chain_certified {Np1 D mlpDim : ℕ} (d : ℕ) (bq : Vec D) (ln1 : Vec (Np1 * D)) (Wq : Mat D D) (ss : Vec (Np1 * Np1)) (k v : Vec (Np1 * D)) (ε γ2 : ℝ) (Wo : Mat D D) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i j : Fin D) : Wq i j - lr * rowDense_weight_grad (Mat.unflatten ln1) (Mat.unflatten (vitCotDQ d ss k v (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut))) i j = Wq i j - lr * ∑ o : Fin (Np1 * D), pdiv (fun (w : Vec (D * D)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten w) bq (Mat.unflatten ln1 r)) Wq.flatten (finProdFinEquiv (i, j)) o * vitCotDQ d ss k v (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut) o

Wq, chain-certified at vitCotDQ of the full chain (out-proj back → SDPA backward at the saved activations), with the saved LN₁ output as the layer input.

theorem Proofs.vit_render_Wk_chain_certified {Np1 D mlpDim : ℕ} (d : ℕ) (bk : Vec D) (ln1 : Vec (Np1 * D)) (Wk : Mat D D) (ss : Vec (Np1 * Np1)) (q v : Vec (Np1 * D)) (ε γ2 : ℝ) (Wo : Mat D D) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i j : Fin D) : Wk i j - lr * rowDense_weight_grad (Mat.unflatten ln1) (Mat.unflatten (vitCotDK d ss q v (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut))) i j = Wk i j - lr * ∑ o : Fin (Np1 * D), pdiv (fun (w : Vec (D * D)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten w) bk (Mat.unflatten ln1 r)) Wk.flatten (finProdFinEquiv (i, j)) o * vitCotDK d ss q v (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut) o

Wk, chain-certified at vitCotDK.

theorem Proofs.vit_render_Wv_chain_certified {Np1 D mlpDim : ℕ} (bv : Vec D) (ln1 : Vec (Np1 * D)) (Wv : Mat D D) (p : Vec (Np1 * Np1)) (ε γ2 : ℝ) (Wo : Mat D D) (Wfc1 : Mat D mlpDim) (Wfc2 : Mat mlpDim D) (h : Vec (Np1 * D)) (m1 : Vec (Np1 * mlpDim)) (dyOut : Vec (Np1 * D)) (lr : ℝ) (i j : Fin D) : Wv i j - lr * rowDense_weight_grad (Mat.unflatten ln1) (Mat.unflatten (vitCotDV p (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut))) i j = Wv i j - lr * ∑ o : Fin (Np1 * D), pdiv (fun (w : Vec (D * D)) => Mat.flatten fun (r : Fin Np1) => dense (Mat.unflatten w) bv (Mat.unflatten ln1 r)) Wv.flatten (finProdFinEquiv (i, j)) o * vitCotDV p (vitCotAtt ε γ2 Wo Wfc1 Wfc2 h m1 dyOut) o

Wv, chain-certified at vitCotDV.

theorem Proofs.vit_render_ln1gamma_chain_certified {Np1 D : ℕ} (ε β : ℝ) (γ : Vec 1) (xin : Vec (Np1 * D)) (Wq Wk Wv : Mat D D) (dQ dK dV : Vec (Np1 * D)) (lr : ℝ) : γ 0 - lr * rowLN_grad_gamma Np1 D ε (Mat.unflatten xin) (Mat.unflatten (vitCotLn1 Wq Wk Wv dQ dK dV)) = γ 0 - lr * ∑ o : Fin (Np1 * D), pdiv (fun (γ' : Vec 1) => Mat.flatten fun (r : Fin Np1) => layerNormForward D ε (γ' 0) β (Mat.unflatten xin r)) γ 0 o * vitCotLn1 Wq Wk Wv dQ dK dV o

LN₁ γ, chain-certified at vitCotLn1 — the THREE-WAY fan-in of the Q/K/V dense-backs (the structural wrinkle no prior net had), with the saved block input xin as the LN input.

theorem Proofs.vit_render_ln1beta_chain_certified {Np1 D : ℕ} (ε γsc : ℝ) (β : Vec 1) (xin : Vec (Np1 * D)) (Wq Wk Wv : Mat D D) (dQ dK dV : Vec (Np1 * D)) (lr : ℝ) : β 0 - lr * rowLN_grad_beta Np1 D (Mat.unflatten (vitCotLn1 Wq Wk Wv dQ dK dV)) = β 0 - lr * ∑ o : Fin (Np1 * D), pdiv (fun (β' : Vec 1) => Mat.flatten fun (r : Fin Np1) => layerNormForward D ε γsc (β' 0) (Mat.unflatten xin r)) β 0 o * vitCotLn1 Wq Wk Wv dQ dK dV o

LN₁ β, chain-certified.

theorem Proofs.vit_render_lnFgamma_chain_certified {N D nClasses : ℕ} (ε β : ℝ) (γ : Vec 1) (b2out : Vec ((N + 1) * D)) (Wcls : Mat D nClasses) (dy : Vec nClasses) (lr : ℝ) : γ 0 - lr * rowLN_grad_gamma (N + 1) D ε (Mat.unflatten b2out) (Mat.unflatten (vitCotFl N D nClasses Wcls dy)) = γ 0 - lr * ∑ o : Fin ((N + 1) * D), pdiv (fun (γ' : Vec 1) => Mat.flatten fun (r : Fin (N + 1)) => layerNormForward D ε (γ' 0) β (Mat.unflatten b2out r)) γ 0 o * vitCotFl N D nClasses Wcls dy o

Final-LN γ, chain-certified at vitCotFl (classifier-back scattered to row 0), with the saved block-2 output as the LN input.

theorem Proofs.vit_render_pos_chain_certified {ic H W P N D : ℕ} (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (N + 1) D) (img : Vec (ic * H * W)) (ε γ1 : ℝ) (Wq Wk Wv : Mat D D) (xin dQ dK dV cotH : Vec ((N + 1) * D)) (lr : ℝ) (i : Fin ((N + 1) * D)) : pos.flatten i - lr * vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH i = pos.flatten i - lr * ∑ j : Fin ((N + 1) * D), pdiv (fun (p : Vec ((N + 1) * D)) => patchEmbed_flat ic H W P N D Wc bc cls (Mat.unflatten p) img) pos.flatten i j * vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH j

pos-embed, chain-certified at the block-1 input cotangent vitCotXin — the cotangent the whole chain delivers at the embed output.

theorem Proofs.vit_render_cls_chain_certified {ic H W P N D : ℕ} (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (N + 1) D) (img : Vec (ic * H * W)) (ε γ1 : ℝ) (Wq Wk Wv : Mat D D) (xin dQ dK dV cotH : Vec ((N + 1) * D)) (lr : ℝ) (i : Fin D) : cls i - lr * cls_token_grad (vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH) i = cls i - lr * ∑ j : Fin ((N + 1) * D), pdiv (fun (cl : Vec D) => patchEmbed_flat ic H W P N D Wc bc cl pos img) cls i j * vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH j

CLS token, chain-certified — the row-0 slice of the block-1 input cotangent.

theorem Proofs.vit_render_patchW_chain_certified {ic H W P N D : ℕ} (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (N + 1) D) (img : Vec (ic * H * W)) (ε γ1 : ℝ) (Wq Wk Wv : Mat D D) (xin dQ dK dV cotH : Vec ((N + 1) * D)) (lr : ℝ) (d : Fin D) (c : Fin ic) (kh kw : Fin P) : Wc d c kh kw - lr * patchEmbed_weight_grad ic H W P N D img (vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH) d c kh kw = Wc d c kh kw - lr * ∑ o : Fin ((N + 1) * D), pdiv (fun (v : Vec (D * ic * P * P)) => patchEmbed_flat ic H W P N D (Kernel4.unflatten v) bc cls pos img) Wc.flatten (finProdFinEquiv (finProdFinEquiv (finProdFinEquiv (d, c), kh), kw)) o * vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH o

Patch kernel, chain-certified — the patch-grid reduce at the block-1 input cotangent.

theorem Proofs.vit_render_patchb_chain_certified {ic H W P N D : ℕ} (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (N + 1) D) (img : Vec (ic * H * W)) (ε γ1 : ℝ) (Wq Wk Wv : Mat D D) (xin dQ dK dV cotH : Vec ((N + 1) * D)) (lr : ℝ) (i : Fin D) : bc i - lr * patchEmbed_bias_grad N D (vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH) i = bc i - lr * ∑ o : Fin ((N + 1) * D), pdiv (fun (b' : Vec D) => patchEmbed_flat ic H W P N D Wc b' cls pos img) bc i o * vitCotXin ε γ1 Wq Wk Wv xin dQ dK dV cotH o

Patch bias, chain-certified.