PApply_sub
The normalized projector PApply respects vector subtraction in finite dimensions. Researchers developing the cost-induced operator algebra cite this when verifying linearity of the rank-one projector. The proof is a short tactic sequence that rewrites subtraction via additivity and negation lemmas already established for PApply.
claimLet $P$ be the normalized projector $P(v) = mu^{-1} A(v)$ associated to the almost-product operator $A$ induced by inverse metric kernel $h^{-1}$ and covector $β$. 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 inverse of the scalar $μ$ (see the definition of PApply). Vec $n$ denotes the type of $n$-component real vectors, i.e., maps from Fin $n$ to ℝ. Upstream lemmas establish additivity $P(v + w) = P(v) + P(w)$ and negation $P(-w) = -P(w)$, which together imply the subtraction rule.
proof idea
The proof proceeds in tactic mode. The ext tactic reduces the vector equality to componentwise statements indexed by $i$. The sub_eq_add_neg rewrite converts the left-hand side into an addition of a negation, after which the already-proved PApply_add and PApply_neg lemmas are applied directly, followed by simp to finish the componentwise identities.
why it matters in Recognition Science
PApply_sub supplies the subtraction property required by the downstream theorem PApply_FApply, which verifies that the projector applied to the almost-product operator F recovers the original vector. It completes the basic linearity checks for the normalized projector inside the cost framework, supporting the finite-dimensional model of the rank-one tensor algebra described in the module documentation. No open scaffolding remains for this algebraic identity.
scope and limits
- Does not establish homogeneity under arbitrary real scalars.
- Does not address infinite-dimensional or continuous limits.
- Does not compute or bound the normalization factor mu.
- Does not derive any spectral properties of the projector.
Lean usage
theorem use_PApply_sub {n : ℕ} (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v w : Vec n) : PApply lam hInv β (v - w) = PApply lam hInv β v - PApply lam hInv β w := PApply_sub lam hInv β v wformal statement (Lean)
151theorem PApply_sub {n : ℕ}
152 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
153 (v w : Vec n) :
154 PApply lam hInv β (v - w) = PApply lam hInv β v - PApply lam hInv β w := by
proof body
Term-mode proof.
155 ext i
156 simp [sub_eq_add_neg, PApply_add, PApply_neg]
157