det_xHessianMatrix2_zero_cost
plain-language theorem explainer
When the exponential aggregate of two positive coordinates equals one, the determinant of their two-by-two x-coordinate Hessian vanishes. Workers on degeneracy loci in reciprocal cost models cite this to locate neutral points where the Hessian loses rank. The proof is a one-line rewrite of the closed determinant formula followed by simplification under the aggregate-equals-one hypothesis.
Claim. Let $R = e^{a log x + b log y}$. If $R=1$, $x≠0$ and $y≠0$, then the determinant of the $2×2$ Hessian matrix built from the positive-coordinate reciprocal cost is zero.
background
The module records explicit Hessian formulas for the multi-component reciprocal cost in positive coordinates. The aggregate function is the exponential $R(α,x)=exp(∑α_i log x_i)$, which serves as the weighted product that normalizes the cost. The two-by-two Hessian xHessianMatrix2 is obtained by specializing the general entry formula to the vector pair (a,b) and (x,y) with R computed from those components. The local setting is the specialization of the general n-dimensional Hessian to the 2×2 case, yielding a closed determinant factorization together with the zero-cost degeneracy statement.
proof idea
One-line wrapper that applies det_xHessianMatrix2_formula to obtain the explicit determinant expression and then simplifies under the hypothesis that aggregate(vec2 a b, vec2 x y)=1.
why it matters
This theorem supplies the zero-cost degeneracy statement referenced in the module documentation for the 2×2 positive-coordinate Hessian. It identifies the neutral locus aggregate=1 as the place where the Hessian determinant vanishes, thereby supporting the subsequent nondegeneracy criterion away from that locus. In the Recognition framework it marks a concrete degeneracy surface inside the cost domain before higher-dimensional or dynamical extensions are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.