hessianMatrix
plain-language theorem explainer
The definition supplies the rank-one outer-product matrix with entries α_i α_j as the equilibrium Hessian model for the n-dimensional reciprocal cost. Workers on the metric tensor in log-coordinates cite this when the second variation factors through a single aggregate dot product. The body is the direct pointwise product that realizes α ⊗ α without further computation.
Claim. For a vector α ∈ ℝ^n the equilibrium Hessian matrix is defined by H_{ij} = α_i α_j.
background
Vec n denotes the space of n-component real vectors, realized as functions from Fin n to ℝ. The module treats the n-dimensional cost in log-coordinates, where the cost depends only on the weighted aggregate dot α t. Consequently the Hessian is rank one and equals the outer product α ⊗ α. Upstream, Vec is imported from Core as the coordinate functions for the logarithmic aggregate.
proof idea
One-line definition that sets the (i,j) entry to the product α i * α j, directly implementing the outer-product model.
why it matters
This definition is the base model used by hessianAt_zero to recover the Hessian at the origin and by hessianAt_factor to scale it by cosh(dot α t). It also equates to the metric entry at equilibrium in Metric.lean. In the Recognition framework it supplies the rank-one structure required for the n-dimensional extension of the cost Hessian, consistent with the single aggregate dependence in log-space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.