PApply_sub
plain-language theorem explainer
PApply_sub establishes linearity of the normalized projector PApply under vector subtraction in finite dimensions. Researchers on the cost-induced operator algebra in Recognition Science cite it to confirm that the projector respects the underlying vector space operations. The proof is a short tactic sequence that rewrites subtraction via the additivity and negation lemmas already proved for PApply.
Claim. Let $P$ be the normalized projector associated to parameters $λ$, inverse kernel $h^{-1}$, and covector $β$, defined by $P(v) = μ^{-1} · A(v)$ where $A$ is the almost-product operator and $μ$ its normalization factor. Then for vectors $v, w ∈ ℝ^n$, $P(v - w) = P(v) - P(w)$.
background
The Cost.Ndim.Projector module packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector β and inverse metric kernel hInv determine the sharp vector, the operator A = h^{-1} g̃, its quadratic law, and the normalized projector P. Vec n is the type of n-component real vectors, i.e., maps Fin n → ℝ. PApply implements the normalized projector as (mu lam hInv β)^{-1} • AApply lam hInv β v. This theorem relies on the upstream results PApply_add, which shows additivity of PApply, and PApply_neg, which shows that PApply preserves negation.
proof idea
The proof applies the extensionality tactic ext to reduce the functional equality to pointwise equality on components. It then invokes simp with the rewriting sub_eq_add_neg together with the lemmas PApply_add and PApply_neg to reduce the subtraction case to the already-proved addition and negation cases.
why it matters
PApply_sub is invoked by the downstream theorem PApply_FApply to establish that the projector satisfies P(F v) = P v. It completes the basic linearity properties of the projector within the cost-induced algebra, supporting the almost-product operator F = 2P - I described in the module documentation. This step aligns with the finite-dimensional setup underlying the Recognition Science derivation of physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.