xDiagonalCorrection
plain-language theorem explainer
Researchers analyzing the Hessian of the n-dimensional reciprocal cost cite this definition for the explicit diagonal correction term. It isolates the contribution that appears only on matching indices when differentiating twice with respect to the x-coordinates. The definition is realized by a direct conditional expression returning the scaled inverse-square term on the diagonal and zero elsewhere.
Claim. The diagonal correction term in the x-coordinate Hessian of the n-dimensional cost is given by $d_{ij} = 1$ if $i=j$ and $d_{ij}=0$ otherwise, with the nonzero value equal to $a_i / x_i^2$.
background
The module supplies explicit Hessian formulas for the multi-component reciprocal cost in positive coordinates. The underlying cost is the n-dimensional JcostN, which composes the J-logarithm with the componentwise logarithm of the coordinate vector. Vec n denotes the type of n-tuples of reals, realized as functions from Fin n to ℝ. The general Hessian entry combines a rank-one update built from the aggregate R = aggregate α x with the present diagonal correction.
proof idea
The definition is realized by a direct conditional expression: return α i / (x i)^2 when the indices coincide and return 0 otherwise. No lemmas or tactics are invoked; the expression is used verbatim when unfolding xHessianEntry in the downstream results.
why it matters
The definition supplies the explicit term required to construct xHessianEntry and its specializations (xHessianEntry_diag, xHessianEntry_offDiag, xHessianEntry_zero_cost). These in turn support the 2×2 determinant factorization and the degeneracy statement on the neutral locus where aggregate α x = 1. Within the Recognition framework it contributes the local second-derivative geometry needed for stability analysis near the phi-forced fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.