PApply_neg
plain-language theorem explainer
The normalized projector P associated to parameters λ, inverse kernel h^{-1} and covector β satisfies P(-w) = -P(w) for any vector w. Researchers extending the finite-dimensional cost-induced operator algebra would cite this homogeneity when building linear combinations. The proof is a one-line wrapper that instantiates the scalar-multiplication rule at scalar -1.
Claim. Let $P$ be the normalized projector $P(v) = (mu)^{-1} A(v)$, where $A$ is the almost-product operator determined by real parameter $λ$, inverse kernel $h^{-1}$ and covector $β$. Then $P(-w) = -P(w)$ for every vector $w$.
background
The Cost.Ndim.Projector module packages the finite-dimensional operator algebra for the rank-one tensor picture. A covector $β$ and inverse metric kernel $hInv$ determine an operator $A$ via AApply that obeys the quadratic law $A^2 = μ A$, together with the normalized projector PApply defined by $P(v) = (mu λ hInv β)^{-1} • A(v)$. Vectors live in the type Vec n of maps from Fin n to ℝ.
proof idea
The proof is a one-line wrapper that applies the scalar-multiplication theorem PApply_smul with scalar -1.
why it matters
This result is invoked directly by the proof of PApply_sub, which establishes additivity of the projector and is required to define the induced almost-product operator F = 2P - I. It closes a basic linearity property of the cost-induced projectors in the finite-dimensional setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.