efficientnetInputGradBFull is the certified whole-net paper EfficientNet-B0 gradient #

The whole-net backward tie for efficientnetForwardBFull, all sixteen MBConv blocks, against the concrete efficientnetForwardBFullHasVJP and, through efficientnetForwardBFullHasVJP_correct, against the Jacobian of the committed nested-application forward itself.

The stem and head endpoint ties (stemBBack_eq_vjp_backward, headFwdBBack_eq_vjp_backward) are EfficientNetWholeBackCertifiedTie.lean's, used at the paper widths (head 320→1280 at 7×7); the sixteen blocks stay opaque in the tie, entering as HasVJP witnesses whose .backward is what the reverse chain's block slots are pinned to, so the composition is checked between variables. Unlike MobileNetV2's tie there is no smooth point: swish and the SE sigmoid are differentiable everywhere, and the only hypothesis is w.EpsPos. The forward has no drop-path and no classifier dropout, and is in exact arithmetic.

The three pieces #

1. efficientnetBFullHasVJP — the generic eighteen-stage apex head ∘ b16 ∘ … ∘ b1 ∘ stem, seventeen vjpComps and nothing else, and opaqueA0 … A16, one prefix def per running activation (the MobileNetV2 paper file's answer to the quadratic writing of nested applications; plain defs so the closing rfl sees through them).
2. efficientnetInputGradBFull_eq_efficientnetB_full_vjp — the tie with the stem and head concrete and the sixteen blocks opaque: unfold, two rws, rfl.
3. efficientnetInputGradBFull_eq_efficientnetForwardB_full_vjp — the tie instantiated at the sixteen concrete blocks (mbNoExpW, mbStridedW, mbResidW, mbExpW at B0Weights's widths) and carried to efficientnetForwardBFullHasVJP by HasVJP.backward_unique: two witnesses for one map have one backward, so the tactic-built whole-net witness never has to be unfolded. efficientnetInputGradBFull_correct then reads the result through efficientnetForwardBFullHasVJP_correct, whose proof IS the shape check efficientnetForwardBFull_eq_chain: the hand-written chain is the pdiv-contracted Jacobian of efficientnetForwardBFull at every input, every cotangent and every pixel.

General N. bnBatchLAHasVJP exists at every batch size, so the tie does.