FApply_MetallicApply
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the quadratic relation for MetallicApply itself.
- Does not hold when μ(lam, hInv, β) = 0.
- Does not address infinite-dimensional extensions.
- Does not compute the explicit value of μ or link it to the golden ratio.
formal statement (Lean)
238theorem FApply_MetallicApply {n : ℕ}
239 (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
240 (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
241 FApply lam hInv β (MetallicApply p q lam hInv β v)
242 = (p / 2) • FApply lam hInv β v
243 + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v := by
proof body
Term-mode proof.
244 unfold MetallicApply
245 rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
246