pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Hessian

show as:
view Lean formalization →

The module defines log-coordinate gradient entries and Hessian structures for the N-dimensional reciprocal cost JlogN. Researchers extending scalar J-cost to vector settings for metrics and projectors cite these definitions. Content consists of direct lifts from the scalar kernel via weighted log aggregates in the imported Core module.

claimGradient entry $\partial_i J_{\log N}$ and Hessian matrix $H_{ij}$ of the multi-component reciprocal cost in log coordinates.

background

The Core module defines N-dimensional reciprocal cost by lifting the scalar J-kernel through a weighted log aggregate. This Hessian module specializes to log-coordinate derivatives of that aggregate. The underlying J satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ and appears in the forcing chain as the uniqueness map T5.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Feeds the log-coordinate cost metric, the cost-induced projector algebra with its quadratic law $A^2=\mu A$, and the radical distribution on the hyperplane orthogonal to the active direction. Supports the rank-one tensor picture in the Recognition framework and the transition from scalar to N-dimensional cost structures.

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)