mu
plain-language theorem explainer
mu defines the scalar coefficient μ such that the rank-one operator A obeys the quadratic law A squared equals μ times A. Workers on finite-dimensional cost projectors cite this when establishing scaling and idempotence relations for the algebra. It is realized as the direct product of λ with the dot product of β against its index-raised image under the inverse kernel.
Claim. $μ(λ, h^{-1}, β) = λ (β · β^♯)$, where β^♯ is the vector whose i-th component equals ∑_j h^{-1}_{i j} β_j.
background
The module assembles the finite-dimensional operator algebra for rank-one tensors arising from cost. Vectors are coordinate maps from a finite index set of size n to the reals. The dot product sums the componentwise products of two such maps. The sharp map raises a covector β to a vector by contracting against the inverse kernel hInv.
proof idea
This is a one-line definition that multiplies λ by the dot product of β with the vector produced by applying sharp to β under hInv.
why it matters
The scalar μ supplies the eigenvalue factor in the quadratic relation A² = μ A and is invoked by the surrounding theorems that derive the action of A, the normalized projector P, and the metallic operators. It closes the algebraic identities required for the rank-one tensor picture in the cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.