IndisputableMonolith.Cost.Ndim.XCoordinates
This module defines the active x-coordinate direction as the ratio α_i / x_i in the N-dimensional reciprocal cost framework. It supplies supporting definitions for directions, diagonal corrections, and Hessian entries that extend the scalar kernel. Researchers modeling multi-component costs cite these when handling coordinate-specific contributions. The module is purely definitional and imports only the core Ndim definitions.
claimThe active x-coordinate direction is the ratio $α_i / x_i$, equipped with maps for diagonal corrections and Hessian matrix entries $H_{ij}$ in the N-dimensional reciprocal cost.
background
The upstream Core module defines the N-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. This XCoordinates module specializes that construction to the active x-directions. It introduces xDirection for the ratio α_i/x_i together with xDiagonalCorrection, xHessianEntry (off-diagonal, diagonal, and zero-cost cases), and the associated 2-by-2 Hessian matrices.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the x-specific coordinate components that feed into the full N-dimensional cost computations and Hessian analyses within the Cost.Ndim package. It completes the direction slot required by the multi-component reciprocal cost definition.
scope and limits
- Does not contain any theorem statements or proofs.
- Does not define the complete reciprocal cost function.
- Does not address y-coordinates or other directions.
- Does not import modules beyond Core.
depends on (1)
declarations in this module (15)
-
def
xDirection -
def
xDiagonalCorrection -
def
xHessianEntry -
def
xHessianMatrix -
theorem
xHessianEntry_offDiag -
theorem
xHessianEntry_diag -
theorem
xHessianEntry_zero_cost -
abbrev
vec2 -
def
xHessianMatrix2OfR -
def
xHessianMatrix2 -
theorem
xHessianMatrix2_eq_general -
theorem
det_xHessianMatrix2OfR_formula -
theorem
det_xHessianMatrix2_formula -
theorem
det_xHessianMatrix2_zero_cost -
theorem
det_xHessianMatrix2_ne_zero_of_generic