FApply_GApply
plain-language theorem explainer
Algebraic relation between the almost-product operator F and golden operator G: F applied to G v equals half of F v plus (sqrt five over two) times v. Researchers on Recognition Science finite-dimensional projectors cite this for closing the metallic operator algebra. The term-mode proof substitutes the definition of G and reduces via linearity and the involution F squared equals the identity.
Claim. Let $F$ be the almost-product operator $F=2P-I$ and $G$ the golden operator $G=1/2 I + (√5/2) F$ induced by λ, inverse kernel $h^{-1}$, and covector β in dimension n. Assuming μ(λ, $h^{-1}$, β) ≠ 0, then for any vector v, $F(Gv) = (1/2) Fv + (√5/2) v$.
background
This module packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector β and an inverse metric kernel hInv determine a sharp vector β♯, an operator A = h^{-1} g̃ with quadratic law A² = μ A, and the normalized projector P. Vectors are maps Fin n → ℝ.
proof idea
Unfolds the definition of GApply to write G v as a linear combination of v and F v. Applies the additivity and scalar-multiplication theorems for FApply to push F inside the combination. Invokes FApply_square under the hypothesis hμ to replace F(F v) by v, producing the target identity.
why it matters
Feeds directly into the proof of GApply_square, which establishes the quadratic relation for the golden operator. This closes the algebraic structure of the golden and metallic families in the cost-induced projector setting. It supports the self-similar fixed-point structures associated with the golden ratio in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.