xHessianEntry
plain-language theorem explainer
The xHessianEntry definition supplies the explicit (i,j) entry of the Hessian for the J-cost on positive n-vectors, formed as the symmetrized aggregate factor times the product of direction components minus the antisymmetrized factor times the diagonal correction. Curvature analysts in the Recognition Science cost framework cite this when extracting eigenvalues or stability conditions from the second variation. It is realized as a direct algebraic term that composes the upstream aggregate, xDirection, and xDiagonalCorrection definitions.
Claim. For positive vectors $α, x ∈ ℝ^n$ the $(i,j)$-entry of the Hessian of the $J$-cost is given by $(R + R^{-1})/2 · d_i d_j - (R - R^{-1})/2 · c_{ij}$, where $R = exp(∑_k α_k log x_k)$, $d_k = α_k / x_k$, and $c_{ij} = δ_{ij} α_i / x_i^2$.
background
The module records positive-coordinate Hessian formulas for the multi-component reciprocal cost. The aggregate computes the exponential of the weighted log-sum, $R = exp(∑ α_i log x_i)$, which encodes the overall positive scale. Vec n is the type of coordinate functions Fin n → ℝ. The direction extracts the active components α_i / x_i while the diagonal correction supplies the second-derivative adjustment α_i / x_i² on the diagonal and zero off-diagonal.
proof idea
The definition is a direct term that multiplies the symmetrized aggregate factor by the product of the two direction components and subtracts the antisymmetrized factor times the diagonal correction. It applies the definitions of aggregate, xDirection, and xDiagonalCorrection with no additional lemmas or tactics.
why it matters
This entry is the primitive block for xHessianMatrix and its specializations (diagonal, off-diagonal, and zero-cost degeneracy where the matrix collapses to the outer product of the direction vector). It fills the general formula in the positive-coordinate Hessian development, enabling the 2×2 determinant factorization and nondegeneracy criteria away from the neutral locus. In the Recognition framework it supports second-variation analysis of the J-cost that underpins the forcing chain from T5 J-uniqueness onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.