AApply_neg
plain-language theorem explainer
The rank-one operator AApply satisfies AApply lam hInv β (-w) = -AApply lam hInv β w for any input vector w. Researchers verifying linearity of cost-induced projectors in the finite-dimensional Recognition Science algebra would cite this result. The proof is a one-line wrapper that instantiates the scalar-multiplication theorem AApply_smul at the factor -1.
Claim. For any natural number $n$, real scalar $λ$, inverse metric kernel $h^{-1} : Fin n → Fin n → ℝ$, and vectors $β, w ∈ ℝ^n$, the rank-one operator satisfies $A(λ, h^{-1}, β, -w) = -A(λ, h^{-1}, β, w)$, where $A(λ, h^{-1}, β, v)_i = λ · (β♯)_i · (β · v)$.
background
The module Cost.Ndim.Projector packages the finite-dimensional operator algebra behind the rank-one tensor picture. A covector β and inverse metric kernel hInv determine the sharp vector β♯ and the operator A = h^{-1} g̃ with g̃ = λ β ⊗ β; this A obeys the quadratic law A² = μ A and feeds the normalized projector P. Vec n is the type of n-component real vectors, represented as functions Fin n → ℝ. The upstream theorem AApply_smul states that AApply lam hInv β (c • v) = c • AApply lam hInv β v, encoding homogeneity under scaling.
proof idea
The proof is a one-line wrapper that applies the scalar-multiplication theorem AApply_smul with scalar factor -1.
why it matters
AApply_neg is invoked by the additivity theorem AApply_sub, which completes the verification that AApply is linear. In the Recognition Science framework this algebraic property supports the projector P and the almost-product operators in the cost module. It contributes to the finite-dimensional realization of the rank-one operators underlying the forcing chain and the phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.