GApply
plain-language theorem explainer
GApply defines the golden operator on n-dimensional real vectors as the linear combination of the identity with the almost-product operator FApply, using coefficients 1/2 and √5/2. Researchers working on the finite-dimensional cost algebra in Recognition Science cite this definition when composing operators in the projector family. The definition is a direct one-line functional expression that applies scalar multiplication and vector addition to FApply.
Claim. For natural number $n$, real parameter $λ$, inverse metric kernel $h^{-1}:[n]×[n]→ℝ$, and covector $β∈ℝ^n$, the golden operator $G:ℝ^n→ℝ^n$ is defined by $G(v)=½v+(√5/2)F(v)$, where $F$ is the almost-product operator induced by the same $λ$, $h^{-1}$, and $β$.
background
The Cost.Ndim.Projector module packages the finite-dimensional operator algebra for cost-induced projectors. Vectors are coordinate functions Fin n → ℝ. The almost-product operator FApply is the map v ↦ 2P v - v, where P is the normalized projector built from the rank-one update using the inverse kernel hInv and covector β. This sits inside the rank-one tensor picture in which an operator A satisfies A² = μ A, yielding the projector P and then the derived family of operators.
proof idea
The definition is a one-line wrapper that applies the linear combination ((1:ℝ)/2)•v + (Real.sqrt 5 / 2)•FApply lam hInv β v, using the vector space operations on Vec n and the already-defined FApply from the same module.
why it matters
GApply supplies the golden operator that is invoked by the composition theorems FApply_GApply and GApply_square in the same module. It completes the metallic family derived from the almost-product operator, furnishing the operator-level realization of the self-similar fixed point in the Recognition Science cost algebra. The construction aligns with the J-uniqueness step of the forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.