⭐⭐ efficientnetInputGradB_full IS the certified whole-net PAPER EfficientNet-B0 gradient #

EfficientNetWholeBackCertifiedTie.lean closed this for the three-block representative. This file closes it for the net efficientnetForwardB_full actually is: all sixteen MBConv blocks, the T6 row of planning/archive/proofs_tier_to_paper_nets.md §3.3(c) — and closes it one step further than the representative's, against the concrete efficientnetForwardB_full_has_vjp and, through efficientnetForwardB_full_has_vjp_correct, against the Jacobian of the committed nested-application forward itself.

Nothing here is new mathematics. The two endpoint stage ties (stemBBack_eq_vjp_backward, headFwdBBack_eq_vjp_backward) are the representative's, reused verbatim 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. As on B0's representative and unlike MobileNetV2's, there is no smooth point: swish and the SE sigmoid are differentiable everywhere.

The three pieces #

1. efficientnetB_full_has_vjp — the generic eighteen-stage apex head ∘ b16 ∘ … ∘ b1 ∘ stem, seventeen vjp_comps 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. efficientnetInputGradB_full_eq_efficientnetB_full_vjp — the tie with the stem and head concrete and the sixteen blocks opaque: unfold, two rws, rfl.
3. efficientnetInputGradB_full_eq_efficientnetForwardB_full_vjp — the tie instantiated at the sixteen concrete blocks (mbNoExpW, mbStridedW, mbResidW, mbExpW at B0Weights's widths) and carried to efficientnetForwardB_full_has_vjp by HasVJP.backward_unique: two witnesses for one map have one backward, so the tactic-built whole-net witness never has to be unfolded. ⭐ That is what the representative's file could not do — it stopped at a ▸-transported _committed witness that the kernel could not reduce through — and the difference is not depth but backward_unique, which was proved for ConvNeXt-T's tie. efficientnetInputGradB_full_correct then reads the result through efficientnetForwardB_full_has_vjp_correct, whose proof IS the shape check efficientnetForwardB_full_eq_chain: the hand-written chain is the pdiv-contracted Jacobian of efficientnetForwardB_full at every input, every cotangent and every pixel.

⭐ General N. bnBatchLA_has_vjp exists at every batch size, so the tie does; this is the certified chain's property, not the float chain's (EfficientNetBackFloatBudget.lean's number is at N = 1 for a reason that does not apply here).

⛔ No backward number at sixteen blocks. b0_full_back_chain's certified window at the shipped leaves is 9.112·10²⁶⁴⁸; the float file this imports says why it is not written down.