normalizedProjector_isProjector
plain-language theorem explainer
If an endomorphism satisfies A² = μA with μ ≠ 0, then P = μ⁻¹ A is a genuine projector (P² = P). Anyone citing the Hessian-geometry route from cost tensors to golden operators needs this algebraic step. The proof is a short pointwise calculation: apply A² = μA, cancel the scalar with field_simp, and simplify the normalized definition.
Claim. Let $A$ be an endomorphism of a real module $V$ and let $\mu \in \mathbb{R}$ with $\mu \neq 0$. If $A^2 = \mu A$, then the normalized operator $P = \mu^{-1} A$ is a projector: $P^2 = P$.
background
This module isolates the algebraic core of the paper on golden and metallic structures on Hessian manifolds. Reciprocal cost geometry produces a rank-one Hessian tensor; after normalization one obtains an endomorphism $P$ that should be a projector. The forcing stack only needs the pure algebra: once $P^2 = P$, the almost-product operator $F = 2P - I$ satisfies $F^2 = I$, and the golden operator $G = \varphi P + (1-\varphi)(I-P)$ satisfies $G^2 = G + I$.
A projector endomorphism is defined by $P \cdot P = P$. The normalized projector of a scalar $\mu$ and an operator $A$ is simply $\mu^{-1} \bullet A$. The hypothesis $A^2 = \mu A$ is the algebraic shadow of a rank-one Hessian construction (later specialized via rank-one endomorphisms $x \mapsto \ell(x),v$). The ambient space $V$ is a real module; no manifold structure is used here.
proof idea
Pointwise on vectors. From $A \cdot A = \mu \bullet A$, evaluate both sides at $v$ to get $A(Av) = \mu \bullet Av$. The scalar identity $\mu^{-1}\cdot\mu^{-1}\cdot\mu = \mu^{-1}$ follows by field_simp from $\mu \neq 0$. Unfold normalizedProjector, rewrite with smul_smul and the pointwise relation, then cancel via the scalar identity. Extensionality of endomorphisms finishes $P^2 = P$.
why it matters
This is the algebraic projector step named in the Hessian-geometry paper and required by the projector-to-golden forcing path. Downstream, normalizedProjector_goldenOperator_sq lifts the same hypotheses to $G^2 = G + I$ for the golden operator built from the normalized projector. The rank-one specialization rankOneEnd_normalized_isProjector is a one-line application: a nondegenerate rank-one endomorphism squares to a scalar multiple of itself, so normalization yields a projector. Both feed projector_golden_certificate, which packages almost-product, golden structure, and the normalized-operator facts into a single certificate that cost-induced projectors carry the golden polynomial. In the broader Recognition stack this is the pure-algebra hinge between cost geometry and the golden fixed-point structure tied to $\varphi$ (T5–T6), deliberately free of manifold scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.