Forward-over-reverse mode computes the Hessian-vector product

By [F4], the input reverse accumulator is the function $x\mapsto \mathrm{grad}f(x)$. Since $f$ is $C^2$ by [F2] under the primitive hypotheses in [F1], its directional derivative at $x$ exists. By [F3], the forward recurrence supplies every primitive-input direction ${\dot{z}}_{pa}=D{z}_{pa}(x)v$.

At a node $j$, the exact reverse contribution to parent slot $i$ is $A^T{\bar{z}}_j$. Since each primitive is $C^2$, $A$ is $C^1$; the finite reverse recurrence is therefore differentiable, as it consists of sums and bounded bilinear matrix-vector products of $C^1$ maps. Differentiate this matrix-vector product along $x+tv$. The product rule [F6] gives $A^T{\dot{\bar{z}}}_j+(DA[{\dot{z}}_{pa}]{)}^T{\bar{z}}_j$, exactly the second recurrence in [F5]. Reverse topological induction therefore shows that every ${\dot{\bar{z}}}_i$ equals the directional derivative of the corresponding exact reverse accumulator. If the scalar output is an input coordinate, its seeded gradient is the constant coordinate vector and the initialized tangent-cotangent remains zero, as this recurrence also gives.

At the inputs, step 2.1 identifies the returned vector with $D(\mathrm{grad}f)(x)v$, which by definition is $H_f(x)v$.