xHessianMatrix2_eq_general
plain-language theorem explainer
Equality between the specialized 2x2 x-coordinate Hessian matrix and the general entry-wise definition holds for any real parameters a b x y. Researchers computing Hessians of reciprocal costs in two dimensions cite it to switch between explicit matrix and entry formulas. The verification uses index extensionality, finite case splitting on Fin 2, and algebraic simplification.
Claim. For real numbers $a,b,x,y$, the $2times2$ x-coordinate Hessian matrix constructed from the aggregate $R$ of vectors $(a,b)$ and $(x,y)$ coincides with the matrix whose $(i,j)$ entry is computed by the general x-coordinate Hessian entry formula applied to those vectors.
background
This module develops positive-coordinate Hessian formulas for the multi-component reciprocal cost. The general entry is expressed using the aggregate $R = $ aggregate $alpha x$, after which the formulas are specialized to the $2times2$ case to support determinant calculations and degeneracy statements. vec2 assembles two real numbers into a vector of length 2. xDirection extracts the ratios $alpha_i / x_i$ for each component. xDiagonalCorrection supplies the term $alpha_i / x_i^2$ on the diagonal and zero elsewhere. xHessianEntry assembles each matrix entry from the combination $((R + R^{-1})/2) times$ product of directions minus $((R - R^{-1})/2) times$ the diagonal correction. xHessianMatrix2OfR builds the explicit matrix with these terms, and xHessianMatrix2 inserts the actual aggregate value for $R$.
proof idea
The proof reduces the matrix equality to entrywise equality via extensionality. It then splits into the four index cases with fin_cases on $i$ and $j$, applies simplification using the definitions of xHessianMatrix2, xHessianMatrix2OfR, xHessianEntry, xDirection, xDiagonalCorrection and vec2, and resolves the resulting algebraic identities with the ring tactic.
why it matters
The declaration confirms consistency between the specialized and general presentations of the $2times2$ x-Hessian, which is required for the closed-form determinant factorization and nondegeneracy criteria developed in the same module. It thereby supports the broader analysis of the reciprocal cost Hessian that feeds into the Recognition Science derivation of physical constants and dimensions from the J-uniqueness and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.