applyTensor
plain-language theorem explainer
applyTensor defines the coordinate action of an n by n real tensor H on a vector v, returning the vector whose i-th component is the sum over j of H i j times v j. Researchers modeling the n-dimensional reciprocal cost Hessian cite it when reducing matrix-vector products in log coordinates. The implementation is a direct finite summation over Fin n with no auxiliary lemmas.
Claim. Let $H : (Fin n) → (Fin n) → ℝ$ be a tensor and $v : Vec n$ an n-component real vector. The map sends $v$ to the vector whose $i$-th component equals $∑_j H_{ij} v_j$.
background
The module supplies Hessian formulas for the n-dimensional reciprocal cost. In log-coordinates the cost depends only on the single weighted aggregate dot α t, so the Hessian is rank one and factors through the outer product α ⊗ α. Vec n is the abbreviation Fin n → ℝ for n-component real vectors. The shifted cost H(x) = J(x) + 1 satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Upstream results include the J-cost structure from PhiForcingDerived and the ledger factorization from DAlembert.
proof idea
This is a one-line definition that implements the tensor-vector product by explicit coordinate summation: for each output index i the component is ∑_j H i j * v j. No lemmas are applied; the construction is the primitive matrix-vector product.
why it matters
This definition supplies the coordinate implementation invoked by applyHessian to produce the vector applyHessian α t v and by applyHessian_eq_direction to prove the output is parallel to α. It realizes the rank-one Hessian structure arising from dependence on the scalar dot product, consistent with the eight-tick octave and D = 3 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.