det_xHessianMatrix2_ne_zero_of_generic
plain-language theorem explainer
Nondegeneracy of the 2 by 2 x-coordinate Hessian holds away from the neutral locus where the aggregate R equals 1 and away from the secondary discriminant zero set. Analysts of the reciprocal cost Hessian in Recognition Science cite this when establishing local invertibility of coordinate maps for generic positive weights and coordinates. The argument substitutes the closed-form determinant expression and factors the numerator into the supplied nonzero terms using aggregate positivity and basic field arithmetic.
Claim. Let $R = e^{a log x + b log y}$. Suppose $x ≠ 0$, $y ≠ 0$, $a ≠ 0$, $b ≠ 0$, $R ≠ 1$, and $R^2(a + b - 1) + (a + b + 1) ≠ 0$. Then the determinant of the $2 × 2$ x-coordinate Hessian matrix built from weights $(a, b)$ and coordinates $(x, y)$ is nonzero.
background
The module records explicit formulas for the x-coordinate Hessian of the multi-component reciprocal cost. The aggregate function is the exponential aggregate $R = exp(α · log x)$, where the dot product is taken after taking componentwise logarithms of the positive coordinate vector. The vec2 abbreviation constructs the two-dimensional vectors $[a, b]$ and $[x, y]$. The xHessianMatrix2 definition specializes the general Hessian matrix to this aggregate value R. An upstream theorem supplies the closed-form determinant factorization for the resulting 2 by 2 matrix.
proof idea
The proof defines R as the aggregate of the weight and coordinate vectors, then invokes aggregate_pos to obtain R > 0 and hence R ≠ 0 together with R + 1 ≠ 0. It verifies the denominator 4 R² x² y² is nonzero by successive mul_ne_zero applications to the squared terms. After rewriting the determinant via the formula theorem, it chains mul_ne_zero, neg_ne_zero, and sub_ne_zero to confirm that the numerator factor a b (R - 1) (R + 1) disc is nonzero under the four explicit hypotheses.
why it matters
This result supplies the generic nondegeneracy criterion for the 2 by 2 x-Hessian inside the positive-coordinate formulas module. It supports analysis of local invertibility for the reciprocal cost away from the neutral locus R = 1. Within the Recognition Science framework it contributes to the cost structure that underlies the forcing chain steps T5 through T8 and the phi-ladder mass formulas by guaranteeing the Hessian remains invertible for generic positive coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.