xHessianEntry_offDiag
plain-language theorem explainer
Off-diagonal entries of the x-coordinate Hessian for the multi-component reciprocal cost equal the scaled product of direction vectors, with the correction term vanishing. Researchers deriving the second variation of J-costN in n dimensions cite this when assembling the full Hessian matrix or its determinant in the 2x2 specialization. The proof is a direct unfolding of the general entry definition followed by simplification that drops the zero correction under the i ≠ j hypothesis.
Claim. Let $R = R(α, x) = exp(∑_k α_k log x_k)$ denote the exponential aggregate. For $i ≠ j$, the Hessian entry satisfies $H_{ij} = [(R + R^{-1})/2] ⋅ (α_i / x_i) ⋅ (α_j / x_j)$.
background
The module records explicit formulas for the Hessian of the log-coordinate cost JcostN in positive coordinates. The aggregate R(α, x) is defined as exp(α · logVec x), the exponential of the weighted sum of logarithms. The direction vector has components α_i / x_i. The general Hessian entry is [(R + R^{-1})/2] times the product of directions minus [(R - R^{-1})/2] times the diagonal correction term, which is α_i / x_i² when i = j and zero otherwise. This local setting specializes the general entry to obtain closed forms for the 2 × 2 determinant and nondegeneracy statements away from the neutral locus.
proof idea
One-line wrapper that unfolds the definitions of xHessianEntry and xDiagonalCorrection, then applies simp with the hypothesis i ≠ j to eliminate the correction term.
why it matters
This supplies the off-diagonal case needed to assemble the full xHessianMatrix and its 2 × 2 determinant factorization in sibling declarations. It completes the explicit Hessian formulas for the multi-component reciprocal cost, supporting later nondegeneracy criteria and the closed determinant expression. In the Recognition framework it contributes to the cost analysis that precedes the phi-ladder mass formulas and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.