hessianAt_zero
plain-language theorem explainer
The theorem shows that the n-dimensional Hessian operator applied to the zero log-state recovers exactly the outer-product matrix with entries given by products of the weight coordinates. Workers on reciprocal-cost models in log-space would invoke this identity when linearizing the second-derivative structure around equilibrium. The argument reduces the matrix equality to entrywise comparison and simplifies via the zero-state entry lemma.
Claim. Let $n$ be a natural number and let $α ∈ ℝ^n$ be a vector of weights. Then the Hessian of the cost at the zero state equals the outer-product matrix, i.e., $H(α, 0) = α α^T$ where the right-hand side has entries $α_i α_j$.
background
In the n-dimensional extension of the reciprocal cost the state is a vector $t ∈ ℝ^n$ in log-coordinates and the cost depends only on the single weighted aggregate $α · t$. Consequently the Hessian is rank-one and factors through the outer product of the weight vector $α$. Vec n is the type of n-component real vectors realized as functions Fin n → ℝ. The equilibrium Hessian model is defined directly as the matrix whose (i,j) entry is $α_i α_j$. The zero-state entry lemma states that substituting the zero function into the entry formula yields precisely $α_i α_j$.
proof idea
The proof is a one-line wrapper. It applies function extensionality to reduce the matrix equality to entrywise equality, then simplifies using the definitions of hessianAt and hessianMatrix together with the zero-entry theorem.
why it matters
This identity closes the reduction of the second-derivative structure at equilibrium to the explicit outer-product form required by the rank-one property of the log-cost. It supports the n-dimensional cost module that replaces the missing private file referenced by Metric.lean. No downstream uses are recorded yet, but the result is a direct consequence of the zero-state entry simplification and feeds the broader Hessian calculus in the cost domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.