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 vjp_comp-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.
⭐ batchMap_has_vjp's transport does not block the reduction, and the planning note that
said it would is withdrawn. It is built as (batchMap_eq_rowwiseFlat f).symm ▸ hasVJPMat_to_hasVJP (rowwise_has_vjp_mat …), and §5's standing trap is that an Eq.mpr blocks
.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 vjp_comp-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.