dot_AApply
plain-language theorem explainer
The identity states that the weighted dot product of covector β with its image under the rank-one operator A equals the scalar μ times the dot product of β with input v. Researchers verifying the eigenvector property of β under A in finite-dimensional cost projectors cite this step. The proof unfolds the definitions then factors the sum via distributivity and ring simplification.
Claim. Let $A v_i = λ (β^♯)_i (β · v)$ where $β^♯_i = ∑_j h^{-1}_{ij} β_j$ and $μ = λ β · β^♯$. Then $β · (A v) = μ (β · v)$.
background
The Cost.Ndim.Projector module develops the finite-dimensional operator algebra for rank-one tensors. The weighted dot product is defined by dot(α, t) = ∑_i α_i t_i. The sharp map raises a one-form β to a vector via the inverse kernel: β^♯_i = ∑_j hInv_i j β_j. The operator AApply is the rank-one update A v = λ β^♯ (β · v), while mu extracts the coefficient μ = λ β · β^♯ for the quadratic relation A² = μ A.
proof idea
The proof unfolds dot, AApply, and mu, then applies a calc chain. It factors the sum using Finset.mul_sum and sum_congr with ring to pull out the common dot β v term. A second ring step commutes the scalars, and simp recovers the definition of mu.
why it matters
This identity supports the quadratic law for operator A and feeds directly into the downstream theorem AApply_sq establishing A² = μ A. It supplies the algebraic verification step in the rank-one tensor picture of the cost module, consistent with the Recognition framework's projector constructions that lead to the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.