FApply_MetallicApply
plain-language theorem explainer
The theorem shows that the almost-product operator F applied to MetallicApply(p, q) v equals (p/2) F v plus (sqrt(p² + 4q)/2) v. Researchers deriving quadratic relations for metallic operators in the finite-dimensional cost algebra would cite it when closing the operator identities. The proof is a direct term reduction that unfolds MetallicApply and rewrites via linearity of F together with its involution property.
Claim. Let $F$ be the almost-product operator $F(v) = 2P(v) - v$ induced by parameters $lam$, $hInv$, and covector $β$. Let $M_{p,q}(v) = (p/2) v + (√(p² + 4q)/2) F(v)$. Then, provided $μ(lam, hInv, β) ≠ 0$, one has $F(M_{p,q}(v)) = (p/2) F(v) + (√(p² + 4q)/2) v$.
background
The Cost.Ndim.Projector module builds the finite-dimensional operator algebra from a covector β and inverse metric kernel hInv. These determine a sharp vector, the operator A = h^{-1} g̃ satisfying A² = μ A, the normalized projector P, and the almost-product operator F = 2P - I. The metallic family is defined directly from F as the linear combination (p/2)v + (√(p² + 4q)/2) F(v). Upstream results establish that F is additive and homogeneous, and that F(F v) = v whenever μ ≠ 0.
proof idea
The proof is a term-mode reduction. It unfolds the definition of MetallicApply, then rewrites the expression by applying the additivity theorem FApply_add, the scalar-multiplication theorems FApply_smul (twice), and the involution theorem FApply_square under the nonzero-μ hypothesis.
why it matters
This identity is the immediate predecessor of MetallicApply_square, which establishes the quadratic law for the metallic operator. It supplies a required algebraic step in the rank-one tensor picture described in the module documentation. Within Recognition Science it supports the cost-induced structures that feed the forcing chain and the emergence of metallic ratios from the almost-product operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.