det_xHessianMatrix2OfR_formula
plain-language theorem explainer
The formula supplies an explicit closed-form determinant for the 2-by-2 positive-coordinate Hessian matrix expressed through the aggregate parameter R. Researchers analyzing the reciprocal cost Hessian in the Ndim setting cite it to obtain the factored expression needed for nondegeneracy checks. The proof is a direct algebraic reduction: unfold the matrix definition, clear denominators via field_simp, and verify the identity by ring.
Claim. Let $H$ be the $2×2$ matrix with entries $H_{11}=a/(2x^2)·((a-1)R+(a+1)R^{-1})$, $H_{12}=H_{21}=ab/(2xy)·(R+R^{-1})$, $H_{22}=b/(2y^2)·((b-1)R+(b+1)R^{-1})$. Then, for $x≠0$, $y≠0$, $R≠0$, $det(H)=-(ab(R-1)(R+1)(aR^2+bR^2-R^2+a+b+1))/(4R^2 x^2 y^2)$.
background
The module records explicit Hessian formulas for the multi-component reciprocal cost restricted to positive coordinates. The aggregate $R$ stands for the positive sum $R=aggregate(α,x)$ that appears in the general entry formula. The definition xHessianMatrix2OfR constructs the concrete $2×2$ matrix whose diagonal blocks contain weighted combinations of $R$ and $R^{-1}$ scaled by the component weights $a$ and $b$, while the off-diagonal blocks are proportional to $ab(R+R^{-1})$ divided by the product of the coordinates.
proof idea
The proof applies simp to unfold xHessianMatrix2OfR together with the 2×2 determinant formula. It then invokes field_simp under the three nonzero hypotheses to clear all denominators, reducing the claim to a polynomial identity. The final ring tactic expands both sides and confirms cancellation.
why it matters
This theorem supplies the factored determinant that the downstream result det_xHessianMatrix2_formula obtains by substituting the concrete aggregate $R=aggregate(vec2 a b)(vec2 x y)$. It completes the 2×2 specialization path described in the module documentation, furnishing the closed-form expression required for later nondegeneracy arguments inside the cost domain of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.