AApply_sub
plain-language theorem explainer
The theorem establishes linearity of the rank-one operator A under vector subtraction: A(v - w) equals A v minus A w. Researchers verifying algebraic properties of cost-induced projectors in finite-dimensional Recognition Science models would cite it when confirming that A is a linear map. The proof is a one-line wrapper that rewrites subtraction as addition of a negative and invokes the additivity and negation lemmas.
Claim. Let $A$ be the rank-one operator defined by $A(v)_i = λ · (β^♯)_i · (β · v)$, where $β^♯$ is obtained from the inverse metric kernel $h^{-1}$ and $λ$ is the scalar coefficient. Then for any vectors $v, w ∈ ℝ^n$, $A(v - w) = A v - A w$.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra for the rank-one tensor picture. Vec n denotes n-component real vectors as functions Fin n → ℝ. The operator AApply lam hInv β maps a vector v to the vector whose i-th component is lam times the sharp vector component times the dot product β · v; this encodes A = h^{-1} g̃ with g̃ = λ β ⊗ β. The module documentation states that a covector β and inverse metric kernel hInv determine the sharp vector β♯, the operator A, its quadratic law A² = μ A, and the normalized projector P.
proof idea
The proof is a term-mode one-liner. It applies ext i to reduce vector equality to componentwise equality, then uses simp with sub_eq_add_neg, AApply_add, and AApply_neg. This rewrites the left-hand side as A(v + (-w)) and distributes via the already-proved additivity and negation properties.
why it matters
This declaration verifies that AApply is linear, a prerequisite for the quadratic relation A² = μ A and the normalized projector P in the rank-one tensor picture. It belongs to the algebraic development of cost-induced projectors that support Recognition Science finite-dimensional approximations. No downstream uses appear yet, but the result underpins the almost-product, golden, and metallic operators listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.