det_xHessianMatrix2_formula
plain-language theorem explainer
The formula computes the determinant of the 2 by 2 x-coordinate Hessian for the reciprocal cost model as an explicit rational function of the aggregate R. Cost analysts examining degeneracy in the 2D case cite it to identify the neutral locus where the determinant vanishes. The proof is a direct reduction that unfolds the specialized matrix definition and applies the parameterized determinant formula together with aggregate positivity.
Claim. Let $R = e^{a log x + b log y}$. For $x ≠ 0$ and $y ≠ 0$, the determinant of the 2×2 x-coordinate Hessian satisfies $det(H) = -ab(R-1)(R+1)(R^2(a+b-1)+a+b+1)/(4R^2 x^2 y^2)$.
background
The module records positive-coordinate Hessian formulas for the multi-component reciprocal cost. The aggregate is the exponential $R = exp(α · log x)$ of the dot product between the coefficient vector and the log-coordinate vector. The 2×2 x-Hessian matrix is obtained by specializing the general parameterized matrix xHessianMatrix2OfR to this concrete aggregate value. Upstream, the parameterized determinant theorem supplies the closed form for arbitrary nonzero R, while aggregate_pos guarantees the strict positivity required to discharge the non-zero hypothesis on R.
proof idea
The proof dsimps the definition of xHessianMatrix2 to substitute the aggregate into the parameterized matrix, then invokes det_xHessianMatrix2OfR_formula with the concrete R together with the positivity theorem aggregate_pos to satisfy the nonzero condition on R.
why it matters
It supplies the explicit determinant used by the zero-cost degeneracy theorem, which shows the determinant vanishes on the neutral locus aggregate = 1, and by the generic nondegeneracy theorem away from that locus and the secondary discriminant factor. This completes the 2×2 specialization of the Hessian formulas, enabling analysis of degeneracy loci in the cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.