EfficientNet-B0's stem and head endpoint ties #
The two concrete endpoints the sixteen-block whole-net tie (EfficientNetFullWholeBackCertifiedTie)
stands on: stemBBack_eq_vjp_backward (at the XLA-SAME phase every shipped B0 artifact emits) and
headFwdBBack_eq_vjp_backward. Each is one rw of a per-example leaf tie and then rfl: the
batched stage's VJP is vjpComp-built, so its backward already reduces to the composition of the
stage backwards, and batchMap's VJP reduces to the leaf backward applied row-wise.
batchMapHasVJP's transport does not block the reduction. It is built as
(batchMap_eq_rowwiseFlat f).symm ▸ HasVJPMat.toHasVJP (rowwiseHasVJPMat …), and an Eq.mpr
can block .backward from reducing. It does not here: the transported equation holds by
funext … ; rfl, and proof irrelevance is definitional in Lean, so .backward reduces straight
through the ▸ to the leaf backward applied row-wise — checked as a bare rfl, and every tie below
relies on it.
The STEM tie. The hand-written batchMap (flatConvStride2XlaBack) ∘ bnBack ∘ swishBack
IS stemB's certified backward. One rw of the odd-phase leaf tie, then rfl — the
stage's VJP is vjpComp-built so its backward is already the composition, and the leaf's
backward is input-independent (a convolution is linear), so the row-wise batchMap lift
matches at every saved input.
The HEAD tie. The four-stage hand chain batchMap (convFlatBack) ∘ bnBack ∘ swishBack ∘ batchMap gapBack ∘ batchMap (dense Wᵀ 0) IS headFwdB's certified backward. gapBack needs
no rewrite: it is definitionally the global-average-pool VJP's backward.