PApply_add
plain-language theorem explainer
The normalized projector PApply preserves addition of vectors in finite dimensions. Researchers developing the cost-induced operator algebra for rank-one tensors in Recognition Science cite this when composing projectors with sums. The proof is a direct reduction: componentwise extensionality simplifies via the definition of PApply and the additivity of AApply, then normalizes by ring arithmetic.
Claim. Let $P$ be the normalized projector given by $P(v) = (mu)^{-1} A(v)$, where $A$ is the almost-product operator induced by inverse metric kernel $hInv$ and covector $β$, and $mu$ is the associated scalar. Then $P(v + w) = P(v) + P(w)$ for all vectors $v, w$ in the space of $n$-component real vectors.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra for the rank-one tensor picture. A covector $β$ and inverse metric kernel $hInv$ determine a sharp vector, the operator $A = h^{-1} ˜g$ obeying the quadratic law $A^2 = μ A$, and the normalized projector $P$ obtained by scaling $A$ by the reciprocal of $μ$ (see the definition of PApply). Vec $n$ is the type of $n$-component real vectors, realized as functions from Fin $n$ to ℝ. This additivity result rests on the upstream theorem AApply_add, which establishes the corresponding property for the un-normalized operator $A$.
proof idea
The proof is a short tactic sequence. Extensionality reduces the vector equation to a componentwise statement. Simplification unfolds the definition of PApply and invokes the additivity theorem for AApply. The resulting scalar expression is normalized by the ring tactic.
why it matters
This theorem supplies the additivity needed to construct the almost-product operator $F = 2P - I$ and is invoked directly in the proofs of FApply_add and PApply_sub. It fills a basic algebraic step in the finite-dimensional projector package that supports the broader cost-induced operator algebra of the Recognition framework, consistent with the rank-one tensor picture outlined in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.