xHessianEntry_diag
plain-language theorem explainer
The diagonal entries of the Hessian for the multi-component reciprocal cost equal an explicit formula linear in the aggregate R and quadratic in the weights α. Analysts computing curvature or stability of the J-cost in n dimensions would cite this when specializing the general entry formula. The identity follows from direct substitution of the direction and diagonal-correction definitions followed by algebraic simplification.
Claim. For vectors α, x ∈ ℝⁿ and index i, the diagonal Hessian entry satisfies H_{ii}(α,x) = (α_i / (2 x_i²)) ⋅ ((α_i − 1) R + (α_i + 1) R⁻¹), where R = exp(∑_j α_j log x_j).
background
The module records explicit Hessian formulas for the multi-component reciprocal cost on positive coordinates. The aggregate R = exp(∑ α_i log x_i) is the exponential of the weighted log-dot product. The direction vector has components α_i / x_i and the diagonal correction is α_i / x_i² on the matching indices. The general entry combines a rank-one term built from R + R⁻¹ with a diagonal subtraction of the correction scaled by (R − R⁻¹)/2.
proof idea
The proof unfolds the definitions of xHessianEntry, xDirection and xDiagonalCorrection, then applies simp and ring to reduce the resulting algebraic expression.
why it matters
This identity supplies the concrete diagonal formula needed to assemble the full x-Hessian matrix and to derive its determinant factorization in the 2 × 2 case. It supports the zero-cost degeneracy statement that the Hessian collapses to a rank-one outer product when R = 1. Within Recognition Science the result contributes to the second-variation analysis of the J-cost that underlies stability criteria on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.