MetallicApply
plain-language theorem explainer
MetallicApply constructs the metallic operator family on n-dimensional vectors from parameters p, q and the almost-product operator FApply. Workers on finite-dimensional models in Recognition Science cite this when generalizing the golden operator to metallic cases in the cost projector algebra. The definition directly assembles a scaled sum of the input vector and its image under FApply using the quadratic root coefficient.
Claim. MetallicApply(p, q, λ, h^{-1}, β)(v) = (p/2) v + (√(p² + 4q)/2) F(v), where F is the almost-product operator F = 2P - I induced by covector β and inverse kernel h^{-1}.
background
Vec n denotes the space of n-component real vectors as maps Fin n → ℝ. The module develops the finite-dimensional operator algebra for the rank-one tensor picture in cost-induced projectors. A covector β together with inverse metric kernel hInv determines the sharp vector, the operator A = h^{-1} g̃ satisfying A² = μ A, and the normalized projector P. FApply implements the induced almost-product operator F = 2P - I.
proof idea
One-line wrapper that applies the linear combination (p/2) • v + (sqrt(p² + 4q)/2) • FApply lam hInv β v.
why it matters
This definition supplies the metallic operator used by the theorems FApply_MetallicApply and MetallicApply_square, which establish its commutation and squaring properties. It completes the metallic family derived from the same almost-product operator in the cost projector module. In the Recognition framework it extends the golden operator to support the quadratic relations needed for the rank-one tensor algebra behind the cost-induced projectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.