goldenOperator_sq
plain-language theorem explainer
A real endomorphism that is a projector induces a golden operator G satisfying G² = G + I. Anyone citing the algebraic core of the projector-to-golden step in the Recognition forcing stack would use this. The proof expands G on vectors, applies P² = P and the identity φ² = φ + 1, then finishes by ring and module arithmetic.
Claim. Let $P$ be an endomorphism of a real module $V$ with $P^2 = P$. Define the golden operator $G = \varphi P + (1-\varphi)(I - P)$, where $\varphi$ is the golden ratio. Then $G^2 = G + I$.
background
This module isolates the algebraic step from the paper on golden and metallic structures on Hessian manifolds: once a rank-one Hessian construction supplies a projector, the golden operator is forced. The setting is endomorphisms of a real module $V$, not a full manifold formalization.
A projector is an endomorphism $P$ with $P^2 = P$. The golden operator built from $P$ is $G = \varphi P + (1-\varphi)(I-P)$, with $\varphi$ the positive root of $x^2 - x - 1 = 0$. The companion almost-product operator is $F = 2P - I$, which squares to the identity; the present result is the golden twin of that fact.
The only external arithmetic input is the golden-ratio identity $\varphi^2 = \varphi + 1$ from Constants.phi_sq_eq. Everything else is endomorphism algebra over $\mathbb{R}$.
proof idea
Pointwise on vectors: ext v. From the projector hypothesis, $P(Pv) = Pv$. Rewrite $\varphi^2 = \varphi + 1$ and the complementary scalar identity $(1-\varphi)^2 = 2-\varphi$ via phi_sq_eq and a short ring/nlinarith calculation. Expand $G(Gv)$ with the definition of the golden operator, push scalars and maps through map_add/map_smul, substitute the two scalar identities, and close with the module tactic.
why it matters
This is the algebraic core named in the module header: projectors force golden operators. Downstream, normalizedProjector_goldenOperator_sq lifts the same identity to operators that only satisfy $A^2 = \mu A$ with $\mu \neq 0$ after normalization, and projector_golden_certificate packages the whole family (almost-product, golden structure, normalized variants, rank-one squares) as a single certificate.
In the Recognition stack the golden ratio is forced as the self-similar fixed point (T6). The identity $G^2 = G + I$ is exactly the metallic polynomial structure that the cost-geometry projector is required to carry; the certificate theorem states that the cost geometry supplies the projector while this lemma supplies the polynomial. Status is fully proved: zero sorry, zero new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.