AApply_smul
plain-language theorem explainer
The rank-one operator A, built from the inverse metric kernel and covector β, satisfies A(c v) = c A(v) for any real scalar c. Researchers modeling finite-dimensional cost projectors in Recognition Science cite this when deriving the algebra of the normalized projector P and its quadratic relation. The proof reduces componentwise via functional extensionality, unfolds the definitions, and factors the scalar through the dot-product sum using mul_sum, sum_congr, and ring.
Claim. Let $A$ be the rank-one operator defined by $(A v)_i = λ · (β♯)_i · (β · v)$, where β♯ is the vector obtained by raising the covector β with the inverse kernel $h^{-1}$. Then $A(c v) = c · A v$ for any real scalar $c$.
background
The module packages the finite-dimensional operator algebra for cost-induced projectors. Vectors are maps from Fin n to the reals. The dot product is the sum ∑ α_i t_i. The sharp map raises a covector β via the inverse kernel: β♯_i = ∑j hInv{i j} β_j. The operator A is then A(v)_i = λ · β♯_i · (β · v), realizing the rank-one update A = h^{-1} (λ β ⊗ β).
proof idea
Functional extensionality reduces the claim to each component. After unfolding AApply and dot, a calc block pulls the scalar c out of the inner sum via Finset.mul_sum and sum_congr with ring, recognizes the dot product, and commutes the scalar by ring.
why it matters
This linearity is invoked directly in the proofs of AApply_neg, PApply_smul, and PApply_idempotent, which establish the projector algebra needed for the quadratic law A² = μ A. It supports the finite-dimensional side of the Recognition Science operator constructions that feed into the J-uniqueness and phi-ladder steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.