costHessianOperator_normalized_isProjector
plain-language theorem explainer
On any real inner-product space, the multi-coordinate recognition-cost Hessian operator, after scaling by its nonzero eigenvalue, is an algebraic projector. Anyone citing paper Corollary 3.1 or assembling the multi-coordinate golden-structure certificate needs this fact. The proof is a one-line application of the rank-one normalized-projector lemma, using nonvanishing of the Hessian quadratic form at α ≠ 0.
Claim. For any vectors $\alpha, t$ in a real inner-product space $V$ with $\alpha \neq 0$, if $A$ is the endomorphism induced by the multi-coordinate cost Hessian at $t$ in direction $\alpha$ and $\mu = \langle A\alpha, \alpha \rangle$, then $\mu^{-1} A$ is a projector: $(\mu^{-1} A)^2 = \mu^{-1} A$.
background
This module extends one-dimensional Phase 4 φ-forcing to the multi-coordinate recognition cost. In log-coordinates the cost is $J(t)=\cosh(\alpha\cdot t)-1$ for a comparison direction $\alpha\neq 0$. Its Hessian is the rank-one tensor $\nabla^2 J=\cosh(\alpha\cdot t),(\alpha\otimes\alpha)$, positive semidefinite of rank one in every dimension.
Pairing with the reference metric yields the $(1,1)$-tensor $A$ satisfying $A^2=\mu A$ with $\mu=\cosh(\alpha\cdot t),|\alpha|^2=\mathrm{tr},A$. The scalar $\mu$ is strictly positive by $\cosh>0$ and $\alpha\neq 0$. The normalized operator $P=A/\mu$ is then a projector in the sense $P\circ P=P$ (paper Corollary 3.1).
Upstream, IsProjector is the proposition $P*P=P$, and normalizedProjector is scalar inversion $\mu^{-1}\bullet A$. The rank-one endomorphism lemma already proves that any rank-one operator of this shape normalizes to a projector once the quadratic form on the generating vector is nonzero.
proof idea
Term-mode one-liner. Apply rankOneEnd_normalized_isProjector to the bilinear cost-Hessian form at $(\alpha,t)$, with generating vector $\alpha$. The side condition that the self-pairing of the form on $\alpha$ is nonzero is discharged by costHessianForm_self_ne_zero, which uses $\alpha\neq 0$ together with positivity of $\cosh$. No further algebraic work is done here.
why it matters
This is the projector half of multi-coordinate Phase 4 closure. Downstream, jHessianGoldenMultiCertificate packages four facts (positive curvature scalar, positive eigenvalue, operator square law $A^2=\mu A$, and this normalized-projector statement) into the golden-structure interface. From the projector $P$ one builds $G=\varphi P+(1-\varphi)(I-P)$, which satisfies $G^2=G+I$ and forces the positive eigenvalue to be the golden ratio $\varphi$ (paper §4, eq. (6.7)).
In the forcing chain this is the multi-coordinate upgrade of the unit curvature $J''(1)=1$ used in the one-dimensional JHessianGolden route, and it holds over an arbitrary real inner-product space, so the dimension is unrestricted. It feeds the T6 φ-forcing story: φ appears as the self-similar fixed point of the induced golden operator rather than being inserted by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.