innerForm
plain-language theorem explainer
The comparison one-form of the multi-coordinate recognition cost is the real-linear functional pairing a fixed direction α against an arbitrary tangent vector by the ambient inner product. Anyone building the multi-coordinate J-Hessian or the golden projector cites this as the metric dual of the comparison direction. The definition packages Mathlib's real inner product as a linear map, discharging additivity and homogeneity by the standard inner-product identities.
Claim. For a fixed comparison direction $\alpha$ in a real inner-product space $V$, the comparison one-form is the real-linear map $\omega_\alpha:V\to\mathbb{R}$ given by $\omega_\alpha(X)=\langle\alpha,X\rangle$.
background
This module lifts one-dimensional $\varphi$-forcing from the single-ray cost to the genuine multi-coordinate recognition manifold. The $n$-dimensional reciprocal cost is $J(x_1,\ldots,x_n)=\tfrac12(R+R^{-1})-1$ with $R=\prod x_i^{\alpha_i}$ and $\alpha\in\mathbb{R}^n\setminus{0}$. In logarithmic coordinates $t_i=\log x_i$ one has $J(t)=\cosh(\alpha\cdot t)-1$, whose Hessian is the rank-one tensor $\nabla^2 J=\cosh(\alpha\cdot t),(\alpha\otimes\alpha)$.
Pairing that tensor with a nondegenerate reference Hessian metric $h_0$ produces the $(1,1)$-tensor $A=h_0^{-1}\nabla^2 J$. On the inner-product model $h_0$ is the identity, so the first lowered index is simply the metric dual of the comparison direction $\alpha$. The paper writes this dual as $\omega=\sum\alpha_i,dx_i/x_i$ (equivalently $V=h^{-1}\omega$). The present definition is exactly that dual, realized as a real-linear functional on an arbitrary real inner-product space.
proof idea
Definitional construction of a LinearMap over $\mathbb{R}$. The underlying function is Mathlib's real inner product against the fixed vector $\alpha$. Additivity is discharged by inner_add_right; scalar homogeneity by real_inner_smul_right (with the identity ring homomorphism on $\mathbb{R}$). No further lemmas are required.
why it matters
Immediate parent is the cost-Hessian functional, obtained by scaling this one-form by the curvature scalar $\cosh(\alpha\cdot t)$ to realize the lowered rank-one Hessian $\cosh(\alpha\cdot t),(\alpha\otimes\alpha)$. That form builds the cost-Hessian operator $A$, which satisfies $A^2=\mu A$ with $\mu=\operatorname{tr} A>0$, normalizes to a projector $P=A/\mu$, and induces the golden operator $G=\varphi P+(1-\varphi)(I-P)$ with $G^2=G+I$, forcing the positive eigenvalue to be $\varphi$.
This is the multi-coordinate Phase 4 closure of the forcing chain (T5 J-uniqueness, T6 $\varphi$ as self-similar fixed point), following Washburn-Zlatanović on golden structures on Hessian manifolds. The nondegeneracy source $\mu=\cosh(\alpha\cdot t)|\alpha|^2>0$ is the higher-dimensional analogue of the unit curvature $J''(1)=1$ used in the one-dimensional golden Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.