Pith. sign in
module module moderate

IndisputableMonolith.Cost.Ndim.XCoordinates

show as:
view Lean formalization →

Defines the active x-coordinate chart for the N-dimensional reciprocal cost: direction fields αᵢ/xᵢ, diagonal corrections, and the Hessian of the multi-component cost in those coordinates. Supplies 2D specializations and an explicit determinant formula for the 2×2 Hessian. Cited by anyone computing second-variation structure or curvature of the N-dim cost away from the scalar kernel. Pure definition and algebraic identity layer on top of Cost.Ndim.Core.

claimIn the $x$-chart of the multi-component reciprocal cost, the active direction is $\alpha_i/x_i$. The module assembles the Hessian entries $H_{ij}$ (diagonal and off-diagonal), the full Hessian matrix, its $2\times 2$ specialization, and the closed-form determinant $\det H^{(2)}(r)$ of that specialization.

background

The parent module Cost.Ndim.Core lifts the scalar reciprocal cost kernel to $N$ components by a weighted log aggregate. That construction yields a multi-variable cost whose first and second derivatives are most naturally written in reciprocal (or log-ratio) coordinates.

This module fixes the active $x$-chart: each coordinate direction is the ratio $\alpha_i/x_i$ rather than a raw Cartesian increment. From that choice one obtains diagonal correction terms, individual Hessian entries $H_{ij}$, and the assembled Hessian matrix. A two-dimensional specialization (vec2, $H^{(2)}$) is singled out because many Recognition calculations reduce to a pair of conjugate channels.

Notation follows the Core conventions: the scalar kernel is the usual $J$-cost (T5 uniqueness), and the multi-component lift inherits the Recognition Composition Law structure componentwise through the weighted log sum.

proof idea

Definition module. It introduces xDirection, the diagonal correction, Hessian entry formulas (on- and off-diagonal, including the zero-cost locus), matrix assemblies, and the 2D special case. Algebraic identities such as xHessianMatrix2_eq_general and det_xHessianMatrix2OfR_formula are direct expansions of those definitions; no deep lemmas beyond Core are required.

why it matters in Recognition Science

Second-variation and curvature statements for the N-dimensional reciprocal cost need an explicit Hessian in a concrete chart. The $x$-coordinate Hessian and its 2×2 determinant feed any later positivity, signature, or stability argument for the multi-component cost surface. In the broader Recognition chain this sits under the Cost domain that ultimately supports mass-ladder and coupling calculations built on the unique $J$-kernel (T5) and the self-similar fixed point $\phi$ (T6). No downstream consumers are wired yet in the graph; the module is infrastructure for those curvature lemmas.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)