pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Hessian

show as:
view Lean formalization →

This module supplies the log-coordinate gradient and Hessian entries for the N-dimensional reciprocal J-cost. Workers on cost-induced metrics and projectors cite these when lifting scalar kernels to finite dimensions. The definitions are direct lifts from the Core module via weighted log aggregates, with no internal proofs required.

claimThe gradient entry $g_i = J'_{logN}(x) / x_i$ and Hessian matrix entries $H_{ij}$ for the log-coordinate cost $J_{logN}$ on $N$ components, where $J$ is the scalar kernel $J(x) = (x + x^{-1})/2 - 1$.

background

The module sits inside the Cost domain and imports the N-dimensional reciprocal cost definitions from Core. Core lifts the scalar J-kernel through a weighted log aggregate to produce the multi-component cost function. The Hessian module then extracts the first and second derivatives of this cost expressed in logarithmic coordinates, yielding gradientEntry and hessianEntry together with the associated matrix and application operators.

proof idea

This is a definition module, no proofs. All objects are introduced by direct abbreviation or equation from the scalar J-kernel and the log-coordinate change of variables supplied by the Core import.

why it matters in Recognition Science

The module supplies the Hessian structure required by the downstream Cost metric in log coordinates, the cost-induced projector algebra, and the radical distribution for the rank-one log metric. It therefore closes the finite-dimensional operator picture that feeds the Recognition Science cost framework and the associated rank-one tensor constructions.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)