module module moderate

`IndisputableMonolith.Cost.Ndim.XCoordinates`

The XCoordinates module defines the active x-coordinate direction as the ratio α_i / x_i inside the N-dimensional reciprocal cost. Researchers extending the scalar J-cost to vector settings would cite these coordinate objects. It is a definition module with no proofs.

claimThe active x-coordinate direction is given by $α_i / x_i$.

background

The upstream Core module states: 'This module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate.' The XCoordinates module specializes that construction to the x-coordinates. The local setting is the Cost domain of Recognition Science, where the scalar kernel is lifted to N dimensions via weighted log aggregates.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the x-coordinate direction that supports the Hessian matrix and diagonal correction definitions inside the same Cost.Ndim namespace. It extends the core N-dimensional cost model toward the full multi-component reciprocal cost used in the Recognition framework.

scope and limits

Does not prove any properties of the active direction.
Does not define coordinates in y or z directions.
Does not connect directly to the phi-ladder or forcing chain.
Does not supply numerical implementations or examples.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Ndim.Core module_import

declarations in this module (15)

def xDirection L23
def xDiagonalCorrection L27
def xHessianEntry L31
def xHessianMatrix L36
theorem xHessianEntry_offDiag L39
theorem xHessianEntry_diag L45
theorem xHessianEntry_zero_cost L55
abbrev vec2 L65
def xHessianMatrix2OfR L69
def xHessianMatrix2 L79
theorem xHessianMatrix2_eq_general L82
theorem det_xHessianMatrix2OfR_formula L91
theorem det_xHessianMatrix2_formula L100
theorem det_xHessianMatrix2_zero_cost L112
theorem det_xHessianMatrix2_ne_zero_of_generic L121