FApply
The definition constructs the almost-product operator F as twice the normalized projector P minus the identity map. Researchers deriving algebraic identities for cost-induced operators in finite dimensions cite this construction when proving linearity or involution properties. It is realized directly by the expression 2P(v) minus v.
claimLet $P$ be the normalized projector $P(v) = mu^{-1} A(v)$ associated to scalar $lam$, inverse kernel $hInv$, and covector $beta$. The induced almost-product operator is defined by $F(v) = 2P(v) - v$.
background
The module packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector $beta$ and inverse metric kernel $hInv$ determine a sharp vector, an operator $A = h^{-1} tilde g$ obeying the quadratic law $A^2 = mu A$, and the normalized projector $P$. Vec n denotes the type of n-component real vectors, realized as maps from Fin n to real numbers.
proof idea
One-line definition that constructs the map sending each vector v to twice the image under PApply minus v itself.
why it matters in Recognition Science
This supplies the almost-product operator F that appears throughout the projector family. It feeds the additivity, scaling, negation, and involution theorems such as FApply_square and FApply_GApply. The construction closes the finite-dimensional cost algebra that supports the larger Recognition forcing chain and composition laws.
scope and limits
- Does not establish linearity or involution properties of F.
- Does not fix the dimension n or the value of lam.
- Does not address infinite-dimensional or continuous limits.
- Does not incorporate the golden ratio or metallic means.
formal statement (Lean)
41noncomputable def FApply {n : ℕ}
42 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
proof body
Definition body.
43 fun v => 2 • PApply lam hInv β v - v
44
45/-- The induced golden operator. -/