almostProduct

The module isolates the purely algebraic core of the paper on golden and metallic structures on Hessian manifolds. Reciprocal cost geometry supplies a normalized rank-one projector $P$ on the tangent module; the forcing stack only needs the endomorphism algebra that follows from $P^2 = P$.

An endomorphism $P$ is a projector when $P \circ P = P$. From any such $P$ 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. The module works over an arbitrary real module $V$ with no Hessian or manifold structure assumed.

Status of the file is zero sorry and zero new axioms; this definition is the first named operator in that chain.

Definition only: the body is the endomorphism scalar combination $2 \bullet P - 1$, i.e. $F = 2P - I$ in the ring of module endomorphisms. No tactics, no lemmas.

This is the operator whose square is the identity once $P$ is a projector. Downstream, almostProduct_sq proves exactly that: $P^2 = P$ implies $F^2 = I$. The same operator appears in the first field of ProjectorGoldenCertificate, the Prop package that packages the algebraic projector-to-golden step for the forcing stack.

In the Recognition framework the step sits under the cost-geometry side of the foundation: once the Hessian rank-one projector exists, the almost-product and golden relations are forced algebraically, feeding the metallic-structure layer that interfaces with $\varphi$ (T6) without re-deriving the projector from geometry inside Lean. The module deliberately stops at endomorphisms; full Hessian formalization is out of scope here.