xHessianMatrix
plain-language theorem explainer
The definition supplies the full x-coordinate Hessian matrix for the n-dimensional reciprocal cost as a map from index pairs to reals. Analysts of the J-cost curvature in Recognition Science cite it when assembling the general-dimensional second-derivative operator before specializing to low dimensions. It is realized as a one-line wrapper that delegates every entry to the precomputed xHessianEntry formula.
Claim. Let $R = $ aggregate of the positive weights $α$ and coordinates $x$. Define the matrix $H(α,x)$ by $H_{ij} = ((R + R^{-1})/2) · d_i · d_j - ((R - R^{-1})/2) · c_{ij}$, where $d_k$ is the $k$-th direction factor and $c_{ij}$ is the diagonal correction term for the given vectors.
background
Vec is the abbreviation for n-component real vectors, written as functions from Fin n to ℝ. The upstream xHessianEntry records the explicit (i,j) entry of the x-coordinate Hessian of the multi-component reciprocal cost JcostN, expressed through the aggregate R, the direction factors, and the diagonal correction. The module records positive-coordinate Hessian formulas for this cost; the general entry is written in terms of R and then specialized to the 2×2 case for determinant factorization and nondegeneracy statements.
proof idea
One-line wrapper that applies xHessianEntry to each pair of indices i and j, returning the resulting real value as the matrix entry.
why it matters
This definition assembles the general n-dimensional x-Hessian matrix that precedes the 2×2 specializations appearing among its siblings. It supplies the concrete operator needed to study curvature of the reciprocal cost away from the neutral locus, supporting later nondegeneracy criteria in the cost domain of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.