costHessianForm_self
plain-language theorem explainer
Evaluating the multi-coordinate cost-Hessian form on the comparison direction itself recovers the rank-one eigenvalue density times the squared norm: μ = cosh(α·t)·‖α‖². Anyone tracking the Hessian spectrum of J(t) = cosh(α·t)−1 on the recognition manifold would cite this identity. The proof is a one-line specialization of the form's apply lemma.
Claim. For comparison direction $\alpha$ and log-coordinate point $t$ in the ambient real inner-product space, the cost-Hessian form evaluated on $\alpha$ equals $\cosh(\langle\alpha,t\rangle)\cdot\langle\alpha,\alpha\rangle$.
background
The module extends one-dimensional Phase 4 φ-forcing to the multi-coordinate recognition cost manifold (Washburn–Zlatanović). The $n$-dimensional reciprocal cost is $J=\tfrac12(R+R^{-1})-1$ with $R=\prod x_i^{\alpha_i}$, which in log coordinates $t_i=\log x_i$ is $J(t)=\cosh(\alpha\cdot t)-1$. Its Hessian is the rank-one tensor $\nabla^2 J=\cosh(\alpha\cdot t),(\alpha\otimes\alpha)$.
The cost-Hessian scalar is the curvature density $\cosh(\alpha\cdot t)$. The cost-Hessian form is the lowered rank-one tensor $\ell(X)=\cosh(\alpha\cdot t),\langle\alpha,X\rangle$. Pairing with the reference metric produces the $(1,1)$-tensor $A$ with $A^2=\mu A$ and $\mu=\cosh(\alpha\cdot t),|\alpha|^2$, which normalizes to a projector and forces the golden operator.
proof idea
One-line term proof. simp applies the cost-Hessian form apply lemma, which states $\ell(X)=\cosh(\alpha\cdot t),\langle\alpha,X\rangle$, and specializes the free slot $X$ to $\alpha$. No further algebraic work.
why it matters
This identity is the algebraic step that exposes the eigenvalue $\mu=\cosh(\alpha\cdot t),|\alpha|^2$ as the self-pairing of the form (paper: $\mu=g(V,V)=\mathrm{tr},A$). The immediate parent is the nondegeneracy lemma, which rewrites through this identity and then uses $\cosh>0$ together with $\alpha\neq 0$ to get $\mu>0$. That nondegeneracy is the multi-coordinate analogue of $J''(1)=1>0$ from the one-dimensional golden-Hessian route, and it supplies the strictly positive scale that lets $A/\mu$ become a projector and the induced golden operator $G=\varphi P+(1-\varphi)(I-P)$ satisfy $G^2=G+I$, forcing eigenvalue $\varphi$ (Phase 4 closure, T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.