xHessianMatrix2
plain-language theorem explainer
xHessianMatrix2 supplies the concrete 2 by 2 Hessian for x-coordinates in the two-component reciprocal cost by substituting the weighted aggregate R into the general entry formula. Researchers deriving determinant expressions or degeneracy criteria in the positive-coordinate cost model cite this specialization. The definition is a one-line wrapper that feeds the aggregate of the two vec2 arguments directly into xHessianMatrix2OfR.
Claim. Let $R = $ aggregate of vectors $(a,b)$ and $(x,y)$. The $2$ by $2$ matrix is defined by substituting this $R$ into the general Hessian entries: diagonal blocks scale by $a/(2x^2)$ and $b/(2y^2)$ with factors $((a-1)R + (a+1)R^{-1})$ and $((b-1)R + (b+1)R^{-1})$, while off-diagonal blocks are $(ab/(2xy))(R + R^{-1})$.
background
The module records positive-coordinate Hessian formulas for the multi-component reciprocal cost. The aggregate definition computes the exponential aggregate $R(x) = $ exp of the dot product of the coefficient vector with the log of the coordinate vector. The vec2 abbreviation constructs two-component vectors in coordinate order. The xHessianMatrix2OfR definition supplies the general $2$ by $2$ matrix with an explicit aggregate parameter $R$.
proof idea
The definition is a one-line wrapper that applies xHessianMatrix2OfR to the four scalars together with the aggregate of vec2 a b and vec2 x y.
why it matters
This definition supplies the concrete matrix object required by the determinant formula, the nondegeneracy criterion away from the neutral locus, and the zero-cost degeneracy statement. It completes the specialization from the general entry formula to the $2$ by $2$ case, enabling explicit algebraic work on the Hessian in the Recognition Science cost model. The neutral locus where aggregate equals 1 produces a degenerate Hessian, consistent with the framework emphasis on cost minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.