hessianEntry
plain-language theorem explainer
The definition supplies the (i,j) entry of the Hessian for the n-dimensional log-coordinate cost JlogN as the product α_i α_j cosh(α · t). Researchers extending the Recognition Science reciprocal cost to higher dimensions cite it when building the metric tensor or verifying rank-one structure in log-space. It is introduced as the direct algebraic expression obtained by twice differentiating the cost, which depends only on the scalar aggregate dot α t.
Claim. The $(i,j)$-entry of the Hessian of the log-coordinate cost $J$ at weights $α$ and state $t$ is $α_i α_j cosh(α · t)$, where $α,t ∈ ℝ^n$ and $·$ is the weighted inner product $∑_k α_k t_k$.
background
In the n-dimensional reciprocal cost model the cost in log-coordinates is a function of the single scalar $u = α · t$. Its Hessian is therefore rank one and factors as the outer product $α ⊗ α$ scaled by the second derivative of the cost with respect to $u$. The module supplies the coordinate formulas that replace the missing private Hessian file referenced by the Metric submodule, so that the metric tensor can be read off directly from these entries.
proof idea
One-line definition that encodes the second mixed partial of the cost. Because the cost depends only on the aggregate $u = dot α t$, the first derivative with respect to any coordinate brings down a factor α_i and the second derivative produces the cosh(u) factor from the known second derivative of the underlying J function.
why it matters
This entry is the primitive used by hessianAt, hessianAt_factor, and metricEntry. It realizes the structural claim that the Hessian remains a scalar multiple of the equilibrium outer-product model, which is the key property allowing the n-dimensional cost to stay tractable. The definition closes the gap left by the absent private file and feeds the downstream theorems that the Hessian action is always parallel to α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.