vitInputGradKB is the certified whole-net ViT gradient at a batch #
ViTWholeBackCertifiedTie.lean proves for one image that vitInputGradK, the reverse of
vitForwardKV over that image's N + 1 tokens, is the certified gradient. The batched step tie
(ViTStepTieGB.lean) states every activation as StableHLO.batchMap B of the per-example prefix
and every cotangent as batchMapAux B of the per-example chain, because no ViT op couples
examples. This file proves the same at that index: the five-stage batched chain vitInputGradKB
(ViTBackChains.lean) is the certified gradient of batchMap B vitForwardKV at every batch x,
for every B. The forward vitForwardKV has no drop-path and is in exact arithmetic.
ViT is smooth everywhere: every stage has a global HasVJP, so its batched witness is
batchMapHasVJPAt (the field-by-field lift, BatchMapVJPAt.lean) over HasVJP.toHasVJPAt at
each row. The only hypothesis is 0 < ε; there is no smooth-point condition.
batchMap_comp(BatchMapVJPAt.lean, shared with ConvNeXt's batched tie) —batchMap B (g ∘ f) = batchMap B g ∘ batchMap B f, the lemma the shape check needs and the reason the chain saves its activations stage by stage: the two spellings agree only up tofinProdFinEquiv.symm_apply_apply, which is notrfl.- The batched leaf ties. The patch-embed stage needs none (its backward is
rfl); the other three arebatchMapAux_eq_batchMapHasVJPAt(the head: itsbatchMapform, afterbatchMap_comp) over the per-example tie at each row (vitTowerBackK_eq_vjp,vitFinalLNBack_eq_vjp,vitHeadBack_eq_classifier_vjp). vitKVBHasVJPAt— the four-stage apex, threevjpCompDiffAts over the batched stage witnesses — andvitInputGradKB_eq_vitKVB_vjp, the tie: three leaf rewrites, thenrfl.vitForwardKVB_eq_chain— the shape check: the four batched stages compose tobatchMap B vitForwardKV, byvitForwardKV_eq_chainand threebatchMap_comps — andvitInputGradKB_eq_batchMap_vitForwardKV_vjp, the tie carried to the committed GLOBAL witnessbatchMapHasVJP (vitForwardKV …)throughHasVJPAt.backward_unique_of_eq(batchMapHasVJPis▸-transported, so its.backwarddoes not reduce), plus the∑ pdivreading.vitTinyInputGradB_eq_vitTiny_vjp— the capstone at ViT-Tiny's literal dims, the batchBand the class countnClsbinders.
The batched tower witness at v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched final-LayerNorm witness at v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched classifier-head witness at v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched tower tie. batchMapAux B of the depth-k tower backward at the batched
saved input IS the lift's backward: vitTowerBackK_eq_vjp at each row.
The batched head tie. batchMap B of the CLS scatter after batchMap B of the free dense
backward IS the lift's backward at any saved v (the head is linear): fuse the two lifts by
batchMap_comp, then vitHeadBack_eq_classifier_vjp at one example's row.
The batched whole-net witness, four batched stages composed by vjpCompDiffAt, each
at the batched saved activation the chain uses (vitSavedPEB, vitSavedBodyB).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched tie. vitInputGradKB — the five-stage batched chain, every slot a lift of
the per-example backward at the batched saved activation — is the backward of
vitKVBHasVJPAt. Three leaf rewrites (tower, final LN, head), then rfl: the patch-embed leaf
is definitional.
The shape check. The four batched stages the apex is stated at compose to
batchMap B vitForwardKV, the committed per-example forward lifted whole: the per-example
shape check vitForwardKV_eq_chain and three batchMap_comps.
vitForwardKV is differentiable everywhere (only 0 < ε): the four stage lemmas composed.
The batched apex at the global witness. vitInputGradKB is
(batchMapHasVJP (vitForwardKV …) …).backward x — the certified gradient of the drop-free
per-example forward lifted over B examples, under 0 < ε. Carried from the chain-shaped apex
by HasVJPAt.backward_unique_of_eq along the shape check.
The batched apex, read as the Jacobian. vitInputGradKB is the pdiv-contracted Jacobian
transpose of batchMap B vitForwardKV, at EVERY batch and EVERY cotangent. Only 0 < ε.
ViT-Tiny's batched whole-net backward tie.
vitInputGradKB_eq_batchMap_vitForwardKV_vjp at the exact vitTiny spec
(3×224×224, 16×16 patches, 196 + CLS tokens, D = 192 = 3 × 64, MLP 768, 12 distinct
blocks, vector-[D] LayerNorm), at any class count nCls (10 for the Imagenette spec, 1000
for the vitin_* ImageNet artifacts) and a variable batch B (the vitin_* artifacts run 32,
128 or 256 per device; 512 is the global batch of the 128x4 runs). The forward is the
drop-free vitForwardKV in exact arithmetic; the *drop* artifacts compute another function.
The batched peers of the other nets include r34InputGradB_eq_r34B_full_vjp and
mnv2InputGradB_eq_mobilenetv2B_full_vjp.