ProjectorGoldenCertificate
plain-language theorem explainer
Bundles the algebraic projector-to-golden package: any real-module endomorphism projector induces an almost-product involution and a golden operator satisfying G² = G + I, with rank-one and normalization specializations, plus the positive scalar root forcing φ. The cost-geometry forcing stack and the Hessian-manifold paper bridge cite this certificate. It is a definitional Prop structure; the inhabiting theorem wires already-proved sibling lemmas.
Claim. A certificate asserting eight algebraic facts: (i) if $P$ is a projector on a real module then $F=2P-I$ satisfies $F^2=I$ and $G=\varphi P+(1-\varphi)(I-P)$ satisfies $G^2=G+I$; (ii) any endomorphism with $A^2=\mu A$ and $\mu\neq 0$ normalizes to a projector whose golden operator obeys the same equation; (iii) a rank-one map $v\otimes\ell$ squares to $(\ell v)\cdot(v\otimes\ell)$, and when $\ell v\neq 0$ its normalization is a projector with golden structure; (iv) the unique positive solution of $\lambda^2=\lambda+1$ is $\varphi$.
background
The module is the algebraic core of the paper Golden and Metallic Structures on Hessian Manifolds. Reciprocal cost geometry supplies a rank-one Hessian tensor that normalizes to a projector $P$ with $P^2=P$. The forcing stack only needs the pure endomorphism consequences of that identity, not the full manifold apparatus.
A projector is an endomorphism $P$ with $P\cdot P=P$. From it one builds the almost-product operator $F=2P-I$ and the golden operator $G=\varphi P+(1-\varphi)(I-P)$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation. Normalization takes any $A$ obeying $A^2=\mu A$ with $\mu\neq 0$ to $\mu^{-1}A$, which is then a projector. Rank-one ends $v\otimes\ell$ are the model case coming from the Hessian construction.
The local claim is deliberately algebraic over an arbitrary real module: once $P^2=P$, one obtains $F^2=I$ and $G^2=G+I$, and the positive root of $\lambda^2=\lambda+1$ is forced to be $\varphi$.
proof idea
No proof body: this is a Prop-valued structure that packages eight named fields. Each field is a universal statement over real modules (projectors, normalized operators, rank-one ends, and the scalar golden equation). The inhabiting theorem projector_golden_certificate fills the fields by pointing at the sibling lemmas almostProduct_sq, goldenOperator_sq, normalizedProjector_isProjector, normalizedProjector_goldenOperator_sq, rankOneEnd_square, and the corresponding rank-one and scalar results. Those lemmas do the actual algebra (expand $F=2P-I$ or $G=\varphi P+(1-\varphi)(I-P)$ and cancel using $P^2=P$).
why it matters
This certificate is the typed interface between cost-induced projectors and the golden polynomial structure required by the Recognition forcing stack. Downstream, projector_golden_certificate inhabits it, so any cost geometry that produces a normalized projector automatically inherits $G^2=G+I$.
In the framework landmarks this sits at the projector-to-golden step that feeds T5/T6: J-uniqueness and the forcing of $\varphi$ as the self-similar fixed point. The scalar field golden_scalar_forces_phi is exactly the positive root of $\lambda^2=\lambda+1$, matching the metallic mean that appears once the almost-product and golden operators are in place. The module doc stresses status: zero sorry, zero new axiom, algebraic core only.
Parent use is the single inhabiting theorem; that theorem is what the Hessian-paper bridge and later forcing lemmas quote when they say a cost projector carries golden structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.