Pith. sign in
module module moderate

IndisputableMonolith.Cost.Ndim.Hessian

show as:
view Lean formalization →

Defines the log-coordinate gradient and Hessian of the multi-component reciprocal cost, with entrywise formulas, the Hessian matrix, and its quadratic action on directions. Metric, projector, and radical-distribution modules import these objects. Content is explicit algebraic identities for a rank-one Hessian along the active weight direction.

claimFor the $N$-dimensional reciprocal cost in log coordinates, the module supplies gradient entries, Hessian entries $H_{ij}$, the matrix $H$, and the quadratic form $v \mapsto v^{\top} H v$. The Hessian is supported only along the active weight direction $\alpha$: it vanishes whenever $\alpha \cdot v = 0$, and scales homogeneously under constant factors on the cost.

background

The parent Core module lifts the scalar reciprocal cost kernel through a weighted log aggregate, yielding a multi-component cost $J_{\log N}$ on log-coordinates $t \in \mathbb{R}^n$. The scalar kernel is the RS $J$-cost $J(x)=(x+x^{-1})/2-1$; the $N$-dimensional version aggregates componentwise logs with weights $\alpha$.

Second derivatives of that aggregate in log coordinates produce a Hessian that is necessarily rank-one: only the direction of $\alpha$ is visible to the cost. Gradient and Hessian entries are therefore elementary rational (or hyperbolic) functions of the coordinates and weights, not abstract tensors.

This module sits between those core definitions and the geometric layer (metric, projectors, radical distribution) that treats $H$ as a degenerate bilinear form on the log chart.

proof idea

Definition module: gradient and Hessian entries, the matrix, pointwise evaluation, and apply-maps for the associated quadratic form are introduced by direct formulas. Supporting lemmas are short algebraic reductions: Hessian entries vanish in the expected index patterns, evaluation at zero is zero, constant rescaling of the cost multiplies the Hessian by that factor, and applying $H$ recovers a multiple of the active direction (or zero when the input is $\alpha$-orthogonal).

why it matters in Recognition Science

Supplies the concrete second-derivative data that the log-coordinate cost metric module turns into a bilinear form, and that the projector module packages into the rank-one operator algebra ($A=h^{-1}\tilde g$, $A^2=\mu A$, normalized $P$). The radical-distribution module quotes the same rank-one picture directly: the Hessian detects only $\alpha$, so its radical is the constant hyperplane $\alpha\cdot v=0$ with affine leaves ${\alpha\cdot t=c}$.

In the broader RS cost stack this is the finite-dimensional bridge from the scalar $J$-uniqueness (forcing-chain T5 / RCL) to multi-component geometry used by metallic and golden operators. Without explicit Hessian entries those downstream operator identities have nothing to act on.

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)