xHessianMatrix2OfR
plain-language theorem explainer
The definition supplies the explicit 2 by 2 Hessian matrix for positive x-coordinates in the reciprocal cost model, expressed directly in terms of weights a b, coordinates x y, and aggregate R. Analysts deriving the determinant factorization or checking nondegeneracy in two dimensions cite this construction. It is a direct matrix literal that assembles the four entries from the general Hessian formula without invoking further lemmas.
Claim. The 2×2 Hessian matrix for the positive coordinates is defined by the entries $H_{11} = a((a-1)R + (a+1)R^{-1})/(2x^2)$, $H_{12}=H_{21}=ab(R+R^{-1})/(2xy)$, $H_{22}=b((b-1)R+(b+1)R^{-1})/(2y^2)$, where $R$ is the exponential aggregate of the weights and coordinates.
background
In the Cost.Ndim.XCoordinates module the positive-coordinate Hessian is expressed through the aggregate function. The aggregate is defined as the exponential of the dot product of the log-coordinates with the weights: $R=exp(∑α_i log x_i)$. This module specializes the general entry formulas to the 2×2 case, allowing closed-form expressions for the determinant and degeneracy conditions away from the neutral locus.
proof idea
Direct definition that populates the 2×2 matrix with the four explicit entries derived from the general xHessianEntry formula. The (1,1) and (2,2) diagonals scale the weighted combination of R and R inverse by a or b over the squared coordinate; the off-diagonals use the product ab scaled by (R + R inverse) over the product of coordinates. No lemmas are applied beyond the matrix constructor.
why it matters
This definition supplies the concrete matrix needed for the determinant formula in det_xHessianMatrix2OfR_formula and for the specialization in xHessianMatrix2. It fills the step from the general Hessian entry to the 2×2 closed form, supporting the analysis of nondegeneracy away from the neutral locus in the reciprocal cost model. In the Recognition framework this contributes to the cost structure underlying the forcing chain by providing explicit curvature information in coordinate space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.