almostProduct_sq
plain-language theorem explainer
If an endomorphism P is a projector (P² = P), the almost-product operator F = 2P − I satisfies F² = I. Anyone citing the algebraic projector-to-golden step in the cost-geometry forcing stack needs this identity. The proof is a short pointwise expansion that substitutes the projector law and simplifies.
Claim. Let $P$ be an endomorphism of a real module $V$ with $P^2 = P$. Define the almost-product operator $F := 2P - I$. Then $F^2 = I$.
background
This module isolates the algebraic core of the paper on golden and metallic structures on Hessian manifolds: a normalized projector $P$ built from the rank-one Hessian of reciprocal cost geometry induces an almost-product operator and then a golden operator. The setting is endomorphisms of a real module $V$, not a full Hessian-manifold formalization.
A projector is an endomorphism with $P\cdot P = P$. The almost-product operator is $F = 2\bullet P - 1$ (i.e., $2P - I$). Downstream, the golden operator is $G = \varphi P + (1-\varphi)(I-P)$, and the target polynomial law is $G^2 = G + I$. The present lemma is the intermediate almost-product identity $F^2 = I$ forced by $P^2 = P$.
proof idea
Tactic proof by extensionality on vectors. For arbitrary $v$, the projector hypothesis gives $P(Pv) = Pv$ by applying the endomorphism equality $P\cdot P = P$ at $v$. Unfold almost-product as $2P - I$, rewrite subtraction as addition of negation, substitute $P(Pv) = Pv$, and finish with the module tactic to clear the linear combination to the identity action.
why it matters
This is the first algebraic brick in the projector-to-golden chain. The parent certificate projector_golden_certificate packages it as the almost_product field: any cost-induced normalized projector carries the golden-operator equation, with cost geometry supplying the projector and this theorem supplying the polynomial structure forced by being a projector.
In the Recognition stack, that certificate is the algebraic step linking reciprocal cost geometry to the golden operator $G^2 = G + I$, which sits beside the forcing landmarks that fix $\varphi$ (T6) and the J-cost uniqueness (T5). The module is closed (0 sorry, 0 new axioms); this lemma is pure algebra and does not itself invoke $\varphi$ or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.