IsProjector
plain-language theorem explainer
An endomorphism P of a real module is a projector precisely when it is idempotent: P composed with itself equals P. Anyone working the algebraic projector-to-golden step from the Hessian cost-geometry paper cites this predicate. The body is the standard one-line idempotence equation on Module.End.
Claim. An endomorphism $P$ of a real module $V$ is a projector when $P\circ P=P$.
background
The module CostProjectorGolden isolates the purely algebraic core of the paper Golden and Metallic Structures on Hessian Manifolds. That paper builds a normalized projector from the rank-one Hessian of reciprocal cost geometry; once idempotence holds, two derived operators follow at once.
The almost-product operator is $F=2P-I$, and the golden operator is $G=\varphi P+(1-\varphi)(I-P)$. The forcing claim is algebraic: $P^2=P$ implies $F^2=I$ and $G^2=G+I$. The ambient type is endomorphisms of a real module $V$ (AddCommGroup with Module structure over $\mathbb{R}$), deliberately free of manifold structure.
Status of the module is zero sorry and zero new axiom. The predicate here is the single gate that every later square identity in the file opens with.
proof idea
Definition, not a theorem. The body is the Prop $P*P=P$ on Module.End $\mathbb{R}$ $V$, i.e. ordinary idempotence of the endomorphism ring multiplication. No lemmas are applied.
why it matters
This predicate is the hypothesis of the two main algebraic identities in the module: almost-product square ($P^2=P$ implies $(2P-I)^2=I$) and golden-operator square ($P^2=P$ implies $G^2=G+I$). It is also the conclusion of normalizedProjector_isProjector (scale a near-idempotent $A^2=\mu A$ by $\mu^{-1}$) and of rankOneEnd_normalized_isProjector for nondegenerate rank-one maps.
Downstream, ProjectorGoldenCertificate packages the universal almost-product and golden-structure statements under this predicate. In JHessianGoldenMulti the multi-coordinate cost-Hessian operator normalizes to a projector (paper Corollary 3.1), then inherits the golden equation. The golden relation $G^2=G+I$ is the operator form of the fixed-point equation that forces $\varphi$ in the Recognition stack (T6), so the predicate sits on the algebraic bridge from cost Hessian geometry into the phi-forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.