FApply_neg
plain-language theorem explainer
The theorem establishes that the almost-product operator FApply is odd, sending the negation of any vector to the negation of its image. Researchers verifying homogeneity in the finite-dimensional operator algebra for Recognition Science cost projectors would cite this result. The proof is a one-line wrapper that invokes the scalar-multiplication rule FApply_smul at scalar -1.
Claim. Let $F$ be the operator defined by $F(v) = 2P(v) - v$, where $P$ is the projector induced by scalar parameter $λ$, inverse metric kernel $h^{-1}$, and covector $β$. Then $F(-w) = -F(w)$ for every vector $w$ in the $n$-dimensional real space.
background
The module packages the finite-dimensional operator algebra behind the rank-one tensor picture. Vectors are coordinate functions from Fin n to reals. The operator FApply is defined by F(v) = 2 • PApply lam hInv β v - v, the induced almost-product operator F = 2P - I. Upstream, FApply_smul establishes the scalar rule F(c • v) = c • F(v) for any real scalar c.
proof idea
The proof is a one-line wrapper that applies FApply_smul with scalar -1 to the vector w, then uses simpa to obtain the negation identity.
why it matters
This result supports the additivity proof in FApply_sub, which closes the basic algebraic structure for the golden and metallic operators. It fills a homogeneity step in the projector algebra that underlies cost-induced operators, consistent with the self-similar fixed-point structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.