FApply_smul
plain-language theorem explainer
The theorem establishes homogeneity of the almost-product operator F under scalar multiplication of its input vector. Researchers on finite-dimensional cost operators in Recognition Science cite it when composing golden or metallic applications and verifying algebraic closure. The proof is a direct term-mode reduction that invokes the scalar-multiplication rule for the underlying projector PApply and finishes with ring simplification.
Claim. Let $F$ be the almost-product operator induced by parameter $lam$, inverse metric kernel $hInv$, and covector $β$, defined by $F(v) = 2P(v) - v$ where $P$ is the normalized projector. Then $F(c · v) = c · F(v)$ for any real scalar $c$ and vector $v$.
background
The module Cost.Ndim.Projector develops the finite-dimensional operator algebra behind the rank-one tensor picture. Vectors are coordinate functions Vec n := Fin n → ℝ. The almost-product operator is defined by FApply lam hInv β v := 2 • PApply lam hInv β v - v, where PApply is the normalized projector determined by the inverse metric kernel and covector β.
proof idea
The proof applies function extensionality to reduce to componentwise equality. It then simplifies using the definition of FApply together with the scalar-multiplication theorem PApply_smul, invokes commutativity of multiplication, and closes with the ring tactic.
why it matters
This result supplies the homogeneity needed for the golden and metallic operators. It is invoked directly in the proofs of FApply_neg, FApply_GApply, and FApply_MetallicApply. Within the Recognition framework it ensures the almost-product operator respects the self-similar scaling enforced by the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.