xHessianEntry_zero_cost
plain-language theorem explainer
Researchers working on the geometry of the multi-component J-cost cite this degeneracy result for the Hessian on the unit aggregate surface. When the exponential aggregate R equals one, every entry of the x-Hessian reduces to the product of the corresponding direction components, yielding a rank-one outer product. The argument substitutes the unit condition directly into the general entry formula and splits on index equality.
Claim. Let $R = R(x) = exp(sum alpha_i log x_i)$. If $R=1$, then the $(i,j)$-entry of the $x$-coordinate Hessian of the $n$-dimensional cost equals $(alpha_i / x_i) (alpha_j / x_j)$.
background
The module records explicit formulas for the $x$-coordinate Hessian of the multi-component reciprocal cost. The aggregate $R$ is defined as the exponential of the dot product of the weight vector alpha with the componentwise logarithm of the positive vector x. The direction vector has components alpha_i / x_i. The diagonal correction term is alpha_i / x_i squared when the indices coincide and zero otherwise. The general Hessian entry combines these with the coefficients (R + R inverse)/2 and (R - R inverse)/2.
proof idea
The term proof unfolds the definitions of the Hessian entry, the direction vector, and the diagonal correction, rewrites using the hypothesis that the aggregate equals one, then performs case analysis on whether the indices are equal and simplifies each branch.
why it matters
This supplies the zero-cost degeneracy statement referenced in the module documentation on positive-coordinate Hessian formulas. It supports the subsequent closed determinant factorization for the two-by-two case and the nondegeneracy criterion away from the neutral locus. In the Recognition framework the reduction illustrates how the cost Hessian becomes rank-one precisely on the surface where the aggregate equals one, consistent with the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.