GApply_square
plain-language theorem explainer
The golden operator G satisfies G(Gv) = Gv + v whenever the scalar mu is nonzero. Researchers verifying algebraic closure of cost-induced projectors in the finite-dimensional Recognition Science setting would cite this identity. The proof expands G via its definition in terms of F, invokes the companion relation FApply_GApply, and reduces the resulting sqrt(5) multiples by direct arithmetic.
Claim. Let $G$ denote the golden operator $G(v) = (1/2)v + (√5/2)F(v)$, where $F$ is the almost-product operator induced by parameters $λ$, inverse metric $h^{-1}$, and covector $β$. Then $G(G(v)) = G(v) + v$ for every vector $v$, provided the scalar $μ(λ, h^{-1}, β) ≠ 0$.
background
The module packages the finite-dimensional operator algebra for the rank-one tensor picture. A covector $β$ and inverse metric kernel $hInv$ determine a sharp vector $β♯$, an operator $A = h^{-1} g̃$ obeying the quadratic law $A^2 = μ A$, and the normalized projector $P$. The almost-product operator is then $F = 2P - I$, and the golden operator is defined by $G(v) = (1/2)v + (√5/2)F(v)$.
proof idea
The tactic proof applies extensionality on components. It invokes the upstream theorem FApply_GApply to equate F applied to a linear combination of $v$ and $F(v)$ with the symmetric combination, simplifies the squared coefficients of √5 via nlinarith and ring, substitutes the simplified expression back into the definition of G, and concludes with nlinarith.
why it matters
This identity verifies the quadratic-like closure of the golden operator inside the projector algebra, supporting the self-similar fixed-point structure tied to the golden ratio. It fills an algebraic step required by the metallic-family operators even though no downstream results yet cite it. The construction aligns with the T6 forcing of phi as the self-similar fixed point in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.