forced
plain-language theorem explainer
Packages the algebraic fact that any endomorphism projector forces a golden operator: if P² = P, then G = φP + (1-φ)(I-P) obeys G² = G + I. Cited across foundation, constants, action convexity, and certificate layers that need the golden relation without Hessian geometry. Definitional structure (no proof body); the identities live in sibling lemmas.
Claim. A structure recording that a projector $P$ on a real module (i.e. $P^2 = P$) forces the golden endomorphism $G = \varphi P + (1-\varphi)(I-P)$ to satisfy the golden equation $G^2 = G + I$, together with the companion almost-product $F = 2P - I$ obeying $F^2 = I$.
background
The module is the algebraic core of the paper Golden and Metallic Structures on Hessian Manifolds, stripped of manifold data. On a real module one has endomorphisms; a normalized projector $P$ is an endomorphism with $P^2 = 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 self-similar fixed-point step of the forcing chain.
Sibling definitions supply the raw maps (normalizedProjector, almostProduct, goldenOperator, rankOneEnd) and the predicate IsProjector. The local claim is purely algebraic: projector idempotence alone yields $F^2 = I$ and $G^2 = G + I$. No Hessian metric or reciprocal-cost geometry is assumed here; that geometry only motivates why such a $P$ appears in the paper.
proof idea
No proof body: this is a structure declaration (definitional packaging), not a theorem. The identities it stands for are proved in sibling lemmas such as normalizedProjector_isProjector, almostProduct_sq, goldenOperator_sq, and normalizedProjector_goldenOperator_sq, by direct expansion of endomorphism composition and the minimal polynomial of $\varphi$. Consumers inhabit or reference the structure rather than re-derive $G^2 = G + I$.
why it matters
This is the projector-to-golden bridge required by the forcing stack: once a rank-one cost projector exists, the golden operator (and thus golden/metallic structure) is algebraically inevitable. Downstream it is referenced widely: action convexity (actionJ_convex_on_interp) uses the J-cost geometry that the projector organizes; constant lemmas such as hbar_pos sit on the same $\varphi$-native units; astrophysics and chemistry certificates (pulsar periods, tidal locking, noble-gas shell sums) inherit $\varphi$-ladder and resonance structure that ultimately rest on golden algebra.
In framework terms it sits under T5–T6 (J-uniqueness and $\varphi$ as self-similar fixed point): the golden equation $G^2 = G + I$ is the operator form of the same quadratic that fixes $\varphi$. The module deliberately stops at endomorphisms, leaving full Hessian-manifold formalization open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.