hessianAt_factor
plain-language theorem explainer
Researchers modeling the n-dimensional reciprocal cost in log-coordinates cite this factorization to reduce the Hessian to a scalar multiple of the outer product α ⊗ α. The result follows directly from the entry-wise definition of the Hessian and the weighted dot product. The proof proceeds by extensionality on the matrix entries followed by algebraic simplification.
Claim. For vectors $α, t ∈ ℝ^n$, the Hessian matrix at $(α, t)$ satisfies $H_{ij} = cosh(α · t) · α_i α_j$ for all indices $i, j$.
background
Vec n denotes n-component real vectors as maps from Fin n to ℝ. The weighted aggregate dot α t is the sum ∑ α_i t_i over the n components. hessianAt α t is the matrix whose (i, j) entry is given by hessianEntry α t i j, which expands to α_i α_j cosh(dot α t). The auxiliary hessianMatrix α is the rank-one outer product with entries α_i α_j.
proof idea
The proof applies functional extensionality to equate the two matrix-valued functions on every pair of indices i, j. It unfolds the definitions of hessianAt, hessianEntry, and hessianMatrix. The ring tactic then verifies the scalar multiplication identity by direct algebraic cancellation.
why it matters
This result confirms that the full Hessian is a scalar multiple of the equilibrium outer-product model, matching the module's description of the n-dimensional reciprocal cost. In the Recognition Science framework it supplies the explicit rank-one structure that follows from dependence on the single aggregate dot α t. No downstream theorems are listed, but the factorization supports second-order simplifications in cost and metric calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.