innerForm_apply
plain-language theorem explainer
Applying the comparison one-form of the multi-coordinate recognition cost to a vector recovers the ambient real inner product against the distinguished direction α. Anyone packaging the rank-one Hessian ∇²J = cosh(α·t)(α⊗α) will cite this as the simp bridge between the linear-map form and the metric dual. The equality is definitional; the proof is reflexivity.
Claim. For vectors $\alpha,x$ in the real inner-product space $V$, the comparison one-form associated to $\alpha$ evaluates by $\omega_\alpha(x)=\langle\alpha,x\rangle_{\mathbb{R}}$.
background
The module lifts one-dimensional Phase-4 φ-forcing to a genuine multi-coordinate recognition cost. In log coordinates $t_i=\log x_i$ the reciprocal cost is $J(t)=\cosh(\alpha\cdot t)-1$ for a nonzero comparison direction $\alpha\in V$. Its Hessian is the rank-one tensor $\nabla^2 J=\cosh(\alpha\cdot t),(\alpha\otimes\alpha)$, positive semidefinite in every dimension.
The comparison one-form is the metric dual of that direction: $\omega(X)=\langle\alpha,X\rangle$ (paper: $\omega=\sum\alpha_i,dx_i/x_i$). In Lean it is packaged as a real-linear map innerForm α : V →ₗ[ℝ] ℝ whose underlying function is exactly the ambient inner product. The present lemma is the evaluation rule for that packaging.
The ambient space $V$ is an arbitrary real inner-product space, so the construction is dimension-independent and matches the paper's inner-product model of the reference Hessian metric $h_0$.
proof idea
One-line term proof by rfl. The linear map was defined with toFun := fun x => inner ℝ α x, so applying it is definitionally the inner product; no further lemmas are required.
why it matters
This simp lemma is the evaluation interface for the comparison one-form that seeds every subsequent Hessian object in the module: the curvature scalar along the comparison direction, the rank-one cost-Hessian form, and the normalized projector $P=A/\mu$ with $\mu=\cosh(\alpha\cdot t)|\alpha|^2$. Those objects force the golden operator $G=\varphi P+(1-\varphi)(I-P)$ satisfying $G^2=G+I$, which is the multi-coordinate closure of Phase 4 (T5–T6 J-uniqueness and φ as self-similar fixed point).
The nondegeneracy source is exactly $\cosh>0$ together with $\alpha\neq 0$; the one-form must evaluate as the genuine inner product for that source to be visible. No downstream external users are recorded yet; the lemma is consumed inside the same Hessian cascade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.